Proof-Producing Congruence Closure in Isabelle/HOL

Description

Formalization and formal correctness proofs of the algorithms presented in the paper "Proof-Producing Congruence Closure" by Robert Nieuwenhuis and Albert Oliveras. It includes the explain operation for union-find, the congruence closure algorithm and the explain operation for congruence closure.

All formalizations and proofs are defined in the generic proof assistant Isabelle/HOL.

Dependencies

• Isabelle/HOL
• Theory Union_Find from the Archive of Formal Proofs