A combined superposition and model evolution calculus. (English) Zbl 1267.03033
The paper presents a new calculus for first-order theorem proving with equality, which generalizes both the superposition calculus and the model evolution calculus (with equality). This calculus integrates the inference rules of superposition and of model evolution preserving the individual semantically-based redundancy criteria of both calculi in a single framework. Moreover, this work simplifies the presentation of the model evolution calculus by using the better-known superposition framework. The main result of the paper is the completeness proof of the calculus under semantically justified redundancy criteria and simplification rules.
Reviewer: Emilio Muñoz-Velasco (Málaga)
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
References:
| [1] | Baumgartner, P.: Logical engineering with instance-based methods. In: Pfenning, F. (ed.) CADE-21–The 21st International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 4603, pp. 404–409. Springer (2007) |
| [2] | Bachmair, L., Ganzinger, H.: Chapter 11: Equational reasoning in saturation-based theorem proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction. A Basis for Applications. Vol. I: Foundations. Calculi and Refinements, pp. 353–398. Kluwer Academic Publishers (1998) · Zbl 0973.68215 |
| [3] | Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5(3/4), 193–212 (1994) · Zbl 0797.03008 · doi:10.1007/BF01190829 |
| [4] | Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) · Zbl 0948.68098 |
| [5] | Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) CADE-19–The 19th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 2741, pp. 350–364. Springer (2003) · Zbl 1278.68249 |
| [6] | Baumgartner, P., Tinelli, C.: The model evolution calculus with equality. In: Nieuwenhuis, R. (ed.) CADE-20–The 20th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 3632, pp. 392–408. Springer (2005) · Zbl 1135.03325 |
| [7] | Comon, H.: Disunification: a survey. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson. MIT Press (1991) |
| [8] | Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc. 18th IEEE Symposium on Logic in Computer Science, (LICS’03), pp. 55–64. IEEE Computer Society Press (2003) |
| [9] | Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Computer Science Logic (CSL’04). Lecture Notes in Computer Science, vol. 3210, pp. 71–84. Springer (2004) · Zbl 1095.68111 |
| [10] | Jacobs, S., Waldmann, U.: Comparing instance generation methods for automated reasoning. J. Autom. Reason. 38(1–3), 57–78 (2007) · Zbl 1113.68089 · doi:10.1007/s10817-006-9046-x |
| [11] | Korovin, K.: Iprover–an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 2008. Lecture Notes in Computer Science, vol. 5195, pp. 292–298. Springer (2008) · Zbl 1165.68462 |
| [12] | Korovin, K.: Instantiation-based automated reasoning: from theory to practice. In: Schmidt, R.A. (ed.) Automated Deduction–CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5663, pp. 163–166. Springer (2009) |
| [13] | Lynch, C., McGregor, R.E.: Combining instance generation and resolution. In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems (FroCoS 2009). LNAI, vol. 5749, pp. 304–318. Springer (2009) · Zbl 1193.03028 |
| [14] | Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering and equality constrained clauses. J. Symb. Comput. 19, 321–351 (1995) · Zbl 0844.68107 · doi:10.1006/jsco.1995.1020 |
| [15] | Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reason. 25(3), 167–217 (2000) · Zbl 0959.68115 · doi:10.1023/A:1006376231563 |
| [16] | Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: System description: Spass version 3.0. In: Pfenning, F. (ed.) CADE-21–21st International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 4603, pp. 514–520. Springer (2007) · Zbl 1213.68577 |
| [17] | Zhang, T., Sipma, H.B., Manna, Z.: The decidability of the first-order theory of term algebras with Knuth-Bendix order. In: Nieuwenhuis, R. (ed.) 20th International Conference on Automated Deduction (CADE’05). Lecture Notes in Artificial Intelligence, vol. 3632, pp. 131–148. Springer (2005) · Zbl 1135.03323 |
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.
