Simplified and verified: a second look at a proof-producing union-find algorithm

DOI10.1007/978-3-031-99984-0_15MaRDI QIDQ6869949zbMATH OpenFDO

Authors Lukas Stevens, Rebecca Ghidini

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_15

zbMATH Keywords

satisfiability modulo theoriesinteractive theorem provingequivalence closureproof-producing decision procedure

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 3511563 (Why is no real title available?)
• scientific article; zbMATH DE number 7649969 (Why is no real title available?)
• A graph library for Isabelle
• A verified decision procedure for orders in Isabelle/HOL
• An improved equivalence algorithm
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Efficiency of a Good But Not Linear Set Union Algorithm
• Fast congruence closure and extensions
• Faster, higher, stronger: E 2.3
• Imperative Functional Programming with Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• On the shortest spanning subtree of a graph and the traveling salesman problem
• Refinement to imperative HOL
• Simplification by Cooperating Decision Procedures
• Term Rewriting and Applications
• Types for Proofs and Programs
• Verified Textbook Algorithms
• Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Worst-case Analysis of Set Union Algorithms

This page was built for publication: Simplified and verified: a second look at a proof-producing union-find algorithm

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