zbMATH — the first resource for mathematics

The relative power of semantics and unification. (English) Zbl 1383.68081
Voronkov, Andrei (ed.) et al., Programming logics. Essays in memory of Harald Ganzinger. Berlin: Springer (ISBN 978-3-642-37650-4/pbk). Lecture Notes in Computer Science 7797, 317-344 (2013).
Summary: The OSHL theorem proving method is an attempt to extend propositional theorem proving techniques to first-order logic by working entirely at the ground level. A disadvantage of this approach is that OSHL does not perform unifications between non-ground literals, as resolution does. However, OSHL has the capability to use natural semantics to guide the proof search. The question arises whether the advantage of proof guidance using semantics can make up for the loss of unification between non-ground literals that other methods employ. This question is studied and some evidence is given that a properly chosen semantics causes OSHL to implicitly perform unifications between non-ground levels, suggesting that OSHL may have some of the advantages of theorem proving methods based on unification as well as some of the efficiencies of propositional theorem provers. Some implementation results of OSHL with and without nontrivial semantics are also presented to illustrate its properties.
For the entire collection see [Zbl 1259.03008].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Full Text: DOI
[1] Giunchiglia, E., Walsh, T.: SAT 2005 (January 2004)
[2] Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. Journal of Automated Reasoning 25(3), 167–217 (2000) · Zbl 0959.68115
[3] Baumgartner, P.: FDPLL – A First-Order Davis-Putnam-Logeman-Loveland Procedure. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 200–219. Springer, Heidelberg (2000) · Zbl 0963.68182
[4] Letz, R., Stenz, G.: DCTP - A Disconnection Calculus Theorem Prover - System Abstract. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 381–385. Springer, Heidelberg (2001) · Zbl 0988.68589
[5] Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 350–364. Springer, Heidelberg (2003) · Zbl 1278.68249
[6] Baumgartner, P., Tinelli, C.: Model Evolution with Equality Modulo Built-in Theories. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 85–100. Springer, Heidelberg (2011) · Zbl 1341.68180
[7] 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
[8] Baumgartner, P., Tinelli, C.: The Model Evolution Calculus with Equality. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 392–408. Springer, Heidelberg (2005) · Zbl 1135.03325
[9] Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc. 18th IEEE Symposium on Logic in Computer Science, pp. 55–64. IEEE Computer Society Press (2003)
[10] Korovin, K., Sticksel, C.: iProver-Eq: An Instantiation-Based Theorem Prover with Equality. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 196–202. Springer, Heidelberg (2010) · Zbl 1291.68354
[11] Ganzinger, H., Korovin, K.: Integrating Equational Reasoning into Instantiation-Based Theorem Proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 71–84. Springer, Heidelberg (2004) · Zbl 1095.68111
[12] Lee, S.-J., Plaisted, D.: Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning 9(1), 25–42 (1992) · Zbl 0784.68077
[13] Baumgartner, P., Thorstensen, E.: Instance based methods – a brief overview. KI - Künstliche Intelligenz 24, 35–42 (2010) · Zbl 05743549
[14] Gelernter, H., Hansen, J.R., Loveland, D.W.: Empirical explorations of the geometry theorem proving machine. In: Feigenbaum, E., Feldman, J. (eds.) Computers and Thought, pp. 153–167. McGraw-Hill, New York (1963)
[15] Das, S., Plaisted, D.: An improved propositional approach to first-order theorem proving. In: Baumgartner, P., Fermueller, C. (eds.) CADE-19 Workshop W4 Model Computation - Principles, Algorithms, Applications, Miami, Florida, USA (2003)
[16] Suttner, C.B., Sutcliffe, G.: The TPTP problem library (TPTP v2.0.0). Technical Report AR-97-01, Institut für Informatik, Technische Universität München, Germany (1997) · Zbl 0910.68197
[17] Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the Association for Computing Machinery 7, 201–215 (1960) · Zbl 0212.34203
[18] Robinson, J.: A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery 12, 23–41 (1965) · Zbl 0139.12303
[19] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5, 394–397 (1962) · Zbl 0217.54002
[20] Yahya, A., Plaisted, D.A.: Ordered semantic hyper tableaux. Journal of Automated Reasoning 29(1), 17–57 (2002) · Zbl 1016.03015
[21] McCune, W.: Fascinating XCB inference. AAR Newsletter 66 (February 2005)
[22] Stickel, M.E.: Automated deduction by theory resolution. Journal of Automated Reasoning 1, 333–355 (1985) · Zbl 0616.68076
[23] Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4), 337–362 (2009) · Zbl 1185.68636
[24] McCune, W.: Otter 2.0 (theorem prover). In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 663–664. Springer, Heidelberg (1990)
[25] Claessen, K.: Equinox, a new theorem prover for full first-order logic with equality. In: Dagstuhl Seminar 05431 on Deduction and Applications (October 2005)
[26] Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications 19(1), 35–48 (2006) · Zbl 1112.68464
[27] Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91–110 (2002) · Zbl 1021.68082
[28] Zhu, Y., Plaisted, D.: FOLPLAN: A semantically guided first-order planner. In: Proceedings of the 10th International FLAIRS Conference (1997)
[29] Fikes, R., Nilsson, N.J.: STRIPS: A new approach to the application of theorem proving to problem solving. Artif. Intell. 2(3/4), 189–208 (1971) · Zbl 0234.68036
[30] Lifschitz, V.: On the semantics of STRIPS. In: Reasoning about Actions and Plans: Proceedings of the 1986 Workshop, pp. 1–9. Morgan Kaufmann (1987)
[31] Penberthy, J.S., Weld, D.S.: UCPOP: A sound, complete, partial order planner for ADL. In: The Third International Conference on Knowledge Representation and Reasoning (KR 1992), pp. 103–114 (1992)
[32] Edwin, P.D.: Pednault. ADL and the state-transition model of action. J. Log. Comput. 4(5), 467–512 (1994) · Zbl 0815.68105
[33] Bonacina, M., Hsiang, J.: On semantic resolution with lemmaizing and contraction and a formal treatment of caching. New Generation Computing 16(2), 163–200 (1998)
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.