zbMATH — the first resource for mathematics

Scavenger 0.1: a theorem prover based on conflict resolution. (English) Zbl 06778413
de Moura, Leonardo (ed.), Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-63045-8/pbk; 978-3-319-63046-5/ebook). Lecture Notes in Computer Science 10395. Lecture Notes in Artificial Intelligence, 344-356 (2017).
Summary: 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.
For the entire collection see [Zbl 1369.68037].

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI