Re: [isabelle] union-find based unification
I have an efficient first-order unification algorithm in Imperative HOL
in my shelf (from back in 2009).
I was mainly interested in using Imperative HOL and what the problems in
larger developments are with the Imperative HOL framework.
Also, we used that as case study for the partial function prototype in 2010.
However, I never found time to polish the proofs and make that work
If you are interested, we can discuss if the unpolished development is
of any use for you.
On 03/22/2013 06:03 AM, Christian Sternagel wrote:
is anybody aware of an Isabelle/HOL (or even better Imperative_HOL)
formalization of a union-find data structure for which also code can
be generated? I found
which mentions union-find trees in the introduction, but by skimming
over the theory names nothing immediately jumped at me ;)
The reason I ask is for an efficient (code generatable) formalization,
using union-find, of a first-order unification algorithm. Anybody
aware that this was already done?
This archive was generated by a fusion of
Pipermail (Mailman edition) and