Scavenger 0.1: A Theorem Prover Based on Conflict Resolution

April 11, 2017 · The Ethereal · 🏛 CADE

🔮 THE ETHEREAL: The Ethereal
Pure theory — exists on a plane beyond code

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Daniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo arXiv ID 1704.03275 Category cs.LO: Logic in CS Cross-listed cs.AI, cs.FL Citations 7 Venue CADE Last Checked 5 months ago
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.
Community shame:
Not yet rated
📄 View on arXiv 🌐 View on ar5iv 📑 PDF 🎉 Report Code Found
Community Contributions

Found the code? Know the venue? Think something is wrong? Let us know!

📜 Similar Papers

In the same crypt — Logic in CS