projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f767e82) | patch
[proofs] Alethe: Translate AND_INTRO rule (#7405)
authorLachnitt <lachnitt@stanford.edu>
Tue, 26 Oct 2021 14:00:55 +0000 (07:00 -0700)
committerGitHub <noreply@github.com>
Tue, 26 Oct 2021 14:00:55 +0000 (14:00 +0000)
commit8995119775293b5b3e618701d2e4e318f18e5fed
treecc80a2e1bd0f3c5b3fdd964b4f1cd0524d3ca6eetree
parentf767e820881e57fd315616efa2a1817110758e93commit | diff
[proofs] Alethe: Translate AND_INTRO rule (#7405)

Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus.

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