Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning

DOI10.1007/S10817-017-9408-6MaRDI QIDQ682374zbMATH OpenOpenAlexFDO

Authors Bruno Woltzenlogel Paleo, John K. Slaney

Publication date 2 February 2018

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1602.04568

zbMATH Keywords

proof theoryresolutionnatural deductionautomated reasoningmathematical logicconflict-driven clause learning

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mechanization of proofs and logical operations (03B35)

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 is restricted to (first-order) unit-propagation and the calculus is extended with a mechanism for assuming decision literals and a new inference rule for clause learning, which is a first-order generalization of the propositional conflict-driven clause learning (CDCL) 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.

Recommendations

• Towards causality-based conflict resolution in answer set programs
• Learning from conflicts in propositional satisfiability
• Conflict-driven answer set solving: from theory to practice
• Fine-grained conflict resolution in constraint satisfaction problems
• A resolution calculus for first-order schemata
• Formalization of the Resolution Calculus for First-Order Logic
• Formalization of the resolution calculus for first-order logic

Cites work

• scientific article; zbMATH DE number 1614697 (Why is no real title available?)
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 2090305 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• A machine program for theorem-proving
• AVATAR: The Architecture for First-Order Theorem Provers
• Combining superposition, sorts and splitting
• Completion of first-order clauses with equality by strict superposition
• Complexity and related enhancements for automated theorem-proving programs
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Lemma Learning in the Model Evolution Calculus
• Reducing higher-order theorem proving to a sequence of SAT problems
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Satallax: An Automatic Higher-Order Prover
• Semantically-guided goal-sensitive reasoning: model representation
• System description: E 1.8
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The anatomy of Equinox -- an extensible automated reasoning tool for first-order logic and beyond (talk abstract)
• The model evolution calculus.
• Untersuchungen über das logische Schliessen. I
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)

Cited in

(5)

• Scavenger 0.1: a theorem prover based on conflict resolution
• Deciding floating-point logic with abstract conflict driven clause learning
• A resolution calculus for first-order schemata
• Automated reasoning building blocks
• NRCL -- a model building approach to the Bernays-Schönfinkel fragment

Describes a project that uses

Uses Software

• AVATAR
• DRAT-trim
• Equinox
• iProver
• PicoSAT
• Satallax
• Prover9
• Darwin
• TPTP
• SPASS
• VAMPIRE

This page was built for publication: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q682374)