×

zbMATH — the first resource for mathematics

Evaluating general purpose automated theorem proving systems. (English) Zbl 0996.68182
Summary: A key concern of ATP research is the development of more powerful systems, capable of solving more difficult problems within the same resource limits. In order to build more powerful systems, it is important to understand which systems, and hence which techniques, work well for what types of problems. This paper deals with the empirical evaluation of general purpose ATP systems, to determine which systems work well for what types of problems. This requires also dealing with the issues of assigning ATP problems into classes that are reasonably homogeneous with respect to the ATP systems that (attempt to) solve the problems, and assigning ratings to problems based on their difficulty.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Keywords:
ATP systems
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Astrachan, O.L.; Loveland, D.W., Measuring the performance of automated theorem provers, (), 37-41 · Zbl 0882.68132
[2] Bauer, A.; Clarke, E., Analytica—an experiment in combining theorem proving and symbolic computation, J. automat. reason., 21, 3, 295-325, (1998) · Zbl 0916.68143
[3] Barras, B.; Boutin, S.; Cornes, C.; Courant, J.; Filliatre, J.C.; Giménez, E.; Herbelin, H.; Huet, G.; Muñoz, C.; Murthy, C.; Parent, C.; Paulin, C.; Saı̈bi, A.; Werner, B., The COQ proof assistant reference manual—version 6.1, (1997), Research Report 0203, INRIA Nancy, France
[4] Benzmüller, C.; Cheikhrouhou, L.; Fehrer, D.; Fiedler, A.; Huang, X.; Kerber, M.; Kohlhase, M.; Konrad, K.; Meier, A.; Melis, E.; Schaarschmidt, W.; Siekmann, J.; Sorge, V., OMEGA: towards a mathematical assistant, (), 146-160
[5] Dahn, B.I.; Gehne, J.; Honigmann, T.; Wolf, A., Integration of automated and interactive theorem proving, (), 57-60
[6] DeNivelle, H., Bliksem 1.00, (), 9
[7] Dunker, U., Search space and proof complexity of theorem proving strategies, ()
[8] Feynmann, R.; Leighton, R., Cargo cult science, (), 338-346
[9] Fuchs, D.; Fuchs, M., Code: A powerful prover for problems of condensed detachment, (), 260-263
[10] Gordon, M.; Melham, T., Introduction to HOL, a theorem proving environment for higher order logic, (1993), Cambridge University Press · Zbl 0779.68007
[11] Hanks, S.; Pollack, M.E.; Cohen, P.R., Benchmarks, test beds, controlled experimentation and the design of agent architectures, AI magazine, 14, 4, 17-42, (1993)
[12] Hooker, J.N., Testing heuristics: we have it all wrong, J. heuristics, 1, 33-42, (1996) · Zbl 0853.68155
[13] Johnson, D.S., A Theoretician’s guide to the experimental analysis of algorithms, (1996), Draft available by ftp from: dimacs.rutgers.edu:pub/dsj/temp/exper.ps
[14] Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W., SETHEO: A high-performance theorem prover, J. automat. reason., 8, 2, 183-212, (1992) · Zbl 0759.68080
[15] Letz, R., On the polynomial transparency of resolution, (), 123-129
[16] McCune, W.W., Otter 3.0 reference manual and guide, (1994), Technical Report ANL-94/6, Argonne National Laboratory Argonne, IL
[17] McCune, W.W., Solution of the robbins problem, J. automat. reason., 19, 3, 263-276, (1997) · Zbl 0883.06011
[18] McCune, W.W., EQP: equational prover, (2000), http://www-unix.mcs.anl.gov/AR/eqp/
[19] Paulson, L.C.; Nipkow, T., Isabelle: A generic theorem prover, Lecture notes in computer science, 828, (1994), Springer Berlin
[20] Plaisted, D.A., The search efficiency of theorem proving strategies, (), 57-71
[21] Reif, W., The KIV-approach to software verification, ()
[22] Schulz, S., System abstract: E 0.3, (), 297-301
[23] Sutcliffe, G.; Seyfang, D., Smart selective competition parallelism ATP, (), 341-345
[24] Sutcliffe, G.; Suttner, C., Special issue: the CADE-13 ATP system competition, J. automat. reason., 18, 2, (1997)
[25] Sutcliffe, G.; Suttner, C., ATP system results for the TPTP problem library, (1997), http://www.cs.jcu.edu.au/ tptp/TPTP/Results.html
[26] Sutcliffe, G.; Suttner, C., The TPTP problem library: CNF release v1.2.1, J. automat. reason., 21, 2, 177-203, (1998) · Zbl 0910.68197
[27] Sutcliffe, G.; Suttner, C., The CADE-15 ATP system competition, J. automat. reason., 23, 1, 1-23, (1999)
[28] Sutcliffe, G., The CADE-16 ATP system competition, J. automat. reason., 24, 3, 371-396, (2000) · Zbl 0953.68595
[29] Suttner, C.; Sutcliffe, G., The CADE-14 ATP system competition, J. automat. reason., 21, 1, 99-134, (1998) · Zbl 0916.68141
[30] Tammet, T., Gandalf, J. automat. reason., 18, 2, 199-204, (1997)
[31] Voronkov, A., The anatomy of vampire, J. automat. reason., 15, 2, 237-265, (1995) · Zbl 0838.68100
[32] Weidenbach, C.; Afshordel, B.; Brahm, U.; Cohrs, C.; Engel, T.; Keen, E.; Theobalt, C.; Tpoic, D., System description: SPASS version 1.0.0, (), 378-382
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.