Scavenger 0.1: A Theorem Prover Based on Conflict Resolution
Logic in Computer Science
2017-11-01 v2 Artificial Intelligence
Formal Languages and Automata Theory
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.
Keywords
Cite
@article{arxiv.1704.03275,
title = {Scavenger 0.1: A Theorem Prover Based on Conflict Resolution},
author = {Daniyar Itegulov and John Slaney and Bruno Woltzenlogel Paleo},
journal= {arXiv preprint arXiv:1704.03275},
year = {2017}
}
Comments
Published at CADE 2017