Bibliography of Instance-Based Theorem Proving

David A. Plaisted

Here is a full (I think) bibliography of work on instance-based theorem proving methods. The idea of instance-based theorem proving is to show that a set S of first-order clauses is unsatisfiable by constructing a set T of ground instances of clauses in S and testing T for unsatisfiability using an efficient propositional calculus decision procedure. This bibliography includes not only my own works, but several other papers by others which it turns out are closely related. In all, there are over 30 papers. Most of these are co-authored by me. If you know of other works in this area, I would like to know about them. Though instance-based theorem proving may not be as well known as other approaches, it is noteworthy that instance-based theorem proving methods often far outperform other strategies, even when implemented in Prolog. In addition to the following references, another paper of mine about the use of this approach for set theory problems is forthcoming, and instance-based theorem proving also far outperforms resolution for certain set theory problems, without any human guidance. Finally, I have developed another extension of clause linking which has not been written up, which should have significant advantages on many applications.

A survey of our work on instance-based approaches, written about 1996:

Plaisted, D., The Use of Semantics in Instance-Based Proof Procedures,
available at http://www.cs.unc.edu/~plaisted/mi/mi-publications.html

The basic method of clause linking without semantics:

Inference by clause matching, with Shie-Jue Lee, in Intelligent
Systems, Z. Ras and M. Zemankova, eds. (Ellis Horwood, New York,
1990), pp. 200 - 235.

We show that it iss better than resolution and other methods on near
propositional problems and logic puzzles:

Eliminating duplication with the hyper-linking strategy, with Shie-Jue
Lee, Journal of Automated Reasoning 9:1 (1992) 25-42.

A general paper about clause linking without semantics:

Theorem proving using hyper-matching strategy, with S. Lee,
International Symposium on Methodologies for Intelligent Systems,
October, 1989, Charlotte, North Carolina, also appeared in
Methodologies for Intelligent Systems 4, Z. Ras, ed.  (North-Holland,
1989), pp. 467 - 476.

The model finding part of clause linking without semantics:

New applications of a fast propositional calculus decision procedure,
with Shie-Jue Lee, Proceedings of the 8th Biennial Conference of
Canadian Society for Computational Studies of Intelligence,
(CSCSI-90), University of Ottawa, Ottawa, Ontario, CANADA, May 23-25,
1990, pp. 204-211.

The use of replacement rules with clause linking:

Reasoning with predicate replacement, with Shie-Jue Lee, International
Symposium on Methodologies for Intelligent Systems, Knoxville,
Tennessee, October 24 - 26, 1990; also appeared in Methodologies for
Intelligent Systems 5, Z. Ras, M. Zemankova, and M. Emrich, eds.
(North-Holland, 1990), pp. 530 - 537.

A way to find some proofs faster in instance-based theorem proving
using unit resolution:

Searching for small proofs in automatic theorem proving, with Shie-Jue
Lee, Proceedings of National Computer Symposium, Chung-Li, Taiwan,
Dec. 18 - 19, 1991, pages 626-632.

Some refinements of clause linking:

Use of Unit Clauses and Clause Splitting in Automatic Deduction, with
Shie-Jue Lee, Proceedings for the 4th International Conference on
Computing and Information, Toronto, Ontario, Canada, May 28-30, 1992,
pages 228-232.  Editors: W.W.  Koczkodaj, P.E. Lauer, and A.A.
Toptsis.  IEEE Computer Society Press.

An extension of clause linking to equality (which didn't work very
well) based on Brand's modification method:

Proving equality theorems with hyper-linking, with Geoff Alexander,
system abstract, Eleventh International Conference on Automated
Deduction, Saratoga Springs, New York, June 16 - 18, 1992.

An invited survey of the work on clause linking with and without
semantics and its relation to conditional term-rewriting systems:

Conditional term rewriting and first-order theorem proving, invited
talk, with Geoff Alexander, Heng Chu, and Shie-Jue Lee, Third
International Workshop on Conditional Term-Rewriting Systems,
Pont-a`-Mousson, France, July 8-10, 1992, to appear in the final
proceedings.

Replacement rules with clause linking, which (with some guidance)
vastly outperforms resolution on many set theory and temporal logic
problems:

Use of replace rules in theorem proving, with Shie-Jue Lee, Methods of
Logic in Computer Science 1 (1994) 217-240.

Using instance based theorem proving to solve logic puzzles by
constructing models:

Problem solving by searching for models with a theorem prover,
with Shie-Jue Lee, Artificial Intelligence 69 (1994) 205-233.

Clause linking with semantics, which obtains some reasonably hard
theorems:

Model Finding Strategies in Semantically Guided Instance-Based Theorem
Proving, with Heng Chu, International Symposium on Methodologies for
Intelligent Systems (ISMIS '93), June 15-18, 1993, Norway.
Proceedings to be published by Springer-Verlag in Lecture Notes in
Artificial Intelligence.  See also:

Model finding in semantically guided instance-based theorem proving,
with Heng Chu, Fundamenta Informaticae 21:3 (1994) 221 - 235.

Clause linking with semantics, combined with a kind of resolution to
eliminate large literals:

Rough Resolution: A Refinement of Resolution to Remove Large Literals,
with Heng Chu, Eleventh National Conference on Artificial
Intelligence, Washington, DC, July 11 to July 16, 1993.

A method of using specialized decision procedures (constraints) and
incorporating semantics with clause linking:

Use of Presburger Formulae in Semantically Guided Theorem Proving,
with Heng Chu, Third International Symposium on Artificial Intelligence
and Mathematics, Fort Lauderdale, Florida, January 2-5, 1994.  (No
proceedings.)

The basic idea of semantic hyper-linking, an extension of clause
linking to use semantic information:

Semantically Guided First-Order Theorem Proving using Hyper-Linking,
with Heng Chu, Twelfth Conference on Automated Deduction, Nancy,
France, June 28 - July 1, 1994.

A search strategy for use with instance based theorem proving that
controls the consumption of storage:

Controlling the consumption of storage with sliding priority search
in a hyper-linking based theorem prover, with Shie-Jue Lee,
Computers and Artificial Intelligence 14:6 (1995) 563-578.

A brief overview of clause linking with semantics:

CLINS-S: A Semantically Guided First-Order Theorem Prover,
with Heng Chu, JAR 18(2).

A brief overview of The RRTP theorem prover, another instance-based
theorem prover based on replacement rules::

M. Paramasivam and David A. Plaisted, RRTP, A Replacement Rule Theorem
Prover, Journal of Automated Reasoning, 18(2) pp. 221-226, 1997.

A paper mostly about efficiency of propositional decision procedures,
which also has some information about clause linking:

Propositional Search Efficiency and First-Order Theorem Proving, with
Geoffrey D. Alexander, SATISFIABILITY PROBLEM: THEORY AND APPLICATIONS
(DIMACS Workshop March 11-13, 1996), Ding-Zhu Du, Jun Gu, and Panos
Pardalos, eds., (AMS, 1997, Providence, RI), pp. 335-350.

The RRTP theorem prover and its performance on an application
(description logics), where it often outperforms specialized methods:

M. Paramasivam and David A. Plaisted, Automated Deduction Techniques
for Classification in Description Logics, Journal of Automated
Reasoning 20(3), June, 1998, pp. 337-364.

An introduction to ordered semantic hyper-linking (OSHL), another
instance-based strategy which uses semantics and also has an efficient
equality mechanism:

Plaisted, D. and Yunshan Zhu, Ordered Semantic Hyper Linking,
Proceedings of Fourteenth National Conference on Artificial
Intelligence (AAAI97), July 27 - 31, 1997, Providence, Rhode Island

A more detailed paper about OSHL:

D. Plaisted and Y. Zhu, Ordered Semantic Hyper-Linking, Journal of
Automated Reasoning, to appear.

A book giving an asymptotic analysis of the complexity of many
theorem proving strategies, including some instance-based ones:

The Efficiency of Theorem Proving Strategies:  A Comparative and
Asymptotic Analysis (Vieweg, Wiesbaden, 1997), 170 pp, with Yunshan
Zhu.

The application of OSHL to planning problems, where it outperforms
resolution:

FOLPLAN: A Semantically Guided First-Order Planner, with Yunshan Zhu,
10th International FLAIRS Conference, Daytona Beach, Florida, May
11-14,1997.

Another theorem proving strategy closely related to clause linking,
it turns out, but developed independently:

A partial instantiation based first-order theorem prover, by Hooker,
Rago, Chandru, and Shrivastava, Workshop on First-Order Theorem
Proving, Vienna, Austria, 1998.

A previous method on which Hooker's work is based:

Jeroslow, R.G., Computation-oriented reductions of predicate to
propositional logic, Decision Support Systems 4 (1988) 183-197.

A very early instance-based method:

Gilmore, P. C., A Proof Method for Quantification Theory, IBM Journal
of Research and Development 4 (1960) 28-35.

An early method with some similarities to clause linking:

Davis, M., Eliminating the Irrelevant From Machanical Proofs,
Proceedings Symp. of Applied Math, vol. 15, pp. 15-30, 1963.

The basis of the well-known Davis and Putnam procedure used in many
instance-based methods:

Davis, M. and Putnam, H., A Computing Procedure for Quantification
Theory, JACM 7 (1960) 201-215.

A modification of Davis and Putnam's method which is commonly used
today:

Davis, M., Logemann, G. and Loveland, D., A Machine Program for
Theorem-Proving, CACM 5 (1962) 394-397.