×

zbMATH — the first resource for mathematics

Seventy-five problems for testing automatic theorem provers. (English) Zbl 0642.68147

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] BledsoeW., BoyerR., and HennemanW. (1972) ’Computer proofs of limit theorems’,Artificial Intelligence,3, 27–60. · Zbl 0242.68055 · doi:10.1016/0004-3702(72)90041-0
[2] CookS. and ReckhowR. (1979) ’The relative efficiency of propositional proof systems’,J. Symbolic Logic 44, 36–50. · Zbl 0408.03044 · doi:10.2307/2273702
[3] DeChampeauxD. (1979) ’Sub-problem finder and instance checker: two cooperating preprocessors for theorem provers’IJCAI 6, 191–196.
[4] GalilZ. (1977) ’On resolution with clauses of bounded size’,SIAM J. Computing 6, 444–459. · Zbl 0368.68085 · doi:10.1137/0206031
[5] Kalish, D. & Montague, R. (1964)Logic: Techniques of Formal Reasoning, World, Harcourt & Brace, · Zbl 0166.00105
[6] LuskE. and OverbeekR. (1985) ’Reasoning about equality’,J. Automated Reasoning,1, 209–228.
[7] McCharenR., OverbeekR., & WosL. (1976) ’Problems and experiments for and with automated theorem-proving programs’,IEEE Trans. Computers C-25(8), 773–782. · Zbl 0329.68075 · doi:10.1109/TC.1976.1674696
[8] McCuneW. (1985) ’Schubert’s Steamroller Problem with linked UR-resolution’Assoc. Automated Reasoning Newsletter,4, 4–6.
[9] MontagueR. (1955) ’On the paradox of grounded classes’J. Symbolic Logic 20, 140. · Zbl 0068.24702 · doi:10.2307/2266899
[10] NewellA., ShawJ., and SimonH. (1957) ’Empirical explorations with the logic theory machine: a case study in heuristics’. Reprinted in E.Feigenbaum and J.Feldman (eds.)Computers and Thought (McGraw-Hill, N.Y.) pp. 279–293 (1963).
[11] NewellA. and SimonH. (1972)Human Problem Solving, (Prentice-Hall, Englewood Cliffs).
[12] PelletierF. J. (1982) ’Completely nonclausal, completely heuristically driven automatic theorem proving’, Technical Report TR82-7, (Dept. of Computing Science, Edmonton, Alberta).
[13] PelletierF. J. (1985) ’Six problems in translational equivalence’,Logique et Analyse 108, 423–434.
[14] Sikl√≥ssyL., RichA., and MarinovV. (1973) ’Breadth first search: some surprising results’,Artificial Intelligence 4, 1–27. · Zbl 0258.68048 · doi:10.1016/0004-3702(73)90006-4
[15] StickelM. (1986) ’Schubert’s steamroller problem: formulations and solutions’,J. Automated Reasoning 2, 89–104. · Zbl 0642.68164 · doi:10.1007/BF00246025
[16] ThomasonR. (1972)Symbolic Logic (Prentice-Hall, Englewood Cliffs).
[17] TseitinG. S. (1968) ’On the complexity of derivation in propositional calculus’, reprinted in J.Siekmann and G.Wrightson (eds.)Automation of Reasoning (Springer-Verlag, Berlin).
[18] Urquhart, A. (unpublished a) ’The complexity of Genzen systems for propositional logic’. · Zbl 0688.03039
[19] Urquhart, A. (unpublished b) ’Hard examples for resolution’. · Zbl 0639.68093
[20] WaltherC. (1985) ’A mechanical solution of Schubert’s steamroller by many-sorted resolution’,Artificial Intelligence 26, 217–224. · Zbl 0569.68076 · doi:10.1016/0004-3702(85)90029-3
[21] WhiteheadA. and RussellB. (1910)Principia Mathematica, Vol. I. (Cambridge UP, Cambridge).
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.