Integration of automated and interactive theorem proving in ILF

DOI10.1007/3-540-63104-6_7zbMath1430.68397OpenAlexW1587902436MaRDI QIDQ5234689

Bernd I. Dahn, Jürgen Gehne, Th. Honigmann, Andreas Wolf

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_7

zbMATH Keywords

automated theorem provertheorem proverpolymorphic typeproof presentationbackground system

Mathematics Subject Classification ID

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

Related Items (6)

ILF-SETHEO ⋮ Converting non-classical matrix proofs into sequent-style systems ⋮ Controlled use of clausal lemmas in connection tableau calculi ⋮ Integration of automated and interactive theorem proving in ILF ⋮ Extending Sledgehammer with SMT solvers ⋮ Evaluating general purpose automated theorem proving systems

Uses Software

• SETHEO
• OTTER
• SPASS
• TPTP
• DISCOUNT
• KoMeT
• FLOTTER

Cites Work

• Unnamed Item
• Unnamed Item
• SPASS & FLOTTER version 0.42
• The TPTP problem library
• KoMeT
• Integration of automated and interactive theorem proving in ILF

This page was built for publication: Integration of automated and interactive theorem proving in ILF