Formalizing splitting in Isabelle/HOL

DOI10.4230/LIPICS.ITP.2025.22MaRDI QIDQ7323672zbMATH OpenFDO

Authors Ghilain Bergeron, Florent Krasnopol, Sophie Tourret

Publication date 1 September 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2025.22

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A comprehensive framework for saturation theorem proving
• A modular formalization of superposition in Isabelle/HOL
• A remark on method in transfinite algebra
• AVATAR: The Architecture for First-Order Theorem Provers
• Formalized proof systems for propositional logic
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• scientific article; zbMATH DE number 1301853 (Why is no real title available?)
• Labelled splitting
• Locales: a module system for mathematical theories
• Making higher-order superposition work
• Paramodulation-based theorem proving
• Resolution theorem proving
• Revisiting enumerative instantiation
• Unifying splitting

This page was built for publication: Formalizing splitting in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7323672)