]> matita.cs.unibo.it Git - helm.git/commit - helm/software/components/ng_paramodulation/paramod.ml
Implemented handling of Invertible equalities
authordenes <??>
Tue, 21 Jul 2009 15:38:17 +0000 (15:38 +0000)
committerdenes <??>
Tue, 21 Jul 2009 15:38:17 +0000 (15:38 +0000)
commit5642a453e8b4bbe228d126aa0c44d31e101969ec
treeadbb6a65439bd691decb4ea762bd0d3bba03bac3
parent50b3acd4b20269cf615bb297262f0238cc8e692a
Implemented handling of Invertible equalities
Fixed nasty bug in inferences for Incomparable equalities
helm/software/components/ng_paramodulation/index.ml
helm/software/components/ng_paramodulation/orderings.ml
helm/software/components/ng_paramodulation/paramod.ml
helm/software/components/ng_paramodulation/pp.ml
helm/software/components/ng_paramodulation/superposition.ml
helm/software/components/ng_paramodulation/terms.ml
helm/software/components/ng_paramodulation/terms.mli