Philip Zucker • 5/17/2026

Reading Proof Objects and Completed Rewrite Systems from eprover into Knuckledragger

This article explores using the eprover theorem prover as a Knuth-Bendix completion engine to generate oriented rewrite systems from equational theories. It describes how to invoke eprover with options like --print-saturated and --print-oriented-eqlits-as-rules, and how the resulting rewrite rules can be processed using Prolog (via scryerpy) and integrated into the Knuckledragger proof assistant. The author demonstrates with a group theory example and discusses connections to egraphs and modulo theories.

0 comments

#Prolog #Eprover #Superposition Theorem Proving