Abstract
In this paper we consider first-order logic theorem proving and model building via approximation and instantiation. Given a clause set we propose its approximation into a simplified clause set where satisfiability is decidable. The approximation extends the signature and preserves unsatisfiability: if the simplified clause set is satisfiable in some model, so is the original clause set in the same model interpreted in the original signature. A refutation generated by a decision procedure on the simplified clause set can then either be lifted to a refutation in the original clause set, or it guides a refinement excluding the previously found unliftable refutation. This way the approach is refutationally complete. We do not step-wise lift refutations but lift conflicting cores, finite unsatisfiable clause sets representing at least one refutation. The approach is dual to many existing approaches in the literature.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baeten, J.C.M., Bergstra, J.A., Klop, J.W., Weijland, W.P.: Term-rewriting systems with rule priorities. Theor. Comput. Sci. 67(2&3), 283–301 (1989)
Giunchiglia, F., Giunchiglia, E.: Building complex derived inference rules: A decider for the class of prenex universal-existential formulas. In: ECAI, pp. 607–609 (1988)
Giunchiglia, F., Walsh, T.: A theory of abstraction. Artif. Intell. 57(2–3), 323–389 (1992)
Hobbs, J.R.: Granularity. In: Proceedings of the Ninth International Joint Conference on Artificial Intelligence, pp. 432–435. Morgan Kaufmann (1985)
Imielinski, T.: Domain abstraction and limited reasoning. In: Proceedings of the 10th International Joint Conference on Artificial Intelligence, vol. 2, pp. 997–1003. Morgan Kaufmann Publishers Inc., San Francisco (1987)
Korovin, K.: Inst-Gen - A modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 239–270. Springer, Heidelberg (2013)
Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter examples. J. Autom. Reason. 3(3), 301–317 (1987)
Newell, A.: Human Problem Solving. Prentice-Hall, Inc., Upper Saddle River (1972)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving sat and sat modulo theories: From an abstract davis–putnam–logemann–loveland procedure to dpll(t). Journal of the ACM 53, 937–977 (2006)
Plaisted Theorem, D.A.: proving with abstraction. Artif. Intell. 16(1), 47–108 (1981)
Sacerdott, E.D.: Planning in a hierarchy of abstraction spaces. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, IJCAI 1973, pp. 412–422. Morgan Kaufmann Publishers Inc., San Francisco (1973)
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)
Tenenberg, J.: Preserving consistency across abstraction mappings. In: Proceedings of the 10th IJCAI, International Joint Conference on Artificial Intelligence, pp. 1011–1014 (1987)
Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999)
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, chapter 27, pp. 1965–2012. Elsevier (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Teucke, A., Weidenbach, C. (2015). First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation. In: Lutz, C., Ranise, S. (eds) Frontiers of Combining Systems. FroCoS 2015. Lecture Notes in Computer Science(), vol 9322. Springer, Cham. https://doi.org/10.1007/978-3-319-24246-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-24246-0_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24245-3
Online ISBN: 978-3-319-24246-0
eBook Packages: Computer ScienceComputer Science (R0)