# Scavenger 0.1: A Theorem Prover Based on Conflict Resolution

## TL;DR

Scavenger 0.1 is a novel first-order logic theorem prover utilizing conflict resolution calculus, combining unit propagation, decision literals, and conflict-driven clause learning to enhance proof search efficiency.

## Contribution

It introduces the first theorem prover based on conflict resolution calculus for pure first-order logic without equality, integrating new inference rules.

## Key findings

- Demonstrates the effectiveness of conflict resolution in first-order theorem proving
- Provides a new framework combining unit propagation and clause learning
- Shows potential improvements over traditional methods

## 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.