helm/software/components/tactics/paramodulation/README

   1 make saturate per compilare l'eseguibile da riga di comando (make saturate.opt per la versione ottimizzata)
   2
   3 ./saturate -h per vedere una lista di parametri:
   4
   5 ./saturate: unknown option `-h'.
   6 Usage:
   7   -full Enable full mode
   8   -f Enable/disable full-reduction strategy (default: enabled)
   9   -r Weight-Age equality selection ratio (default: 4)
  10   -s symbols-based selection ratio (relative to the weight ratio, default: 0)
  11   -c Configuration file (for the db connection)
  12   -o Term ordering. Possible values are:
  13         kbo: Knuth-Bendix ordering
  14         nr-kbo: Non-recursive variant of kbo (default)
  15         lpo: Lexicographic path ordering
  16   -l Time limit in seconds (default: no limit)
  17   -w Maximal width (default: 3)
  18   -d Maximal depth (default: 3)
  19   -retrieve retrieve only
  20   -help  Display this list of options
  21   --help  Display this list of options
  22
  23
  24 ./saturate -l 10 -demod-equalities
  25
  26 dove -l 10 e` il timeout in secondi.
  27
  28 Il programma legge da standard input il teorema, per esempio
  29
  30 \forall n:nat.n + n = 2 * n
  31 \forall n:R.n + n = 2 * n
  32 \forall n:R.n+n=n+n
  33
  34 l'input termina con una riga vuota (quindi basta un doppio invio alla fine)
  35
  36 In output, oltre ai vari messaggi di debug, vengono stampati gli insiemi
  37 active e passive alla fine dell'esecuzione. Consiglio di redirigere l'output
  38 su file, per esempio usando tee:
  39
  40 ./saturate -l 10 -demod-equalities | tee output.txt
  41
  42 Il formato di stampa e` quello per gli oggetti di tipo equality (usa la
  43 funzione Inference.string_of_equality)
  44
  45