Seventy-five problems for testing automatic theorem provers

BledsoeW., BoyerR., and HennemanW. (1972) ‘Computer proofs of limit theorems’,Artificial Intelligence,3, 27–60.

CookS. and ReckhowR. (1979) ‘The relative efficiency of propositional proof systems’,J. Symbolic Logic 44, 36–50.

DeChampeauxD. (1979) ‘Sub-problem finder and instance checker: two cooperating preprocessors for theorem provers’IJCAI 6, 191–196.

GalilZ. (1977) ‘On resolution with clauses of bounded size’,SIAM J. Computing 6, 444–459.

Kalish, D. & Montague, R. (1964)Logic: Techniques of Formal Reasoning, World, Harcourt & Brace,

LuskE. and OverbeekR. (1985) ‘Reasoning about equality’,J. Automated Reasoning,1, 209–228.

McCharenR., OverbeekR., & WosL. (1976) ‘Problems and experiments for and with automated theorem-proving programs’,IEEE Trans. Computers C-25(8), 773–782.

McCuneW. (1985) ‘Schubert's Steamroller Problem with linked UR-resolution’Assoc. Automated Reasoning Newsletter,4, 4–6.

MontagueR. (1955) ‘On the paradox of grounded classes’J. Symbolic Logic 20, 140.

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).

NewellA. and SimonH. (1972)Human Problem Solving, (Prentice-Hall, Englewood Cliffs).

PelletierF. J. (1982) ‘Completely nonclausal, completely heuristically driven automatic theorem proving’, Technical Report TR82-7, (Dept. of Computing Science, Edmonton, Alberta).

PelletierF. J. (1985) ‘Six problems in translational equivalence’,Logique et Analyse 108, 423–434.

SiklóssyL., RichA., and MarinovV. (1973) ‘Breadth first search: some surprising results’,Artificial Intelligence 4, 1–27.

StickelM. (1986) ‘Schubert's steamroller problem: formulations and solutions’,J. Automated Reasoning 2, 89–104.

ThomasonR. (1972)Symbolic Logic (Prentice-Hall, Englewood Cliffs).

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).

Urquhart, A. (unpublished a) ‘The complexity of Genzen systems for propositional logic’.

Urquhart, A. (unpublished b) ‘Hard examples for resolution’.

WaltherC. (1985) ‘A mechanical solution of Schubert's steamroller by many-sorted resolution’,Artificial Intelligence 26, 217–224.

WhiteheadA. and RussellB. (1910)Principia Mathematica, Vol. I. (Cambridge UP, Cambridge).