Abstract
We combine constrained literals for model representation with key concepts from first-order superposition and propositional conflict-driven clause learning (CDCL) to create the new calculus Non-Redundant Clause Learning (NRCL) deciding the Bernays-Schönfinkel fragment. We use first-order literals constrained by disequalities between tuples of terms for compact model representation. From superposition, NRCL inherits the abstract redundancy criterion and the monotone model operator. CDCL adds the dynamic, conflict-driven search for a model. As a result, NRCL finds a false clause modulo the current model candidate effectively. It guides the derivation of a first-order ordered resolvent that is never redundant. Similar to 1UIP-learning in CDCL, the learned resolvent induces backtracking and, by blocking the previous conflict state via propagation, it enforces progress towards finding a model or a refutation. The non-redundancy result also implies that only finitely many clauses can be generated by NRCL on the Bernays-Schönfinkel fragment, which proves termination.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alagi, G., Weidenbach, C.: NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Full Paper). CoRR, abs/1502.05501 (2015). http://arxiv.org/abs/1502.05501
Armando, A., Baumgartner, P., Dowek, G. (eds.): IJCAR 2008. LNCS (LNAI), vol. 5195. Springer, Heidelberg (2008)
Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson and Voronkov (eds.) [23], pp. 19–99
Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma Learning in the model evolution calculus. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 572–586. Springer, Heidelberg (2006)
Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 350–364. Springer, Heidelberg (2003)
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)
Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Notes of the Fourth Workshop on Practical Aspects in Automated Reasoning (PAAR) (2014)
Claessen, K., Srensson, N.: New Techniques that Improve MACE-style finite model finding. In: Model Computation - Principles, Algorithms, Applications (2003)
Comon, H.: Disunification: A survey. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 322–359 (1991)
Fietzke, A., Weidenbach, C.: Labelled splitting. Ann. Math. Artif. Intell. 55(1–2), 3–34 (2009)
Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: LICS, pp. 55–64. IEEE Computer Society (2003)
Higman, G.: Ordering by Divisibility in Abstract Algebras. Proceedings of the London Mathematical Society 2(1), 326–336 (1952)
Hillenbrand, T., Weidenbach, C.: Superposition for bounded domains. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 68–100. Springer, Heidelberg (2013)
Korovin, K.: iProver - An instantiation-based theorem prover for first-order logic (system description). In: Armando et al. [2], pp. 292–298
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)
Korovin, K.: Non-cyclic sorts for first-order satisfiability. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 214–228. Springer, Heidelberg (2013)
Lassez, J.-L., Marriott, K.: Explicit Representation of Terms Defined by Counter Examples. J. Autom. Reasoning 3(3), 301–317 (1987)
Lewis, H.R.: Complexity Results for Classes of Quantificational Formulas. J. Comput. Syst. Sci. 21(3), 317–353 (1980)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL nodulo theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 36–50. Springer, Heidelberg (2005)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson and Voronkov [23], pp. 371–443
Pérez, J.A.N., Voronkov, A.: Proof Systems for Effectively Propositional Logic. In: Armando et al. [21], pp. 426–440
Piskac, R., de Moura, L.M., Bjørner, N.: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom. Reasoning 44(4), 401–424 (2010)
Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. 2. Elsevier and MIT Press (2001)
Silva, J.P.M., Sakallah, K.A.: Conflict analysis in search algorithms for satisfiability. In: ICTAI, pp. 467–469 (1996)
Suda, M., Weidenbach, C., Wischnewski, P.: On the saturation of YAGO. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 441–456. Springer, Heidelberg (2010)
Tammet, T.: Finite model building: improvements and comparisons. In: Model Computation: Principles, Algorithms, Applications (2003)
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson and Voronkov [23], pp. 1965–2013
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Alagi, G., Weidenbach, C. (2015). NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment. 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_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-24246-0_5
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)