projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d1397cb) | patch
[proofs] Alethe: Translate Further Equality rules (#7606)
authorLachnitt <lachnitt@stanford.edu>
Tue, 9 Nov 2021 22:37:35 +0000 (14:37 -0800)
committerGitHub <noreply@github.com>
Tue, 9 Nov 2021 22:37:35 +0000 (22:37 +0000)
commitf826638031ae919a03bd48c2003eed82cea7279a
tree3298bd5a4e6b8c1df7f4da149086022bd8b7f09etree
parentd1397cb10bdbd45d3e40f64111408b9a7f0e0cf4commit | diff
[proofs] Alethe: Translate Further Equality rules (#7606)

Implementation of the translation of FALSE_INTRO, FALSE_ELIM, TRUE_INTRO and TRUE_ELIM rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
src/proof/alethe/alethe_post_processor.cpp diff | blob | history