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

DOI10.1007/S10817-017-9408-6zbMATH Open1425.68379arXiv1602.04568OpenAlexW2952307256MaRDI QIDQ682374FDOQ682374

Authors: Bruno Woltzenlogel Paleo, John K. Slaney 

Publication date: 2 February 2018

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

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.

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

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

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)

Cites Work

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

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

Uses Software

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

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)