projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 85f57e1) | patch
[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)
authorLachnitt <lachnitt@stanford.edu>
Mon, 25 Oct 2021 21:23:48 +0000 (14:23 -0700)
committerGitHub <noreply@github.com>
Mon, 25 Oct 2021 21:23:48 +0000 (21:23 +0000)
commit2aaa6ec1dfc3d7a41f120ef5361272b63363347b
treeae75c7ae19ac18b26d9cb00d007c2c83d77e0070tree
parent85f57e1b106e0c91ef73a51ff3ad5194d6634b60commit | diff
[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)

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