# zbMATH — the first resource for mathematics

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.
Reviewer: Nail Zamov (Kazan)

##### MSC:
 03B35 Mechanization of proofs and logical operations 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text:
##### References:
 [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, (), 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, (), 200-219 · Zbl 0963.68182 [5] Baumgartner, P., Logical engineering with instance-based methods, (), 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, (), 350-364 · Zbl 1278.68249 [8] Baumgartner, P.; Tinelli, C., The model evolution calculus with equality, (), 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, (), 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, (), 110-126 [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. [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. [16] de Nivelle, H.; Meng, J., Geometric resolution: A proof procedure based on finite model search, (), 303-317 · Zbl 1222.68378 [17] Ganzinger, H.; Korovin, K., New directions in instantiation-based theorem proving, (), 55-64 [18] Ganzinger, H.; Korovin, K., Integrating equational reasoning into instantiation-based theorem proving, (), 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. [20] Korovin, K., Iprover—an instantiation-based theorem prover for first-order logic (system description), (), 292-298 · Zbl 1165.68462 [21] Korovin, K., Instantiation-based automated reasoning: from theory to practice, (), 163-166 [22] Letz, R.; Stenz, G., Integration of equality reasoning into the disconnection calculus, (), 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. [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. · 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, (), 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] () [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. [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, (), 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.