Evaluating general purpose automated theorem proving systems

DOI10.1016/S0004-3702(01)00113-8MaRDI QIDQ1606324zbMATH OpenFDO

Authors Geoff Sutcliffe, Christian Suttner

Publication date 24 July 2002

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0004-3702(01)00113-8

zbMATH Keywords

ATP systems

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 3881899
• scientific article; zbMATH DE number 1100750
• Evaluation of automated theorem proving on the Mizar mathematical library
• An Evaluation Based Theorem Prover
• Another look at automated theorem-proving
• Automated theorem proving methods
• scientific article; zbMATH DE number 49488
• scientific article; zbMATH DE number 4043814
• Publication:3034850
• Automatic theorem proving for three decades

Cites work

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

Cited in

(19)

• A domain-specific language for cryptographic protocols based on streams
• Automated verification of refinement laws
• 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
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• MaLeS: a framework for automatic tuning of automated theorem provers
• Cooperating proof attempts
• Playing with AVATAR
• On Automating the Calculus of Relations
• An Evaluation Based Theorem Prover
• The 10th IJCAR automated theorem proving system competition -- CASC-J10
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• The 9th IJCAR automated theorem proving system competition -- CASC-J9
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• Investigations into proof structures
• The dependently typed higher-order form for the TPTP world
• An empirical assessment of progress in automated theorem proving
• Stepping stones in the TPTP world
• Filter-based resolution principle for lattice-valued propositional logic LP(X)

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1606324)