projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0b7b6fb) | patch
[proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397)
authorLachnitt <lachnitt@stanford.edu>
Fri, 22 Oct 2021 18:38:47 +0000 (11:38 -0700)
committerGitHub <noreply@github.com>
Fri, 22 Oct 2021 18:38:47 +0000 (18:38 +0000)
commite283d0fb1c09cd482f8483a138d697720cf69ed2
tree42deefde0cf29b961d21ae63996526c8f6d8ca09tree
parent0b7b6fb608a897bf50861ce5a4c25e74c9245f01commit | diff
[proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397)

Implementation of the translation of RESOLUTION and CHAIN_RESOLUTION rules into the Alethe calculus.

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