Evaluating general purpose automated theorem proving systems

DOI10.1016/S0004-3702(01)00113-8zbMath0996.68182MaRDI QIDQ1606324

Christian Suttner, Geoff Sutcliffe

Publication date: 24 July 2002

Published in: Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

ATP systems

Mathematics Subject Classification ID

Related Items (14)

MaLeS: a framework for automatic tuning of automated theorem provers ⋮ Cooperating Proof Attempts ⋮ Playing with AVATAR ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) ⋮ The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ Theorem prover for intuitionistic logic based on the inverse method ⋮ On Automating the Calculus of Relations ⋮ The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 ⋮ A domain-specific language for cryptographic protocols based on streams ⋮ Automated verification of refinement laws ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10

Uses Software

• Coq
• Isabelle
• SETHEO
• ML
• OTTER
• VAMPIRE
• SPASS
• TPTP
• HOL
• Analytica
• CoDe

Cites Work

• Unnamed Item
• SETHEO: A high-performance theorem prover
• The CADE-14 ATP system competition
• Analytica --- an experiment in combining theorem proving and symbolic computation
• The TPTP problem library. CNF release v1. 2. 1
• Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
• Isabelle. A generic theorem prover
• The use of lemmas in the model elimination procedure
• Solution of the Robbins problem
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• Testing heuristics: We have it all wrong
• The CADE-16 ATP system competition
• The search efficiency of theorem proving strategies
• Integration of automated and interactive theorem proving in ILF
• CODE: A powerful prover for problems of condensed detachment

This page was built for publication: Evaluating general purpose automated theorem proving systems