A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
Martin Bromberger, Martin Desharnais, Christoph Weidenbach · Lecture notes in computer science · 2025
Abstract Recently, it has been demonstrated that SCL(FOL) can simulate ground ordered resolution [6]. We revisit this result and provide a new formal proof in Isabelle/HOL. The existing pen-and-paper proof is monolithic and challenging to comprehend. In order to improve clarity, we develop an alternative proof structured as eleven (bi)simulation steps between the two calculi, transitioning from ordered resolution to SCL(FOL). A key simulation lemma ensures that, under certain conditions, one simulation direction can be automatically lifted to the other. Consequently, for each of the eleven steps, it suffices to establish only one direction of simulation. The complete proof is included in the "Image missing" .