From: Lachnitt Date: Wed, 15 Sep 2021 13:25:54 +0000 (-0700) Subject: [proof] Alethe proof rules (#7180) X-Git-Tag: cvc5-1.0.0~1209 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=56e8b8415727fdd2da72b00d5347e5b9309aca91;p=cvc5.git [proof] Alethe proof rules (#7180) Adds header for Alethe proof rules Co-authored-by: Haniel Barbosa --- diff --git a/src/proof/alethe/alethe_proof_rule.h b/src/proof/alethe/alethe_proof_rule.h new file mode 100644 index 000000000..127bb8161 --- /dev/null +++ b/src/proof/alethe/alethe_proof_rule.h @@ -0,0 +1,427 @@ +/****************************************************************************** + * Top contributors (to current version): + * Hanna Lachnitt + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Enumeration of Alethe proof rules + */ + +#include "cvc5_private.h" + +#ifndef CVC4__PROOF__ALETHE_PROOF_RULE_H +#define CVC4__PROOF__ALETHE_PROOF_RULE_H + +#include + +namespace cvc5 { + +namespace proof { + +enum class AletheRule : uint32_t +{ + // This enumeration lists all Alethe proof rules. For each rule a list of + // steps is given. The last step is the conclusion obtained by applying the + // rule in question. There might be zero or more steps occuring before the + // conclusion in the proof. A step has the form: + // + // G > i. F + // where G is a context, i is an id and F is a formula. A context may include + // substitutions x->y and fixed variables x. For more details see + // https://verit.loria.fr/documentation/alethe-spec.pdf + // + //================================================= Special Rules: Commands + // These rules should be printed as commands + // + // ======== subproof + // > i1. F1 + // ... + // > in. Fn + // ... + // > j. F + // --------------------------------- + // > k. (cl (not F1) ... (not Fn) F) + // + // Each subproof in Alethe begins with an anchor command. The outermost + // application of ANCHOR_SUBPROOF will not be printed. + ANCHOR_SUBPROOF, + // ======== bind + // G,y1,...,yn,x1->y1,...,xn->yn > j. (= F1 F2) + // ------------------------------------------------------ + // G > k. (= (forall (x1 ... xn) F1) (forall (y1 ... yn) F2)) + // + // where y1,...,yn are not free in (forall (x1,...,xn) F2) + ANCHOR_BIND, + // ======== input + // > i. F + ASSUME, + //================================================= Rules of the Alethe + // calculus + // + // ======== true + // > i. true + TRUE, + // ======== false + // > i. (not true) + FALSE, + // ======== not_not + // > i. (cl (not(not(not F))) F) + NOT_NOT, + // ======== and_pos + // > i. (cl (not(and F1 ... Fn)) Fi) + // , with 1 <= i <= n + AND_POS, + // ======== and_neg + // > i. (cl (and F1 ... Fn) (not F1) ... (not Fn)) + AND_NEG, + // ======== or_pos + // > i. (cl (not (or F1 ... Fn)) (not F1) ... (not Fn)) + OR_POS, + // ======== or_neg + // > i. (cl (or F1 ... Fn) (not Fi)) + // , with 1 <= i <= n + OR_NEG, + // ======== xor_pos1 + // > i. (cl (not (xor F1 F2)) F1 F2) + XOR_POS1, + // ======== xor_pos2 + // > i. (cl (not (xor F1 F2)) (not F1) (not F2)) + XOR_POS2, + // ======== xor_neg1 + // > i. (cl (xor F1 F2) F1 (not F2)) + XOR_NEG1, + // ======== xor_neg2 + // > i. (cl (xor F1 F2) (not F1) F2) + XOR_NEG2, + // ======== implies_pos + // > i. (cl (not (implies F1 F2)) (not F1) F2) + IMPLIES_POS, + // ======== implies_neg1 + // > i. (cl (implies F1 F2) F1) + IMPLIES_NEG1, + // ======== implies_neg2 + // > i. (cl (implies F1 F2) (not F2)) + IMPLIES_NEG2, + // ======== equiv_pos1 + // > i. (cl (not (= F1 F2)) F1 (not F2)) + EQUIV_POS1, + // ======== equiv_pos2 + // > i. (cl (not (= F1 F2)) (not F1) F2) + EQUIV_POS2, + // ======== equiv_neg1 + // > i. (cl (= F1 F2) (not F1) (not F2)) + EQUIV_NEG1, + // ======== equiv_neg2 + // > i. (cl (= F1 F2) F1 F2) + EQUIV_NEG2, + // ======== ite_pos1 + // > i. (cl (not (ite F1 F2 F3)) F1 F3) + ITE_POS1, + // ======== ite_pos2 + // > i. (cl (not (ite F1 F2 F3)) (not F1) F2) + ITE_POS2, + // ======== ite_neg1 + // > i. (cl (ite F1 F2 F3) F1 (not F3)) + ITE_NEG1, + // ======== ite_neg2 + // > i. (cl (ite F1 F2 F3) (not F1) (not F2)) + ITE_NEG2, + // ======== eq_reflexive + // > i. (= F F) + EQ_REFLEXIVE, + // ======== eq_transitive + // > i. (cl (not (= F1 F2)) ... (not (= F_{n-1} Fn)) (= F1 Fn)) + EQ_TRANSITIVE, + // ======== eq_congruent + // > i. (cl (not (= F1 G1)) ... (not (= Fn Gn)) (= f(F1,...,Fn) + // f(G1,...,Gn))) + EQ_CONGRUENT, + // ======== eq_congruent_pred + // > i. (cl (not (= F1 G1)) ... (not (= Fn Gn)) (= P(F1,...,Fn) + // P(G1,...,Gn))) + EQ_CONGRUENT_PRED, + // ======== distinct_elim + // If called with one argument: + // > i. (= (distinct F) true) + // If applied to terms of type Bool more than two terms can never be distinct. + // Two cases can be possible: + // > i. (= (distinct F G) (not (= F G))) + // and + // > i. (= (distinct F1 F2 F3 ...) false) + // In general: + // > i. (= (distinct F1 ... Fn) (AND^n_i=1 (AND^n_j=i+1 (!= Fi Fj)))) + DISTINCT_ELIM, + // ======== la_rw_eq + // > i. (= (= F G) (and (<= F G) (<= G F))) + LA_RW_EQ, + // Tautology of linear disequalities. + // > i. (cl F1 ... Fn) + LA_GENERIC, + // Tautology of linear integer arithmetic + // > i. (cl F1 ... Fn) + LIA_GENERIC, + // ======== la_disequality + // > i. (= (= F G) (not (<= F G)) (not (<= G F))) + LA_DISEQUALITY, + // ======== la_totality + // > i. (or (<= t1 t2) (<= t2 t1)) + LA_TOTALITY, + // ======== la_tautology + // Tautology of linear arithmetic that can be checked without sophisticated + // reasoning. + LA_TAUTOLOGY, + // ======== forall_inst + // > i. (or (not (forall (x1 ... xn) P)) P[t1/x1]...[tn/xn]) + // args = ((:= x_k1 tk1) ... (:= xkn tkn)) + // where k1,...,kn is a permutation of 1,...,n and xi and ki have the same + // sort. + FORALL_INST, + // ======== qnt_join + // G > i. (= (Q (x1 ... xn) (Q (xn+1 ... xm) F)) (Q (xk1 ... xko) F)) + // where m>n, Q in {forall,exist}, k1...ko is a monotonic map 1,...,m s.t. + // xk1,...,xko are pairwise distinct and {x1,...,xm} = {xk1,...,xko}. + QNT_JOIN, + // ======== qnt_tm_unused + // G > i. (= (Q (x1 ... xn) F) (Q (xk1 ... xkm) F)) + // where m <= n, Q in {forall,exists}, k1,...,km is monotonic map to 1,...,n + // and if x in {xj | j in {1,...,n} and j not in {k1,...,km}} then x is not + // free in P + QNT_RM_UNUSED, + // ======== th_resolution + // > i1. (cl F^1_1 ... F^1_k1) + // ... + // > in. (cl F^n_1 ... F^n_kn) + // ... + // > i1,...,in. (cl F^r1_s1 ... F^rm_sm) + // where (cl F^r1_s1 ... F^rm_sm) are from F^i_j and are the result of a chain + // of predicate resolution steps on the clauses i1 to in. This rule is used + // when the resolution step is not emitted by the SAT solver. + TH_RESOLUTION, + // ======== resolution + // This rule is equivalent to the th_resolution rule but is emitted by the SAT + // solver. + RESOLUTION, + // ======== refl + // G > i. (= F1 F2) + REFL, + // ======== trans + // G > i. (= F1 F2) + // ... + // G > j. (= F2 F3) + // ... + // G > k. (= F1 F3) + TRANS, + // ======== cong + // G > i1. (= F1 G1) + // ... + // G > in. (= Fn Gn) + // ... + // G > j. (= (f F1 ... Fn) (f G1 ... Gn)) + // where f is an n-ary function symbol. + CONG, + // ======== and + // > i. (and F1 ... Fn) + // ... + // > j. Fi + AND, + // ======== tautologic_clause + // > i. (cl F1 ... Fi ... Fj ... Fn) + // ... + // > j. true + // where Fi != Fj + TAUTOLOGIC_CLAUSE, + // ======== not_or + // > i. (not (or F1 ... Fn)) + // ... + // > j. (not Fi) + NOT_OR, + // ======== or + // > i. (or F1 ... Fn) + // ... + // > j. (cl F1 ... Fn) + OR, + // ======== not_and + // > i. (not (and F1 ... Fn)) + // ... + // > j. (cl (not F1) ... (not Fn)) + NOT_AND, + // ======== xor1 + // > i. (xor F1 F2) + // ... + // > j. (cl F1 F2) + XOR1, + // ======== xor2 + // > i. (xor F1 F2) + // ... + // > j. (cl (not F1) (not F2)) + XOR2, + // ======== not_xor1 + // > i. (not (xor F1 F2)) + // ... + // > j. (cl F1 (not F2)) + NOT_XOR1, + // ======== not_xor2 + // > i. (not (xor F1 F2)) + // ... + // > j. (cl (not F1) F2) + NOT_XOR2, + // ======== implies + // > i. (=> F1 F2) + // ... + // > j. (cl (not F1) F2) + IMPLIES, + // ======== not_implies1 + // > i. (not (=> F1 F2)) + // ... + // > j. (not F2) + NOT_IMPLIES1, + // ======== not_implies2 + // > i. (not (=> F1 F2)) + // ... + // > j. (not F2) + NOT_IMPLIES2, + // ======== equiv1 + // > i. (= F1 F2) + // ... + // > j. (cl (not F1) F2) + EQUIV1, + // ======== equiv2 + // > i. (= F1 F2) + // ... + // > j. (cl F1 (not F2)) + EQUIV2, + // ======== not_equiv1 + // > i. (not (= F1 F2)) + // ... + // > j. (cl F1 F2) + NOT_EQUIV1, + // ======== not_equiv2 + // > i. (not (= F1 F2)) + // ... + // > j. (cl (not F1) (not F2)) + NOT_EQUIV2, + // ======== ite1 + // > i. (ite F1 F2 F3) + // ... + // > j. (cl F1 F3) + ITE1, + // ======== ite2 + // > i. (ite F1 F2 F3) + // ... + // > j. (cl (not F1) F2) + ITE2, + // ======== not_ite1 + // > i. (not (ite F1 F2 F3)) + // ... + // > j. (cl F1 (not F3)) + NOT_ITE1, + // ======== not_ite2 + // > i. (not (ite F1 F2 F3)) + // ... + // > j. (cl (not F1) (not F3)) + NOT_ITE2, + // ======== ite_intro + // > i. (= F (and F F1 ... Fn)) + // where F contains the ite operator. Let G1,...,Gn be the terms starting with + // ite, i.e. Gi := (ite Fi Hi Hi'), then Fi = (ite Fi (= Gi Hi) (= Gi Hi')) if + // Hi is of sort Bool + ITE_INTRO, + // ======== duplicated_literals + // > i. (cl F1 ... Fn) + // ... + // > j. (cl Fk1 ... Fkm) + // where m <= n and k1,...,km is a monotonic map to 1,...,n such that Fk1 ... + // Fkm are pairwise distinct and {F1,...,Fn} = {Fk1 ... Fkm} + DUPLICATED_LITERALS, + // ======== connective_def + // G > i. (= (xor F1 F2) (or (and (not F1) F2) (and F1 (not F2)))) + // or + // G > i. (= (= F1 F2) (and (=> F1 F2) (=> F2 F1))) + // or + // G > i. (= (ite F1 F2 F3) (and (=> F1 F2) (=> (not F1) (not F3)))) + CONNECTIVE_DEF, + // ======== Simplify rules + // The following rules are simplifying rules introduced as tautologies that can be + // verified by a number of simple transformations + ITE_SIMPLIFY, + EQ_SIMPLIFY, + AND_SIMPLIFY, + OR_SIMPLIFY, + NOT_SIMPLIFY, + IMPLIES_SIMPLIFY, + EQUIV_SIMPLIFY, + BOOL_SIMPLIFY, + QUANTIFIER_SIMPLIFY, + DIV_SIMPLIFY, + PROD_SIMPLIFY, + UNARY_MINUS_SIMPLIFY, + MINUS_SIMPLIFY, + SUM_SIMPLIFY, + COMP_SIMPLIFY, + NARY_ELIM, + QNT_SIMPLIFY, + // ======== let + // G,x1->F1,...,xn->Fn > j. (= G G') + // --------------------------------- + // G > k. (= (let (x1 := F1,...,xn := Fn.G) G') + LET, + // ======== sko_ex + // G,x1->(e x1.F),...,xn->(e xn.F) > j. (= F G) + // -------------------------------------------- + // G > k. (exists (x1 ... xn) (= F G)) + SKO_EX, + // ======== sko_forall + // G,x1->(e x1.(not F)),...,xn->(e xn.(not F)) > j. (= F G) + // -------------------------------------------------------- + // G > k. (forall (x1 ... xn) (= F G)) + SKO_FORALL, + // ======== symm + // > i. (= F G) + // ... + // > j. (= G F) + SYMM, + // ======== not_symm + // > i. (not (= F G)) + // ... + // > j. (not (= G F)) + NOT_SYMM, + // ======== reorder + // > i1. F1 + // ... + // > j. F2 + // where set representation of F1 and F2 are the same and the number of + // literals in C2 is the same of that of C1. + REORDER, + // ======== undefined + // Used in case that a step in the proof rule could not be translated. + UNDEFINED +}; + +/** + * Converts an Alethe proof rule to a string. + * + * @param id The Alethe proof rule + * @return The name of the Alethe proof rule + */ +const char* aletheRuleToString(AletheRule id); + +/** + * Writes an Alethe proof rule name to a stream. + * + * @param out The stream to write to + * @param id The Alethe proof rule to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, AletheRule id); + +} // namespace proof + +} // namespace cvc5 + +#endif /* CVC4__PROOF__ALETHE_PROOF_RULE_H */