ILF-SETHEO

DOI10.1007/3-540-63104-6_8zbMath1430.68426OpenAlexW4233433372MaRDI QIDQ5234690

Andreas Wolf, Johann Schumann

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_8

zbMATH Keywords

natural deductionproof treetheorem provermodel eliminationinteractive theorem prover

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

ILF-SETHEO, Automatic verification of cryptographic protocols with SETHEO

Uses Software

• SETHEO
• TPTP
• KoMeT

Cites Work

• Unnamed Item
• Unnamed Item
• Set theory in first-order logic: Clauses for Gödel's axioms
• SETHEO: A high-performance theorem prover
• Controlled integration of the cut rule into connection tableau calculi
• Untersuchungen über das logische Schliessen. I
• The TPTP problem library
• Reconstructing proofs at the assertion level
• KoMeT
• Integration of automated and interactive theorem proving in ILF
• Automatic verification of cryptographic protocols with SETHEO