×

Building proofs or counterexamples by analogy in a resolution framework. (English) Zbl 1427.68345

Alferes, José Júlio (ed.) et al., Logics in artificial intelligence. European workshop, JELIA ’96, Évora, Portugal, September 30 – October 3, 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1126, 34-49 (1996).
Summary: Taking an extension of resolution as a base calculus (though its principles are applicable to other calculi) for searching proofs (refutations) and counterexamples (models), we introduce a new method able to find refutations and also models by analogy with refutations and models in a knowledge base. The source objects for the analogy process are generalizations of the refutations (models). They are included in the knowledge base, and then unification techniques for the choice of the relevant source objects as well as the building of a new proof or a model by analogy are used. These steps are rather standard, and can hardly be avoided. Our method follows these steps but incorporates original contributions on each of them. A method to build new proofs as well as models by analogy with existing ones is proposed. Some comparisons with existing methods as well as two detailed running examples on generalization show evidence of the interest of our approach.
For the entire collection see [Zbl 1415.68010].

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68T30 Knowledge representation

Software:

TPTP
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Christophe Bourely, Ricardo Caferra, and Nicolas Peltier. A method for building models automatically. Experiments with an extension of OTTER. In Proc. of CADE-12, pages 72-86. Springer Verlag, 1994. LNAI 814. · Zbl 1433.68536
[2] Th. Boy de la Tour and R. Caferra. Proof analogy in interactive theorem proving: A method to express and use it via second order pattern matching. In Proceedings of AAAI 87, pages 95-99. Morgan Kaufmann, 1987.
[3] Th. Boy de la Tour and Ch. Kreitz. Building proofs by analogy via the Curry-Howard isomorphism. In Proceedings of LPAR 92, pages 202-213. Springer Verlag, 1992. · Zbl 0925.68400
[4] W. W. Bledsoe. Non-resolution theorem proving. Artificial Intelligence, 9:1-35, 1977. · Zbl 0358.68131 · doi:10.1016/0004-3702(77)90012-1
[5] Hubert Comon and Pierre Lescanne. Equational problems and disunification. Journal of Symbolic Computation, 7:371-475, 1989. · Zbl 0678.68093
[6] Ricardo Caferra and Nicolas Peltier. Extending semantic resolution via automated model building: applications. In Proceeding of IJCAI’95, pages 328-334. Morgan Kaufman, 1995.
[7] Ricardo Caferra and Nicolas Peltier. Model building and interactive theory discovery. In Proceeding of Tableaux’95, LNAI 918, pages 154-168. Springer-Verlag, 1995.
[8] R. Curien, Z. Qian, and Hui Shi. Efficient second-order matching. In Proceedings of 7th Rewriting Techniques and Applications, 1996. To appear. · Zbl 1503.68098
[9] Ricardo Caferra and Nicolas Zabel. A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation, 13:613-641, 1992. · Zbl 0770.68104
[10] R.P. Hall. Computational approaches to analogical reasoning: A comparative analysis. Artificial Intelligence, pages 39-120, 1989. · Zbl 0668.68097
[11] R.E. Kling. A paradigm for reasoning by analogy. Artificial Intelligence, 2, 1971. · Zbl 0227.68041
[12] Th. Kolbe and Ch. Walther. Second-order pattern matching modulo evaluation — A technique for reusing proofs. In Chris S. Mellish, editor, Proceedings of IJGAI 95, pages 190-195. IJCAI, Morgan Kaufmann, 1995.
[13] Donald W. Loveland. Automated Theorem Proving: A Logical Basis, volume 6 of Fundamental Studies in Computer Science. North Holland, 1978. · Zbl 0364.68082
[14] E. Melis. A model of analogy-driven proof-plan construction. In C. S. Mellish, editor, Proceedings of IJCAI’95, pages 182-188. IJCAI, Morgan Kaufmann Publishers Inc., 1995.
[15] J.C. Munyer. Analogy as a mean of discovery in problem-solving and learning. PhD thesis, Univ. Calif. Santa Cruz, 1981.
[16] D.A. Plaisted. Theorem proving with abstraction. Artificial Intelligence, 16:47-108, 1981. · Zbl 0454.68113 · doi:10.1016/0004-3702(81)90015-1
[17] Ch. B. Suttner and G. Sutcliffe. The TPTP problem library. Technical report, TU München / James Cook University, 1995. V-1.2.0. · Zbl 0910.68197
[18] Larry Wos, Ross Overbeek, Ewin Lush, and Jim Boyle. Automated Reasoning: Introduction and Application. McGraw-Hill, second edition, 1992. · Zbl 0820.68116
[19] Larry Wos. Automated Reasoning, 33 Basic Research Problems. Prentice Hall, 1988. · Zbl 0663.68102
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.