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.