]> matita.cs.unibo.it Git - helm.git/commit
matitaprover is now flexible enough to allow the computation of statistics on
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 13 Jul 2009 08:56:24 +0000 (08:56 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 13 Jul 2009 08:56:24 +0000 (08:56 +0000)
commit72aa8b2087285826b14fc39a389632f0317c51b6
treec868b28554a8b18c30cae33aa828f9acf8b70b74
parentc83721701dbbd44d3d547fdec6c4a5658322f424
matitaprover is now flexible enough to allow the computation of statistics on
the clauses and then choose an ordering to be used for the proof search
helm/software/components/binaries/matitaprover/matitaprover.ml
helm/software/components/ng_paramodulation/paramod.ml
helm/software/components/ng_paramodulation/paramod.mli