package coq-founify
Correctness and extraction of the unification algorithm
Install
Dune Dependency
Authors
Maintainers
Sources
v8.5.0.tar.gz
md5=ec3d9574e75f256b580cc4faf2d11a9a
Description
A notion of terms based on symbols without fixed arities is defined and an extended unification problem is proved solvable on these terms. An algorithm, close from Robinson algorithm, can be extracted from the proof.
On This Page