Cited in
(19)- Herbrand constructivization for automated intuitionistic theorem proving
- Scalable fine-grained proofs for formula processing
- Certification of nonclausal connection tableaux proofs
- Understanding Resolution Proofs through Herbrand’s Theorem
- On the generation of quantified lemmas
- The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
- SQEMA
- CERES
- Quati
- TIP
- ProofTool
- Scavenger
- Psyche
- Slakje
- WhaleProver
- Complexity of translations from resolution to sequent calculus
- The problem of \(\Pi_{2}\)-cut-introduction
- Sequoia
- Extraction of expansion trees
This page was built for software: GAPT
