src/proof/alethe/alethe_proof_rule.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Hanna Lachnitt
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Enumeration of Alethe proof rules
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC4__PROOF__ALETHE_PROOF_RULE_H
  19 #define CVC4__PROOF__ALETHE_PROOF_RULE_H
  20
  21 #include <memory>
  22
  23 namespace cvc5 {
  24
  25 namespace proof {
  26
  27 enum class AletheRule : uint32_t
  28 {
  29   // This enumeration lists all Alethe proof rules. For each rule a list of
  30   // steps is given. The last step is the conclusion obtained by applying the
  31   // rule in question. There might be zero or more steps occuring before the
  32   // conclusion in the proof. A step has the form:
  33   //
  34   //   G > i. F
  35   // where G is a context, i is an id and F is a formula. A context may include
  36   // substitutions x->y and fixed variables x. For more details see
  37   // https://verit.loria.fr/documentation/alethe-spec.pdf
  38   //
  39   //================================================= Special Rules: Commands
  40   // These rules should be printed as commands
  41   //
  42   // ======== subproof
  43   // > i1. F1
  44   // ...
  45   // > in. Fn
  46   // ...
  47   // > j. F
  48   // ---------------------------------
  49   // > k. (cl (not F1) ... (not Fn) F)
  50   //
  51   // Each subproof in Alethe begins with an anchor command. The outermost
  52   // application of ANCHOR_SUBPROOF will not be printed.
  53   ANCHOR_SUBPROOF,
  54   // ======== bind
  55   // G,y1,...,yn,x1->y1,...,xn->yn > j.  (= F1 F2)
  56   // ------------------------------------------------------
  57   // G > k. (= (forall (x1 ... xn) F1) (forall (y1 ... yn) F2))
  58   //
  59   // where y1,...,yn are not free in (forall (x1,...,xn) F2)
  60   ANCHOR_BIND,
  61   // ======== input
  62   // > i. F
  63   ASSUME,
  64   //================================================= Rules of the Alethe
  65   // calculus
  66   //
  67   // ======== true
  68   // > i. true
  69   TRUE,
  70   // ======== false
  71   // > i. (not true)
  72   FALSE,
  73   // ======== not_not
  74   // > i.  (cl (not(not(not F)))  F)
  75   NOT_NOT,
  76   // ======== and_pos
  77   // > i.  (cl (not(and F1 ... Fn))  Fi)
  78   // , with 1 <= i <= n
  79   AND_POS,
  80   // ======== and_neg
  81   // > i.  (cl (and F1 ... Fn) (not F1) ... (not Fn))
  82   AND_NEG,
  83   // ======== or_pos
  84   // > i.  (cl (not (or F1 ... Fn)) (not F1) ... (not Fn))
  85   OR_POS,
  86   // ======== or_neg
  87   // > i.  (cl (or F1 ... Fn) (not Fi))
  88   // , with 1 <= i <= n
  89   OR_NEG,
  90   // ======== xor_pos1
  91   // > i.  (cl (not (xor F1 F2)) F1 F2)
  92   XOR_POS1,
  93   // ======== xor_pos2
  94   // > i.  (cl (not (xor F1 F2)) (not F1) (not F2))
  95   XOR_POS2,
  96   // ======== xor_neg1
  97   // > i.  (cl (xor F1 F2) F1 (not F2))
  98   XOR_NEG1,
  99   // ======== xor_neg2
 100   // > i.  (cl (xor F1 F2) (not F1) F2)
 101   XOR_NEG2,
 102   // ======== implies_pos
 103   // > i.  (cl (not (implies F1 F2)) (not F1) F2)
 104   IMPLIES_POS,
 105   // ======== implies_neg1
 106   // > i.  (cl (implies F1 F2) F1)
 107   IMPLIES_NEG1,
 108   // ======== implies_neg2
 109   // > i.  (cl (implies F1 F2) (not F2))
 110   IMPLIES_NEG2,
 111   // ======== equiv_pos1
 112   // > i.  (cl (not (= F1 F2)) F1 (not F2))
 113   EQUIV_POS1,
 114   // ======== equiv_pos2
 115   // > i.  (cl (not (= F1 F2)) (not F1) F2)
 116   EQUIV_POS2,
 117   // ======== equiv_neg1
 118   // > i.  (cl (= F1 F2) (not F1) (not F2))
 119   EQUIV_NEG1,
 120   // ======== equiv_neg2
 121   // > i.  (cl (= F1 F2) F1 F2)
 122   EQUIV_NEG2,
 123   // ======== ite_pos1
 124   // > i.  (cl (not (ite F1 F2 F3)) F1 F3)
 125   ITE_POS1,
 126   // ======== ite_pos2
 127   // > i.  (cl (not (ite F1 F2 F3)) (not F1) F2)
 128   ITE_POS2,
 129   // ======== ite_neg1
 130   // > i.  (cl (ite F1 F2 F3) F1 (not F3))
 131   ITE_NEG1,
 132   // ======== ite_neg2
 133   // > i.  (cl (ite F1 F2 F3) (not F1) (not F2))
 134   ITE_NEG2,
 135   // ======== eq_reflexive
 136   // > i.  (= F F)
 137   EQ_REFLEXIVE,
 138   // ======== eq_transitive
 139   // > i.  (cl (not (= F1 F2)) ... (not (= F_{n-1} Fn)) (= F1 Fn))
 140   EQ_TRANSITIVE,
 141   // ======== eq_congruent
 142   // > i.  (cl (not (= F1 G1)) ... (not (= Fn Gn)) (= f(F1,...,Fn)
 143   // f(G1,...,Gn)))
 144   EQ_CONGRUENT,
 145   // ======== eq_congruent_pred
 146   // > i.  (cl (not (= F1 G1)) ... (not (= Fn Gn)) (= P(F1,...,Fn)
 147   // P(G1,...,Gn)))
 148   EQ_CONGRUENT_PRED,
 149   // ======== distinct_elim
 150   // If called with one argument:
 151   //  > i. (= (distinct F) true)
 152   // If applied to terms of type Bool more than two terms can never be distinct.
 153   // Two cases can be possible:
 154   //  > i. (= (distinct F G) (not (= F G)))
 155   // and
 156   //  > i. (= (distinct F1 F2 F3 ...) false)
 157   // In general:
 158   //  > i. (= (distinct F1 ... Fn) (AND^n_i=1 (AND^n_j=i+1 (!= Fi Fj))))
 159   DISTINCT_ELIM,
 160   // ======== la_rw_eq
 161   // > i. (= (= F G) (and (<= F G) (<= G F)))
 162   LA_RW_EQ,
 163   // Tautology of linear disequalities.
 164   // > i. (cl F1 ... Fn)
 165   LA_GENERIC,
 166   // Tautology of linear integer arithmetic
 167   // > i. (cl F1 ... Fn)
 168   LIA_GENERIC,
 169   // ======== la_disequality
 170   // > i. (= (= F G) (not (<= F G)) (not (<= G F)))
 171   LA_DISEQUALITY,
 172   // ======== la_totality
 173   // > i. (or (<= t1 t2) (<= t2 t1))
 174   LA_TOTALITY,
 175   // ======== la_tautology
 176   // Tautology of linear arithmetic that can be checked without sophisticated
 177   // reasoning.
 178   LA_TAUTOLOGY,
 179   // ======== forall_inst
 180   // > i. (or (not (forall (x1 ... xn) P)) P[t1/x1]...[tn/xn])
 181   // args = ((:= x_k1 tk1) ... (:= xkn tkn))
 182   // where k1,...,kn is a permutation of 1,...,n and xi and ki have the same
 183   // sort.
 184   FORALL_INST,
 185   // ======== qnt_join
 186   // G > i. (= (Q (x1 ... xn) (Q (xn+1 ... xm) F)) (Q (xk1 ... xko) F))
 187   // where m>n, Q in {forall,exist}, k1...ko is a monotonic map 1,...,m s.t.
 188   // xk1,...,xko are pairwise distinct and {x1,...,xm} = {xk1,...,xko}.
 189   QNT_JOIN,
 190   // ======== qnt_tm_unused
 191   // G > i. (= (Q (x1 ... xn) F) (Q (xk1 ... xkm) F))
 192   // where m <= n, Q in {forall,exists}, k1,...,km is monotonic map to 1,...,n
 193   // and if x in {xj | j in {1,...,n} and j not in {k1,...,km}} then x is not
 194   // free in P
 195   QNT_RM_UNUSED,
 196   // ======== th_resolution
 197   // > i1. (cl F^1_1 ... F^1_k1)
 198   // ...
 199   // > in. (cl F^n_1 ... F^n_kn)
 200   // ...
 201   // > i1,...,in. (cl F^r1_s1 ... F^rm_sm)
 202   // where (cl F^r1_s1 ... F^rm_sm) are from F^i_j and are the result of a chain
 203   // of predicate resolution steps on the clauses i1 to in. This rule is used
 204   // when the resolution step is not emitted by the SAT solver.
 205   TH_RESOLUTION,
 206   // ======== resolution
 207   // This rule is equivalent to the th_resolution rule but is emitted by the SAT
 208   // solver.
 209   RESOLUTION,
 210   // ======== refl
 211   // G > i. (= F1 F2)
 212   REFL,
 213   // ======== trans
 214   // G > i. (= F1 F2)
 215   // ...
 216   // G > j. (= F2 F3)
 217   // ...
 218   // G > k. (= F1 F3)
 219   TRANS,
 220   // ======== cong
 221   // G > i1. (= F1 G1)
 222   // ...
 223   // G > in. (= Fn Gn)
 224   // ...
 225   // G > j. (= (f F1 ... Fn) (f G1 ... Gn))
 226   // where f is an n-ary function symbol.
 227   CONG,
 228   // ======== and
 229   // > i. (and F1 ... Fn)
 230   // ...
 231   // > j. Fi
 232   AND,
 233   // ======== tautologic_clause
 234   // > i. (cl F1 ... Fi ... Fj ... Fn)
 235   // ...
 236   // > j. true
 237   // where Fi != Fj
 238   TAUTOLOGIC_CLAUSE,
 239   // ======== not_or
 240   // > i. (not (or F1 ... Fn))
 241   // ...
 242   // > j. (not Fi)
 243   NOT_OR,
 244   // ======== or
 245   // > i. (or F1 ... Fn)
 246   // ...
 247   // > j. (cl F1 ... Fn)
 248   OR,
 249   // ======== not_and
 250   // > i. (not (and F1 ... Fn))
 251   // ...
 252   // > j. (cl (not F1) ... (not Fn))
 253   NOT_AND,
 254   // ======== xor1
 255   // > i. (xor F1 F2)
 256   // ...
 257   // > j. (cl F1 F2)
 258   XOR1,
 259   // ======== xor2
 260   // > i. (xor F1 F2)
 261   // ...
 262   // > j. (cl (not F1) (not F2))
 263   XOR2,
 264   // ======== not_xor1
 265   // > i. (not (xor F1 F2))
 266   // ...
 267   // > j. (cl F1 (not F2))
 268   NOT_XOR1,
 269   // ======== not_xor2
 270   // > i. (not (xor F1 F2))
 271   // ...
 272   // > j. (cl (not F1) F2)
 273   NOT_XOR2,
 274   // ======== implies
 275   // > i. (=> F1 F2)
 276   // ...
 277   // > j. (cl (not F1) F2)
 278   IMPLIES,
 279   // ======== not_implies1
 280   // > i. (not (=> F1 F2))
 281   // ...
 282   // > j. (not F2)
 283   NOT_IMPLIES1,
 284   // ======== not_implies2
 285   // > i. (not (=> F1 F2))
 286   // ...
 287   // > j. (not F2)
 288   NOT_IMPLIES2,
 289   // ======== equiv1
 290   // > i. (= F1 F2)
 291   // ...
 292   // > j. (cl (not F1) F2)
 293   EQUIV1,
 294   // ======== equiv2
 295   // > i. (= F1 F2)
 296   // ...
 297   // > j. (cl F1 (not F2))
 298   EQUIV2,
 299   // ======== not_equiv1
 300   // > i. (not (= F1 F2))
 301   // ...
 302   // > j. (cl F1 F2)
 303   NOT_EQUIV1,
 304   // ======== not_equiv2
 305   // > i. (not (= F1 F2))
 306   // ...
 307   // > j. (cl (not F1) (not F2))
 308   NOT_EQUIV2,
 309   // ======== ite1
 310   // > i. (ite F1 F2 F3)
 311   // ...
 312   // > j. (cl F1 F3)
 313   ITE1,
 314   // ======== ite2
 315   // > i. (ite F1 F2 F3)
 316   // ...
 317   // > j. (cl (not F1) F2)
 318   ITE2,
 319   // ======== not_ite1
 320   // > i. (not (ite F1 F2 F3))
 321   // ...
 322   // > j. (cl F1 (not F3))
 323   NOT_ITE1,
 324   // ======== not_ite2
 325   // > i. (not (ite F1 F2 F3))
 326   // ...
 327   // > j. (cl (not F1) (not F3))
 328   NOT_ITE2,
 329   // ======== ite_intro
 330   // > i. (= F (and F F1 ... Fn))
 331   // where F contains the ite operator. Let G1,...,Gn be the terms starting with
 332   // ite, i.e. Gi := (ite Fi Hi Hi'), then Fi = (ite Fi (= Gi Hi) (= Gi Hi')) if
 333   // Hi is of sort Bool
 334   ITE_INTRO,
 335   // ======== duplicated_literals
 336   // > i. (cl F1 ... Fn)
 337   // ...
 338   // > j. (cl Fk1 ... Fkm)
 339   // where m <= n and k1,...,km is a monotonic map to 1,...,n such that Fk1 ...
 340   // Fkm are pairwise distinct and {F1,...,Fn} = {Fk1 ... Fkm}
 341   DUPLICATED_LITERALS,
 342   // ======== connective_def
 343   //  G > i. (= (xor F1 F2) (or (and (not F1) F2) (and F1 (not F2))))
 344   // or
 345   //  G > i. (= (= F1 F2) (and (=> F1 F2) (=> F2 F1)))
 346   // or
 347   //  G > i. (= (ite F1 F2 F3) (and (=> F1 F2) (=> (not F1) (not F3))))
 348   CONNECTIVE_DEF,
 349   // ======== Simplify rules
 350   // The following rules are simplifying rules introduced as tautologies that can be
 351   // verified by a number of simple transformations
 352   ITE_SIMPLIFY,
 353   EQ_SIMPLIFY,
 354   AND_SIMPLIFY,
 355   OR_SIMPLIFY,
 356   NOT_SIMPLIFY,
 357   IMPLIES_SIMPLIFY,
 358   EQUIV_SIMPLIFY,
 359   BOOL_SIMPLIFY,
 360   QUANTIFIER_SIMPLIFY,
 361   DIV_SIMPLIFY,
 362   PROD_SIMPLIFY,
 363   UNARY_MINUS_SIMPLIFY,
 364   MINUS_SIMPLIFY,
 365   SUM_SIMPLIFY,
 366   COMP_SIMPLIFY,
 367   NARY_ELIM,
 368   QNT_SIMPLIFY,
 369   // ======== let
 370   // G,x1->F1,...,xn->Fn > j. (= G G')
 371   // ---------------------------------
 372   // G > k. (= (let (x1 := F1,...,xn := Fn.G) G')
 373   LET,
 374   // ======== sko_ex
 375   // G,x1->(e x1.F),...,xn->(e xn.F) > j. (= F G)
 376   // --------------------------------------------
 377   // G > k. (exists (x1 ... xn) (= F G))
 378   SKO_EX,
 379   // ======== sko_forall
 380   // G,x1->(e x1.(not F)),...,xn->(e xn.(not F)) > j. (= F G)
 381   // --------------------------------------------------------
 382   // G > k. (forall (x1 ... xn) (= F G))
 383   SKO_FORALL,
 384   // ======== symm
 385   // > i. (= F G)
 386   // ...
 387   // > j. (= G F)
 388   SYMM,
 389   // ======== not_symm
 390   // > i. (not (= F G))
 391   // ...
 392   // > j. (not (= G F))
 393   NOT_SYMM,
 394   // ======== reorder
 395   // > i1. F1
 396   // ...
 397   // > j. F2
 398   // where set representation of F1 and F2 are the same and the number of
 399   // literals in C2 is the same of that of C1.
 400   REORDER,
 401   // ======== undefined
 402   // Used in case that a step in the proof rule could not be translated.
 403   UNDEFINED
 404 };
 405
 406 /**
 407  * Converts an Alethe proof rule to a string.
 408  *
 409  * @param id The Alethe proof rule
 410  * @return The name of the Alethe proof rule
 411  */
 412 const char* aletheRuleToString(AletheRule id);
 413
 414 /**
 415  * Writes an Alethe proof rule name to a stream.
 416  *
 417  * @param out The stream to write to
 418  * @param id The Alethe proof rule to write to the stream
 419  * @return The stream
 420  */
 421 std::ostream& operator<<(std::ostream& out, AletheRule id);
 422
 423 }  // namespace proof
 424
 425 }  // namespace cvc5
 426
 427 #endif /* CVC4__PROOF__ALETHE_PROOF_RULE_H */