Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning
Published in: Journal of Automated Reasoning 2/2018

24-02-2017

Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning

Authors: John Slaney, Bruno Woltzenlogel Paleo

Published in: Journal of Automated Reasoning | Issue 2/2018

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

This paper defines the (first-order) conflict resolution calculus: an extension of the resolution calculus inspired by techniques used in modern Sat-solvers. The resolution inference rule is restricted to (first-order) unit propagation and the calculus is extended with a mechanism for assuming decision literals and with a new inference rule for clause learning, which is a first-order generalization of the propositional conflict-driven clause learning procedure. The calculus is sound (because it can be simulated by natural deduction) and refutationally complete (because it can simulate resolution), and these facts are proven in detail here.
next article Genetic Programming Proof Search Automatic Improvement

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Footnotes
1
CR is based on resolution instead of superposition, because superposition’s ordering-based refinements would restrict unit-propagation and the selection of decision literals. In Sat-solvers unit-propagation is unrestricted (because it is very effective anyway) and the best literal selection strategies are not based on orderings. By extending unrestricted resolution, CR remains general enough to admit the strategies used by Sat-solvers.
 
2
By Herbrand’s theorem, a finite number of instances would suffice in the case of an unsatisfiable clause set. As the logic is undecidable, however, there is no way to know in advance how many “several” might be.
 
3
This rule is also known as unit-resulting resolution [24, 25]. Here we use the name unit-propagating resolution instead in order to make the connection with the technique of unit-propagation more explicit.
 
4
As mentioned in Sect. 3, modern Sat-solvers implement optimized clause learning procedures that may also contain duals of propagated literals. A modification of CR ’s \(\mathbf {cl}\) inference rule to cover more sophisticated clause learning procedures is briefly discussed in Sect. 4.2.
 
5
The usual definition of UIP in terms of conflict graphs also relies on the notion of decision level of assigned literals and requires that the propagated literal be assigned at the current decision level. Therefore, our definition is slightly more general. This is intentional. The notion of decision level, which keeps track of the order in which decision literals were assigned, is beyond the purely proof-theoretical scope of this paper, as it relates to particular proof search and backtracking procedures.
 
6
CND is a calculus for classical logic: the law of excluded middle can be easily derived with a single application of implication introduction. Interestingly, its classicality is implicit in the use of involutive negation and the equivalence involving disjunctions and implications.
 
7
Since we assume that distinct clauses in \(\psi '\) do not share variables and \(\psi '\) is tree-like, we do not need to worry about variable clashes in the composition of all substitutions. The topological order is needed because a variable x introduced by a substitution \(\sigma _1\) may be in the domain of another substitution \(\sigma _2\) occurring below \(\sigma _1\). In this case, the topologically ordered composition is \(\sigma _1 \sigma _2\) (i.e. apply first \(\sigma _1\) and then \(\sigma _2\)).
 
8
TPTP’s general proof format [30] requires that the conclusion of an inference rule be a logical consequence of (or equi-satisfiable to) its premises. This limitation prevents an easy representation of natural deduction’s implication introduction rule, tableaux’s \(\beta \) rule or splitting. CR ’s conflict-driven clause learning is also affected by this limitation.
 
9
It is assumed (without loss of generality) that, for every i, \(\varGamma _i\) is actually used in \(\varphi _i\). Otherwise, if \(\varGamma _j\) were not used in \(\varphi _j\) for some j, \(\varphi _j\) would already be a refutation of S, and it would not be necessary to split \(\varGamma _1 \vee \ldots \vee \varGamma _k\).
 
10
It may be reused many times, since \(\varphi _i\) does not need to be tree-like.
 
11
Although antecedents of sequents and a Sat-solver’s trail resemble each other, as both store decision literals, they are not quite the same thing. Whereas a Sat-solver’s trail is typically a global structure, each sequent’s antecedent is local and stores only the decisions that have been necessary to derive the sequent’s succedent.
 
Literature
1.
Alagi, G., Weidenbach, C.: Non-redundant clause learning. In: FroCoS, pp. 69–84 (2015)
2.
Beth, E.W.: Semantic entailment and formal derivability. In: Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde 18(13), 309–342 (1955)
3.
Bachmair, L., Ganzinger, H.: Completion of first-order clauses with equality by strict superposition (Extended Abstract). In: 2nd International Workshop Conditional and Typed Rewriting Systems, LNCS 516, pp. 162–180. Springer, Berlin (1990)
4.
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)MathSciNetCrossRefMATH
5.
Baumgartner, P.: A first order Davis-Putnam-Longeman-Loveland procedure. In: Proceedings of the 17th International Conference on Automated Deduction (CADE), pp. 200–219 (2000)
6.
Baumgartner, P.: Model evolution based theorem proving. IEEE Intel. Syst. 29(1), 4–10 (2014)CrossRef
7.
Baumgartner, P., Tinelli, C.: The model evolution calculus. In: CADE, pp. 350–364 (2003)
8.
Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma learning in the model evolution calculus. In: LPAR, pp. 572–586 (2006)
9.
Biere, A.: PicoSAT Essentials. JSAT 4(2–4), 75–97 (2008)
10.
Bonacina, M.P.: Plaisted, DA.: SGGS theorem proving: an exposition. In: Schulz, S., de Moura, L., Konev, B. (eds.) 4th Workshop on Practical Aspects of Automated Reasoning, PAAR@IJCAR 2014, Vienna, Austria, 2014, vol. 31, pp. 25–38. EasyChair (2014)
11.
Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reason. 56(2), 113–141 (2016)
12.
Brown, CE.: Satallax: An automatic higher-order prover. In: IJCAR, pp. 111–117 (2012)
13.
Brown, CE.: Reducing higher-order theorem proving to a sequence of SAT problems. J. Autom. Reason. 51(1), 57–77 (2013)
14.
Claessen, K.: The anatomy of equinox—an extensible automated reasoning tool for first-order logic and beyond (Talk Abstract). In: Proceedings of the 23rd International Conference on Automated Deduction (CADE-23), pp. 1–3 (2011)
15.
16.
17.
de Nivelle, H., Meng, J.: Geometric resolution: a proof procedure based on finite model search. In: 3rd International Joint Conference on Automated Reasoning (IJCAR), pp. 303–317 (2006)
18.
Gentzen, G.: Untersuchungen über das logische Schließen I & II. Math. Z. 39(1), 176–210, 405–431 (1935)
19.
Barbosa, H., Fontaine, P.: Congruence closure with free variables (Work in Progress). In: 2nd International Workshop on Quantification (2015)
20.
Korovin, K.: iProver—an instantiation-based theorem prover for first-order logic (system description)”. In: International Joint Conference on Automated Reasoning (IJCAR), pp. 292–298 (2008)
21.
Korovin, K.: Inst-gen—a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics, vol. 7797, pp. 239–270. Springer, Berlin (2013)
22.
Marques-Silva, J., Sakallah, K.A.: GRASP—a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design, pp. 220–227 (1996)
23.
Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 127–149 (2008)
24.
McCharen, J., Overbeek, R., Wos, L.: Complexity and related enhancements for automated theorem-proving programs. Comput. Math. Appl. 2, 1–16 (1976)MATH
25.
26.
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2–3), 91–110 (2002)MATH
27.
28.
Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order thories with equality. Mach. Intell. 4, 135–150 (1969)MATH
29.
Schultz, S.: System description: E 1.8. In: LPAR, pp. 735–743 (2013)
30.
Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337–362 (2009)MathSciNetCrossRefMATH
31.
Voronkov, A.: AVATAR: The architecture for first-order theorem provers. In: CAV, pp. 696–710 (2014)
32.
Waldmann, U.: Superposition. In: Paleo, B.W. (eds.) Towards an Encyclopaedia of Proof Systems, p. 29. College Publications, London, UK (2017)
33.
Waldmann, U.: Saturation with redundancy. In: Paleo, B.W. (eds.) Towards an Encyclopaedia of Proof Systems, p. 30. College Publications, London, UK (2017)
34.
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965–2013. Elsevier and MIT Press (2001)
35.
Weidenbach, C.: The Theory of SPASS version 2.0. In: SPASS 2.0 documentation
36.
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: CADE, pp. 140–145 (2009)
37.
Wetzler, N., Heule, M., Hunt Jr, WA.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: SAT, pp. 422–429 (2014)
38.
Zhang, L., Madigan, CF., Moskewicz, MH., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: International Conference on Computer-Aided Design, pp. 279–285 (2001)
Metadata
Title
Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning
Authors
John Slaney
Bruno Woltzenlogel Paleo
Publication date
24-02-2017
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 2/2018
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-017-9408-6

Other articles of this Issue 2/2018

Journal of Automated Reasoning 2/2018 Go to the issue

OriginalPaper

Many-Sorted Equivalence of Shiny and Strongly Polite Theories

OriginalPaper

A Formalization of Metric Spaces in HOL Light

OriginalPaper

Visibly Linear Temporal Logic

OriginalPaper

Genetic Programming Proof Search Automatic Improvement

Premium Partner

    Image Credits