A method for building models automatically. Experiments with an extension of OTTER. (English) Zbl 1433.68536
Bundy, Alan (ed.), Automated deduction – CADE-12. 12th international conference, Nancy, France, June 26 – July 1, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 814, 72-86 (1994).
Summary: A previous work on Herbrand model construction is extended in two ways. The first extension increases the capabilities of the method, by extending one of its key rules. The second, more important one, defines a new method for simultaneous search of refutations and models for set of equational clauses. The essential properties of the new method are given. The main theoretical result of the paper is the characterization of conditions assuring that models can be built. Both methods (for equational and non equational clauses) have been implemented as an extension of OTTER. Several running examples are given, in particular a new automatic solution of the ternary algebra problem first solved by Winker.
The examples emphasize the unified approach to model building allowed by the ideas underlying our method and the usefulness of using constrained clauses. Several problems open by the present work are the main lines of future work.
For the entire collection see [Zbl 0875.00063].
The examples emphasize the unified approach to model building allowed by the ideas underlying our method and the usefulness of using constrained clauses. Several problems open by the present work are the main lines of future work.
For the entire collection see [Zbl 0875.00063].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Christophe BOURELY, Ricardo CAFERRA, and Nicolas PELTIER. Model building in automated deduction. Forthcoming, 1994. · Zbl 1433.68536 |
| [2] | Leo BACHMAIR, Harald GANZINGER, and Uwe WALDMANN. Superposition with simplification as a decision procedure for the monadic class with equality. In Computational Logic and Proof Theory, KGC’93, pages 83-96. Springer-Verlag, Lecture Notes in Computer Science 713, 1993. · Zbl 0793.68127 |
| [3] | W.W. BLEDSOE and D.W. LOVELAND. Automated Theorem Proving after 25 years, volume 29 of Contemporary Mathematics. American Mathematical Society, Providence, RI, USA, 1984. · Zbl 0545.00023 |
| [4] | Hubert COMON and Pierre LESCANNE. Equational problems and disunification. Journal of Symbolic Computation, 7:371-475, 1989. · Zbl 0678.68093 |
| [5] | Hubert COMON. Disunification: a survey. In Jean-Louis Lassez and Gordon Plötkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991. |
| [6] | Ricardo CAFERRA and Nicolas ZABEL. Extending resolution for model construction. In Logics in AI, JELIA’90, pages 153-169. Springer-Verlag, Lecture Notes in Artificial Intelligence 478, 1991. · Zbl 0797.03009 |
| [7] | 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 |
| [8] | Christian G. FERMüLLER and Alexander LEITSCH. Model building by resolution. In Computer Science Logic, CSL’92, pages 134-148. Springer-Verlag, Lecture Notes in Computer Science 702, 1992. · Zbl 0788.68128 |
| [9] | C. FERMüLLER, A. LEITSCH, T. TAMMET, and N. ZAMOV. Resolution Methods for the Decision Problem. Lecture Notes in Artificial Intelligence 679. Springer-Verlag, 1993. · Zbl 0789.03013 |
| [10] | Masayuki FUJITA, John SLANEY, and Frank BENNETT. Automatic generation of some results in finite algebra. In Proceedings of IJCAI’93, pages 52-67. Morgan and Kaufmann, 1993. |
| [11] | H. GELERNTER, J.R. HANSEN, and D.W. LOVELAND. Empirical explorations of the geometry theorem-proving machine. In Jörg Siekmann and Graham Wrightson, editors, Automation of Reasoning, vol. 1, pages 140-150. Springer-Verlag, 1983. Originally published in 1960. |
| [12] | Rainer MANTHEY and François BRY. Satchmo: A theorem prover implemented in PROLOG. In Proc. of CADE-9, pages 415-434. Springer-Verlag, Lecture Notes in Computer Science 310, 1988. · Zbl 0668.68104 |
| [13] | William W. McCUNE. OTTER 2.0 Users Guide. Argonne National Laboratory, 1990. · Zbl 1509.68312 |
| [14] | Saharon SHELAH. Decidability of a portion of the predicate calculus. Israel Journal of Mathematics, 28(1-2):32-44, 1977. · Zbl 0368.02014 |
| [15] | James R. SLAGLE. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687-697, October 1967. · Zbl 0157.02405 |
| [16] | Steve WINKER. Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions. Journal of the ACM, 29:273-284, 1982. · Zbl 0488.68056 |
| [17] | Larry WOS. |
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.
