Herbrand constructivization for automated intuitionistic theorem proving

DOI10.1007/978-3-030-29026-9_20zbMath1435.68364OpenAlexW2969536091MaRDI QIDQ2180528

Gabriel Ebner

Publication date: 14 May 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-29026-9_20

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ Slakje

Uses Software

• Coq
• ILTP
• Isabelle/HOL
• VAMPIRE
• SPASS
• TPTP
• Prover9
• Mace4
• Sat4j
• Agda
• leanCoP
• E Theorem Prover
• Lean
• GAPT
• ProofTool
• AVATAR
• WhaleProver

This page was built for publication: Herbrand constructivization for automated intuitionistic theorem proving