Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
Slaney J., Woltzenlogel Paleo B. Journal of Automated Reasoning60 (2):133-156,2018.Type:Article
Date Reviewed: Jul 3 2018

This work introduces the conflict resolution calculus (CR), which is shown to use unification “to generalize conflict-driven clause learning,” and an intermediary calculus, clausal natural deduction (CND). It proves the following:

  • Theorem 1: CR simulates resolution
  • Theorem 2: refutation is always possible in CR; and
  • Theorem 3: CND simulates CR.

With these tools CR is shown to be capable of splitting, and therefore can be written sequentially, thus potentially becoming useful for theorem proving of first-order models. The work is written from a theoretical, albeit practically driven, perspective. Current SAT solvers, such as Equinox, iProver, and AVATAR, are compared with regard to attack variables and implication elimination, where satisfiability is known to be NP-complete. Results suggest that CR might finally lead to “the first-order case through unification.”

The paper does not explore how to implement CR, which would be an important branch of future work.

I strongly recommend this paper to SAT solver researchers and to students willing to read a survey paper about the foundations of SAT solvers and alternative propositions, either using variables or parameters in propositional calculus.

Reviewer:  Arturo Ortiz-Tapia Review #: CR146122 (1809-0513)
Bookmark and Share
  Featured Reviewer  
 
Mathematical Logic (F.4.1 )
 
 
Deduction And Theorem Proving (I.2.3 )
 
Would you recommend this review?
yes
no
Other reviews under "Mathematical Logic": Date
Fundamentals of computing for software engineers
Tanik M. (ed), Chan E., Van Nostrand Reinhold Co., New York, NY, 1991. Type: Book (9780442005252)
Aug 1 1992
Fuzzy sets and fuzzy logic
Gottwald S., Friedr. Vieweg & Sohn Verlagsgesellschaft mbH, Wiesbaden, Germany, 1993. Type: Book (9783528053116)
Apr 1 1994
Logics of time and computation
Goldblatt R., Center for Study of Lang. and Info., Stanford, CA, 1987. Type: Book (9789780937073124)
Feb 1 1988
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy