Abstract
We present a proof procedure that is complete for first-order logic, but which can also be used when searching for finite models. The procedure uses a normal form which is based on geometric formulas. For this reason we call the procedure geometric resolution. We expect that the procedure can be used as an efficient proof search procedure for first-order logic. In addition, the procedure can be implemented in such a way that it is complete for finding finite models.
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.
References
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 4(3), 217–247 (1994)
Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 350–364. Springer, Heidelberg (2003)
Bezem, M.: Disproving distributivity in lattices using geometric logic. In: Workshop on Disproving, Non-Theorems, Non-Validity, Non-Provability, informal proceedings, July 2005, pp. 24–31 (2005)
Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 246–260. Springer, Heidelberg (2005)
Bry, F., Torge, S.: A deduction method complete for refutation and finite satisfiability. In: Dix, J., Fariñas del Cerro, L., Furbach, U. (eds.) JELIA 1998. LNCS (LNAI), vol. 1489, pp. 122–138. Springer, Heidelberg (1998)
de Nivelle, H., de Rijke, M.: Deciding the guarded fragments by resolution. Journal of Symbolic Computation 35(1), 21–58 (2003)
Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: LICS 1999, pp. 295–303 (1999)
Kazakov, Y., de Nivelle, H.: A resolution decision procedure for the guarded fragment with transitive guards. In: IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 122–136. Springer, Heidelberg (2004)
Kim, S., Zhang, H.: ModGen: Theorem proving by model generation. In: Hayes-Roth, B., Korf, R. (eds.) Proceedings of AAAI 1994, pp. 162–167. AAAI Press, Menlo Park (1994)
McCune, W.: Models and counter examples MACE2 (system), http://www-unix.mcs.anl.gov/AR/mace2/
Robinson, J.A.: A machine oriented logic based on the resolution principle. Journal of the ACM 12, 23–41 (1965)
Slaney, J.: Scott: A model-guided theorem prover. In: IJCAI 1993, pp. 109–114 (1993)
Zhang, J.: Constructing finite algebras with FALCON. Journal of Automated Reasoning 17, 1–22 (1996)
Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: IJCAI, pp. 298–303 (1995)
Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 295–313. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Nivelle, H., Meng, J. (2006). Geometric Resolution: A Proof Procedure Based on Finite Model Search. In: Furbach, U., Shankar, N. (eds) Automated Reasoning. IJCAR 2006. Lecture Notes in Computer Science(), vol 4130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814771_28
Download citation
DOI: https://doi.org/10.1007/11814771_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37187-8
Online ISBN: 978-3-540-37188-5
eBook Packages: Computer ScienceComputer Science (R0)