Email Gateway (Nov 04 2024 at 15:11): Email Gateway (Nov 04 2024 at 15:11):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
Martin Desharnais has formalized another impressive and recent automated reasoning result: a tight relationship between two seemingly rather different calculi for first-order logic:
SCL Simulates Nonredundant Ground Resolution
by Martin Desharnais
SCL(FOL) (i.e., Simple Clause Learning for First-Order Logic without equality) is known to be able to simulate the derivation of nonredundant clauses by the ground ordered resolution calculus (see Bromberger et al. at CADE 2023). Due to the space constraints of a 16-pages paper, the published proof is monolithic and hard to comprehend. In this work, we reuse the existing strategy for ground ordered resolution and present a new, simpler strategy for SCL(FOL). We prove a stronger bisimulation theorem between these two strategies (i.e., they both simulate each other). Our proof is modular: it consists of ten refinement steps focusing on different aspects of the two strategies.
https://www.isa-afp.org/entries/SCL_Simulates_Ground_Resolution.html
Enjoy!
Dmitriy
Last updated: Jan 04 2025 at 20:18 UTC