Scavenger 0.1: A Theorem Prover Based on Conflict Resolution

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 restr…