projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e283d0f) | patch
[proofs] Alethe: Translate FACTORING rule (#7398)
authorLachnitt <lachnitt@stanford.edu>
Fri, 22 Oct 2021 19:00:52 +0000 (12:00 -0700)
committerGitHub <noreply@github.com>
Fri, 22 Oct 2021 19:00:52 +0000 (19:00 +0000)
commitb3774c9758b6a23c8ef5d98eaa0879a814114674
tree108884675af0a7d17e89d69269b602a64ee97a53tree
parente283d0fb1c09cd482f8483a138d697720cf69ed2commit | diff
[proofs] Alethe: Translate FACTORING rule (#7398)

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

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