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

DOI10.1007/s10817-017-9408-6zbMath1425.68379arXiv1602.04568OpenAlexW2952307256MaRDI QIDQ682374

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

automated reasoningproof theorynatural deductionresolutionmathematical logicconflict-driven clause learning

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Semantically-guided goal-sensitive reasoning: model representation
• Complexity and related enhancements for automated theorem-proving programs
• Untersuchungen über das logische Schliessen. I
• Reducing higher-order theorem proving to a sequence of SAT problems
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• System Description: E 1.8
• Satallax: An Automatic Higher-Order Prover
• AVATAR: The Architecture for First-Order Theorem Provers
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• The Anatomy of Equinox – An Extensible Automated Reasoning Tool for First-Order Logic and Beyond
• Lemma Learning in the Model Evolution Calculus
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Completion of first-order clauses with equality by strict superposition
• Automated Deduction – CADE-19