projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 446185d) | patch
[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)
authorLachnitt <lachnitt@stanford.edu>
Tue, 26 Oct 2021 11:46:26 +0000 (04:46 -0700)
committerGitHub <noreply@github.com>
Tue, 26 Oct 2021 11:46:26 +0000 (11:46 +0000)
commit3735b033da730f532de39af4c069f3a0d00e6484
treeb500021a1e5f156c740a15aaa142cd16c1321623tree
parent446185d47831197312d6a95fc78a89ce4bbe6f9ccommit | diff
[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)

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

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