arxivst stuff from arxiv that you should probably bookmark

Scavenger 0.1: A Theorem Prover Based on Conflict Resolution

Abstract · Apr 11, 2017 13:11 ·

calculus logic solvers conflict sat conflict propositional resolution section cs-lo cs-ai cs-fl

Arxiv Abstract

  • Daniyar Itegulov
  • John Slaney
  • Bruno Woltzenlogel Paleo

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.

Read the paper (pdf) »