Package: areas/reasonng/atp/problems/atp/
CMU Artificial Intelligence Repository
ATP Problem Library
areas/reasonng/atp/problems/atp/
This directory contains a collection of ATP problems from Otter, CADE,
and JAR. They may be used to testing and benchmarking theorem provers.
The problems include algebra, analysis, circuits, geometry, logic
problems, Pelletier's problem set, program verification, puzzles, set
theory, and topology. The problems are given in the form of Otter
input files.
Origin:
anagram.mcs.anl.gov:/pub/ATP_Problems/*
CD-ROM: Prime Time Freeware for AI, Issue 1-1
Author(s): W.W. Bledsoe, Charles Morgan, Hao Wang, Lewis Carroll,
Raymond Smullyan, B. Mitchell, Dana Scott, E.L. Marsden,
Francis Jeffrey Pelletier, Cynthia Wick, William McCune,
R. Boyer, E. Lusk, R. Overbeek, M. Stickel, L. Wos,
McCharen, and Quaife
Keywords:
Algebra, Analysis, Authors!Bledsoe, Authors!Boyer,
Authors!Carroll, Authors!Lusk, Authors!Marsden,
Authors!McCharen, Authors!McCune, Authors!Mitchell,
Authors!Morgan, Authors!Overbeek, Authors!Pelletier,
Authors!Quaife, Authors!Scott, Authors!Smullyan,
Authors!Stickel, Authors!Wang, Authors!Wick, Authors!Wos,
Automated Reasoning!Problem Libraries, Boolean Algebra, CADE,
Category Theory, Circuit Design and Validation,
Equivalential Calculus, Geometry, Godel's Set Theory Axions,
Group Theory, Henkin Models, JAR, Limit Theorems,
Logic Problems, Modular Lattices, OTTER,
Pelletier's Problem Set, Program Verification, Puzzles,
Reasoning!Automated Reasoning, Relevance Logic, Ring Theory,
Set Theory, Taskian Geometry, Test Problems,
Theorem Proving!Problem Libraries, Topology
References:
McCharen, Overbeek, & Wos, "Problems and Experiments for and with
Automated Theorem-Proving Programs", [Aug.1976]
B. Mitchell, "Theory of Categories", Chapter 1, [1965].
Dana Scott, "Identity & Existence in Intuitionist Logic", [1978].
E.L. Marsden, "A Note on Implicative Models", Notices of the American
Mathematical Society, January 1971.
Quaife, "Automated Development of Tarski's Geometry", Journal of
Automated Reasoning 5:97-118, 1989.
Francis Jeffrey Pelletier, "Seventy-Five Problems for Testing
Automatic Theorem Provers", Journal of Automated Reasoning Vol. 2 #2,
pp. 191-216, 1986. [Errata: J. Automated Reasoning Vol. 4 #2, pp.
235-236, June 1988].
Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., & Wos, L.
1986. "Set Theory in First-Order Logic: Clauses for Godel's Axioms".
Journal of Automated Reasoning 2: 287-327.
Cynthia Wick and William McCune (Aug. 1988); reference "Automated
Reasoning about Elementary Point-Set Topology", J. Automated Reasoning
5: 239-255 (1989).
Last Web update on Mon Feb 13 10:27:25 1995
AI.Repository@cs.cmu.edu