projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5e2ee54) | patch
[proofs] Alethe: Translate INSTANTIATE rule (#7607)
authorLachnitt <lachnitt@stanford.edu>
Wed, 10 Nov 2021 12:16:55 +0000 (04:16 -0800)
committerGitHub <noreply@github.com>
Wed, 10 Nov 2021 12:16:55 +0000 (12:16 +0000)
commit9f8d59391ecf0272db184624e4e44ee13241c6bd
tree1fc1e40f3461b99e9bd54b751ad73325630b694atree
parent5e2ee546fed4ca999f933e2e50938110d221f044commit | diff
[proofs] Alethe: Translate INSTANTIATE rule  (#7607)

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

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