{NRCL} - a model building approach to the {Bernays-Schönfinkel} fragment

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.
Type de document :
Communication dans un congrès
Carsten Lutz and Silvio Ranise. Frontiers of Combining Systems, 10th International Symposium (FroCos 2015), 2015, Wroclaw, Poland. Springer, Lecture Notes in Computer Science, 9322, pp.69-84, 〈10.1007/978-3-319-24246-0_5〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01247991
Contributeur : Stephan Merz <>
Soumis le : mercredi 23 décembre 2015 - 11:48:35
Dernière modification le : lundi 20 novembre 2017 - 15:14:02

Identifiants

Collections

Citation

Gábor Alagi, Christoph Weidenbach. {NRCL} - a model building approach to the {Bernays-Schönfinkel} fragment. Carsten Lutz and Silvio Ranise. Frontiers of Combining Systems, 10th International Symposium (FroCos 2015), 2015, Wroclaw, Poland. Springer, Lecture Notes in Computer Science, 9322, pp.69-84, 〈10.1007/978-3-319-24246-0_5〉. 〈hal-01247991〉

Partager

Métriques

Consultations de la notice

102