Diffusion afp-devel ffe08eacc6fb

provide more unification algorithms, e.g., to compute mgu's modulo variable…
ffe08eacc6fb
Actions

Tags

None

Subscribers

None

Description

provide more unification algorithms, e.g., to compute mgu's modulo variable renamings

Details

Provenance

Rene Thiemann <rene.thiemann@uibk.ac.at>

Authored on

Parents

rAFP56b9fc8ccf14: Adapted to devel

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPffe08eacc6fb: provide more unification algorithms, e.g., to compute mgu's modulo variable….Aug 9 2023, 3:33 PM

Changes (10)

Path

Size

First_Order_Terms

Lists_are_Infinite.thy

Renaming2_String.thy

Unification.thy

Unification_String.thy

Regular_Tree_Relations/

Util/

Term_Context.thy

rAFPffe08eacc6fb

thys/First_Order_Terms/Lists_are_Infinite.thy

Loading...

thys/First_Order_Terms/ROOT

Loading...

thys/First_Order_Terms/Renaming2.thy

Loading...

thys/First_Order_Terms/Renaming2_String.thy

Loading...

thys/First_Order_Terms/Term.thy

Loading...

thys/First_Order_Terms/Unification.thy

Loading...

thys/First_Order_Terms/Unification_String.thy

Loading...

thys/Regular_Tree_Relations/Util/Term_Context.thy

Loading...