summaryrefslogtreecommitdiff
path: root/src/expr/proof_rule.cpp
AgeCommit message (Expand)Author
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-10(proof-new) Replace witness form by original form in the internal proof calcu...Andrew Reynolds
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-02-23Add proof for mult sign lemma (#5966)Gereon Kremer
2021-02-23Add proof for monomial bounds check (#5965)Gereon Kremer
2021-02-23(proof-new) Add proof generator for CAD solver (#5964)Gereon Kremer
2021-02-22Add trans secant proofs. (#5957)Gereon Kremer
2021-02-22(proof-new) Add proofs for exponential functions (#5956)Gereon Kremer
2021-02-22(proof-new) Add proofs for sine lemmas in the transcendental solver (#5952)Gereon Kremer
2021-02-02(proof-new) Miscellaneous fixes and regressions (#5841)Andrew Reynolds
2020-12-21Add proof for pi bound lemma (#5709)Gereon Kremer
2020-12-21Add proof for sine shift lemmas. (#5710)Gereon Kremer
2020-12-18(proof-new) Add proof for tangent plane lemmas (#5700)Gereon Kremer
2020-12-07Add support for BV proofs with the simple bitblasting solver. (#5603)Mathias Preiner
2020-12-02(proof-new) Proofs for expand definitions (#5562)Andrew Reynolds
2020-10-26(proof-new) Add datatypes proof checker (#5340)Andrew Reynolds
2020-10-18(proof-new) Implementation of trust substitution (#5276)Andrew Reynolds
2020-10-13(proof-new) New rules for Booleans (#5243)Andrew Reynolds
2020-10-08(proof-new) Fixes and improvements for smt proof postprocessor (#5197)Andrew Reynolds
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-21(proof-new) Add the arrays proof checker (#5047)Andrew Reynolds
2020-09-16[proof-new] Resolution rules and checkers (#5070)Haniel Barbosa
2020-09-02(proof-new) Updates to builtin proof checker (#4962)Andrew Reynolds
2020-09-02(proof-new) Add proof support in TheoryUF (#5002)Andrew Reynolds
2020-08-18(proof-new) Theory preprocessor proof producing (#4807)Andrew Reynolds
2020-08-15(proof-new) Add the strings proof checker (#4858)Andrew Reynolds
2020-08-12(proof-new) Improve interfaces to proof generators (#4803)Andrew Reynolds
2020-08-12(proof-new) Witness form proof generator (#4782)Andrew Reynolds
2020-07-27(proof-new) Proof production for term formula removal (#4687)Andrew Reynolds
2020-07-17(proof-new) Updates to strings core solver (#4642)Andrew Reynolds
2020-07-14(proof-new) Skeleton proof support in the Rewriter (#4730)Andrew Reynolds
2020-07-13 (proof-new) SMT Preprocess proof generator (#4708)Andrew Reynolds
2020-06-28Proof Rules and Checker for Arithmetic (#4665)Alex Ozdemir
2020-06-16Update copyright headers.Aina Niemetz
2020-06-15(proof-new) Add quantifiers proof checker (#4593)Andrew Reynolds
2020-06-03(proof-new) Adding rules and proof checker for EUF (#4559)Haniel Barbosa
2020-06-03(proof-new) Adding rules and proof checker for Boolean reasoning (#4560)Haniel Barbosa
2020-06-03(proof-new) Add builtin proof checker (#4537)Andrew Reynolds
2020-04-20Add SCOPE proof rule (#4332)Andrew Reynolds
2020-04-15Add ProofNode data structure (#4311)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback