2026-07-22T10:45:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20740 2024-11-27T23:17:38Z ddc:004 open_access

A Modular Formalization of Superposition in Isabelle/HOL Desharnais, Martin Toth, Balazs Waldmann, Uwe Blanchette, Jasmin Tourret, Sophie Superposition verification first-order logic higher-order logic Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers. It works by saturating the given set of clauses and is refutationally complete, meaning that if the set is inconsistent, the saturation will contain a contradiction. In this work, we restructured the completeness proof to cleanly separate the ground (i.e., variable-free) and nonground aspects, and we formalized the result in Isabelle/HOL. We relied on the IsaFoR library for first-order terms and on the Isabelle saturation framework. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Martin Desharnais and Balazs Toth and Uwe Waldmann and Jasmin Blanchette and Sophie Tourret 2024 Is Part Of LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2024.12 urn:nbn:de:0030-drops-207401 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.12 eng https://creativecommons.org/licenses/by/4.0/legalcode