X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2FREADME;fp=helm%2Focaml%2Fparamodulation%2FREADME;h=98deef5ad7af639833fcbe8c61fdd7397b777911;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hp=0000000000000000000000000000000000000000;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953;p=helm.git

diff --git a/helm/ocaml/paramodulation/README b/helm/ocaml/paramodulation/README
new file mode 100644
index 000000000..98deef5ad
--- /dev/null
+++ b/helm/ocaml/paramodulation/README
@@ -0,0 +1,43 @@
+make saturate per compilare l'eseguibile da riga di comando (make saturate.opt per la versione ottimizzata)
+
+./saturate -h per vedere una lista di parametri:
+
+./saturate: unknown option `-h'.
+Usage:
+  -full Enable full mode
+  -f Enable/disable full-reduction strategy (default: enabled)
+  -r Weight-Age equality selection ratio (default: 4)
+  -s symbols-based selection ratio (relative to the weight ratio, default: 0)
+  -c Configuration file (for the db connection)
+  -o Term ordering. Possible values are:
+        kbo: Knuth-Bendix ordering
+        nr-kbo: Non-recursive variant of kbo (default)
+        lpo: Lexicographic path ordering
+  -l Time limit in seconds (default: no limit)
+  -w Maximal width (default: 3)
+  -d Maximal depth (default: 3)
+  -retrieve retrieve only
+  -help  Display this list of options
+  --help  Display this list of options
+
+
+./saturate -l 10 -demod-equalities
+
+dove -l 10 e` il timeout in secondi.
+
+Il programma legge da standard input il teorema, per esempio
+
+\forall n:nat.n + n = 2 * n
+
+l'input termina con una riga vuota (quindi basta un doppio invio alla fine)
+
+In output, oltre ai vari messaggi di debug, vengono stampati gli insiemi
+active e passive alla fine dell'esecuzione. Consiglio di redirigere l'output
+su file, per esempio usando tee:
+
+./saturate -l 10 -demod-equalities | tee output.txt
+
+Il formato di stampa e` quello per gli oggetti di tipo equality (usa la
+funzione Inference.string_of_equality)
+
+