Scavenger 0.1: A Theorem Prover Based on Conflict Resolution

2017/04/11 by Daniyar Itegulov, Itegulov, Daniyar, John Slaney +3
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1704.03275

openalex publication_date 2017/04/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

This paper introduces Scavenger, the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.

Related

• Conflict Resolution: a First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning
• SCL(EQ): SCL for First-Order Logic with Equality
• On CDCL-based proof systems with the ordered decision strategy
• SCL(FOL) Revisited
• First-Order Logic Theorem Proving and Model Building via Approximation\n and Instantiation