Model evolution with equality – revised and implemented. (English) Zbl 1258.03020
The paper presents the revised and improved version of the model evolution calculus with equality. The authors extend the model evolution calculus by adding some inference rules for equality reasoning. These rules were centered around a version of the ordered paramodulation inference rules adapted to the model evolution calculus. The new calculus works with a set of literals, which are called a context, and a set of clauses. Correspondingly, it has two kinds of inference rules, one for modifying contexts, and one for deriving new clauses, with the latter consisting mostly on unit-superposition-style inference rule.
As a result, this calculus features more powerful redundancy criteria and removes some nondeterminism from the calculus.
The authors prove the soundness and completeness of the calculus and discuss its implementation in the E-Darvin theorem prover based on Darvin.
As a result, this calculus features more powerful redundancy criteria and removes some nondeterminism from the calculus.
The authors prove the soundness and completeness of the calculus and discuss its implementation in the E-Darvin theorem prover based on Darvin.
Reviewer: Nail Zamov (Kazan)
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
Keywords:
automated theorem proving; equational reasoning; superposition inference rule; instance-based methods; model evolution calculus with equality; theorem prover E-DarvinSoftware:
E Theorem Prover; E-KRHyper; Bliksem; iProver; VAMPIRE; SPASS; Metis_; E-Darvin; OTTER; TPTP; DarwinReferences:
| [1] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press |
| [2] | Bachmair, L.; Ganzinger, H., Chapter 11: Equational reasoning in saturation-based theorem proving, (Bibel, W.; Schmitt, P. H., Automated Deduction. A Basis for Applications. Vol. I: Foundations. Calculi and Refinements (1998), Kluwer Academic Publishers), 353-398 · Zbl 0973.68215 |
| [3] | Bachmair, L.; Ganzinger, H.; Waldmann, U., Refutational theorem proving for hierarchic first-order theories, Applicable Algebra in Engineering, Communication and Computing, 5, 3-4, 193-212 (1994) · Zbl 0797.03008 |
| [4] | Baumgartner, P., FDPLL-A first-order Davis-Putnam-Logeman-Loveland procedure, (McAllester, D., CADE-17-The 17th International Conference on Automated Deduction. CADE-17-The 17th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence., vol. 1831 (2000), Springer), 200-219 · Zbl 0963.68182 |
| [5] | Baumgartner, P., Logical engineering with instance-based methods, (Pfenning, F., CADE-21-The 21st International Conference on Automated Deduction. CADE-21-The 21st International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 4603 (2007), Springer), 404-409 |
| [6] | Baumgartner, P.; Fuchs, A.; Tinelli, C., Implementing the model evolution calculus, International Journal of Artificial Intelligence Tools, 15, 1, 21-52 (2006) |
| [7] | Baumgartner, P.; Tinelli, C., The model evolution calculus, (Baader, F., CADE-19-The 19th International Conference on Automated Deduction. CADE-19-The 19th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 2741 (2003), Springer), 350-364 · Zbl 1278.68249 |
| [8] | Baumgartner, P.; Tinelli, C., The model evolution calculus with equality, (Nieuwenhuis, R., CADE-20-The 20th International Conference on Automated Deduction. CADE-20-The 20th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 3632 (2005), Springer), 392-408 · Zbl 1135.03325 |
| [9] | Baumgartner, P.; Tinelli, C., The model evolution calculus as a first-order DPLL method, Artificial Intelligence, 172, 4-5, 591-632 (2008) · Zbl 1182.03034 |
| [10] | Baumgartner, P.; Waldmann, U., Superposition and model evolution combined, (Schmidt, R., CADE-22-The 22nd International Conference on Automated Deduction. CADE-22-The 22nd International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence., vol. 5663 (2009), Springer), 17-34 · Zbl 1237.03010 |
| [11] | Bernays, P.; Schönfinkel, M., Zum Entscheidungsproblem der Mathematischen Logic, Mathematische Annalen, 99, 342-372 (1928) · JFM 54.0056.05 |
| [12] | Billon, J.-P., The disconnection method, (Miglioli, P.; Moscato, U.; Mundici, D.; Ornaghi, M., Theorem Proving with Analytic Tableaux and Related Methods. Theorem Proving with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence, No. 1071 (1996), Springer), 110-126 · Zbl 1412.68210 |
| [13] | Claessen, K., 2005. Equinox, a new theorem prover for full first-order logic with equality, presentation at Dagstuhl Seminar 05431 on Deduction and Applications.; Claessen, K., 2005. Equinox, a new theorem prover for full first-order logic with equality, presentation at Dagstuhl Seminar 05431 on Deduction and Applications. |
| [14] | Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem proving, Communications of the ACM, 5, 7, 394-397 (1962) · Zbl 0217.54002 |
| [15] | de Nivelle, H., 1999. The Bliksem theorem prover.; de Nivelle, H., 1999. The Bliksem theorem prover. |
| [16] | de Nivelle, H.; Meng, J., Geometric resolution: A proof procedure based on finite model search, (Furbach, U.; Shankar, N., IJCAR. IJCAR, Lecture Notes in Computer Science, vol. 4130 (2006), Springer), 303-317 · Zbl 1222.68378 |
| [17] | Ganzinger, H.; Korovin, K., New directions in instantiation-based theorem proving, (Proc. 18th IEEE Symposium on Logic in Computer Science. Proc. 18th IEEE Symposium on Logic in Computer Science, LICS’03 (2003), IEEE Computer Society Press), 55-64 |
| [18] | Ganzinger, H.; Korovin, K., Integrating equational reasoning into instantiation-based theorem proving, (Computer Science Logic. Computer Science Logic, CSL’04. Computer Science Logic. Computer Science Logic, CSL’04, Lecture Notes in Computer Science, vol. 3210 (2004), Springer), 71-84 · Zbl 1095.68111 |
| [19] | Hurd, J., 2003. First-order proof tactics in higher-order logic theorem provers. In: Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports. pp. 56-68.; Hurd, J., 2003. First-order proof tactics in higher-order logic theorem provers. In: Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports. pp. 56-68. |
| [20] | Korovin, K., iProver—an instantiation-based theorem prover for first-order logic (system description), (IJCAR ’08: Proceedings of the 4th international joint conference on Automated Reasoning (2008), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 292-298 · Zbl 1165.68462 |
| [21] | Korovin, K., Instantiation-based automated reasoning: from theory to practice, (Schmidt, R. A., Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction. Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction. Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5663 (2009), Springer), 163-166 · Zbl 1167.68006 |
| [22] | Letz, R.; Stenz, G., Integration of equality reasoning into the disconnection calculus, (Egly, U.; Fermüller, C. G., TABLEAUX. TABLEAUX, Lecture Notes in Computer Science, vol. 2381 (2002), Springer), 176-190 · Zbl 1015.68172 |
| [23] | McCune, W., Experiments with discrimination-tree indexing and path indexing for term retrieval, Journal of Automated Reasoning, 9, 2, 147-167 (1992) · Zbl 0781.68101 |
| [24] | McCune, W., 2003. OTTER 3.3 Reference Manual. Argonne National Laboratory, Argonne, Illinois.; McCune, W., 2003. OTTER 3.3 Reference Manual. Argonne National Laboratory, Argonne, Illinois. |
| [25] | Nieuwenhuis, R.; Rubio, A., Theorem proving with ordering and equality constrained clauses, Journal of Symbolic Computation, 19, 321-351 (1995) · Zbl 0844.68107 |
| [26] | Nieuwenhuis, R., Rubio, A., 2001. Paramodulation-based theorem proving. In: [32], pp. 371-443.; Nieuwenhuis, R., Rubio, A., 2001. Paramodulation-based theorem proving. In: [32], pp. 371-443. · Zbl 0997.03012 |
| [27] | Pelletier, F. J.; Sutcliffe, G.; Suttner, C., The development of CASC, AI Communications, 15, 2-3, 79-90 (2002) · Zbl 1019.68101 |
| [28] | Pelzer, B.; Wernhard, C., System description: E-KRHyper, (Pfenning, F., Automated Deduction - 21st International Conference on Automated Deduction (CADE-21). Automated Deduction - 21st International Conference on Automated Deduction (CADE-21), Lecture Notes in Computer Science, vol. 4603 (2007), Springer), 508-513 · Zbl 1213.68574 |
| [29] | Plaisted, D. A.; Zhu, Y., Ordered semantic hyper linking, Journal of Automated Reasoning, 25, 3, 167-217 (2000) · Zbl 0959.68115 |
| [30] | Ramsey, F. P., On a problem in formal logic, Proceedings of the London Mathematical Society, 30, 264-286 (1930) · JFM 55.0032.04 |
| [31] | Riazanov, A.; Voronkov, A., The design and implementation of Vampire, AI Communications, 15, 2-3, 91-110 (2002) · Zbl 1021.68082 |
| [32] | (Robinson, J. A.; Voronkov, A., Handbook of Automated Reasoning (in 2 volumes) (2001), Elsevier and MIT Press) · Zbl 0964.00020 |
| [33] | Schulz, S., E — a brainiac theorem prover, AI Communications, 15, 2-3, 111-126 (2002) · Zbl 1020.68084 |
| [34] | Stickel, M.E., Waldinger, R.J., Chaudhri, V.K., 2000. A guide to SNARK. Technical report. SRI International.; Stickel, M.E., Waldinger, R.J., Chaudhri, V.K., 2000. A guide to SNARK. Technical report. SRI International. |
| [35] | Sutcliffe, G.; Suttner, C., The TPTP Problem Library: CNF Release v1.2.1, Journal of Automated Reasoning, 21, 2, 177-203 (1998) · Zbl 0910.68197 |
| [36] | Sutcliffe, G.; Suttner, C., The state of CASC, AI Communications, 19, 1, 35-48 (2006) · Zbl 1112.68464 |
| [37] | Weidenbach, C.; Schmidt, R.; Hillenbrand, T.; Rusev, R.; Topic, D., System description: Spass version 3.0, (Pfenning, F., Automated Deduction — 21st International Conference on Automated Deduction (CADE-21). Automated Deduction — 21st International Conference on Automated Deduction (CADE-21), Lecture Notes in Computer Science, vol. 4603 (2007), Springer), 514-520 · Zbl 1213.68577 |
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.
