]> matita.cs.unibo.it Git - helm.git/tree - helm/software/components/ng_paramodulation/
Active goals are now demodulated after selecting a positive clause.
[helm.git] / helm / software / components / ng_paramodulation /
drwxr-xr-x   ..
-rw-r--r-- 1441 .depend
-rw-r--r-- 1441 .depend.opt
-rw-r--r-- 303 Makefile
-rw-r--r-- 1398 cicBlob.ml
-rw-r--r-- 911 cicBlob.mli
-rw-r--r-- 1599 foSubst.ml
-rw-r--r-- 1276 foSubst.mli
-rw-r--r-- 2814 foUnif.ml
-rw-r--r-- 1086 foUnif.mli
-rw-r--r-- 4726 foUtils.ml
-rw-r--r-- 2108 foUtils.mli
-rw-r--r-- 3281 index.ml
-rw-r--r-- 1289 index.mli
-rw-r--r-- 2773 nCicBlob.ml
-rw-r--r-- 918 nCicBlob.mli
-rw-r--r-- 6887 orderings.ml
-rw-r--r-- 1041 orderings.mli
-rw-r--r-- 7106 paramod.ml
-rw-r--r-- 146 paramod.mli
-rw-r--r-- 3934 pp.ml
-rw-r--r-- 1012 pp.mli
-rw-r--r-- 13787 superposition.ml
-rw-r--r-- 2029 superposition.mli
-rw-r--r-- 1965 terms.ml
-rw-r--r-- 2454 terms.mli