Scavenger 0.1: A Theorem Prover Based on Conflict Resolution
This addresses the need for efficient theorem provers in logic and AI, representing a foundational advancement rather than an incremental improvement.
The paper tackles the problem of automated theorem proving for pure first-order logic without equality by introducing Scavenger, the first theorem prover based on the conflict resolution calculus, achieving a novel approach in this domain.
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.