This is work in progress and not a release version - please do not hesitate to contact me if you cannot get it to work, have special questions, a bug report or want to contribute. You can change and distribute the software for research purposes under the usual academic rules if you provide me with the improvements you obtain.
| sources.cm | File to be passed to SML/NJ's compilation manager to load all files |
| main.sml | The main part of the routines |
| strategies_provers.sig | Interfaces between modules. |
| strategies.sml | The main code is parametric in strategies. |
| provers.sml | The strategies are parametric in provers. |
| tptp.sml | Auxiliary code for TPTP syntax |
| modal.sml | Auxiliary code for modal logic |
| rules.sml | Auxiliary code that reads the file axioms_and_rules.tptp and provides functions to refer to its content |
| axioms_and_rules.tptp | A list of standard axioms and rules |
| utils.sml | Auxiliary code containing various utilities |
| regexp.sml | Auxiliary code to deal with regular expressions because the SML/NJ syntax is terrible. |
| definitions.tptp | Basic definitions of the connectives. |
| pc_big.tptp | The big expansion of the special rule pc |
| pc_small.tptp | The small expansion of the special rule pc |
| definitions_kripke.tptp | Definitions passed to a model finder by the Kripke strategy. |
| scan_main.pl | The main Scan sript |
| operators.pl | An auxiliary Scan script |
| scan.pl | An auxiliary Scan script |
| Scan | The Scan executable for SunOS/Solaris (called by the main script) |
| big.tptp | An example input file |
| small.tptp | An example input file |
| scan_db.txt | A file containing the most common calls to Scan and its output if you don't have Solaris or want to skip the Scan calls. Whether this file is used, is determined by the variable Scan.dblookup : boolean ref |
The program is supposed to call SCAN, which is included but requires Solaris to run; for simplicity, the current program outputs the command line to call SCAN with and expects to be copy-pasted back Scan's output. SCAN requires Prolog; its directory and a path to Prolog have to be set in the variables $path and $FORM{'prolog'} in scan_main.pl. The inclusion of the slightly adapted SCAN files occurs with permission of the developers of SCAN.
Syntax used to call vampire: ./vampire --mode casc -t [time] temp_input.tptp > temp_output
Syntax used to call paradox: ./paradox --sizes [n] --model temp_model temp_input.tptp > temp_output
Syntax used to call Scan: e.g. ./scan_main.pl "imp(box(X),X)" "X"
A typical SML start-up looks like this:
> cd moloss directory
> sml
- CM.make("sources.cm");
- Main.compare("small.tptp","big.tptp");
Alternatively, you can compare sets of hard-coded axiomatizations by
- Main.compare_many(from, to, oracle);
where from and to are lists of axiomatizations as defined in rules.sml. For example, from=[Rules.K] and to=[Rules.S10,Rules.S1] tries to derive S1 and S10 from K. oracle is a boolean that can be set to true to use an oracle that skips the proving attempts and jumps to disproving attempts immediately. If from or to is nil, it is replaced with the list of 11 axiomatizations, we used as examples. For example, you would call
- Main.compare_many(nil,nil,false);
to recreate our test suite.
If you want to switch off strategies, you can uncomment them in the definitions of incl_strategies and nonincl_strategies in main.sml.
During execution, before every external call, the program will display the following menu.
**External call
[command line]
in attempt to prove [TPTP formula]
s: skip with success
f: skip with failure
r=x: success with result x
a: run and do not ask anymore
other: run
Its semantics is:
| s/f | Skip the external call, assume the proof succeeded/failed. (This is helpful, if only certain parts of the search are interesting.) |
| r=x | Skip the external call, assume the action succeeded and assume x to be the returned result. (This is necessary to supply the results of Scan if the program is not run on a Solaris machine. It is also possible to use the entries of scan_db.txt.) |
| a | Run this external call and run all following ones automatically. |
| other | Run this external call and display this menu again next time. |
Some log, success and failures notes are displayed during execution. The complete output including the proof objects and models returned by the external calls will be output at the end. A logfile is set by calling Output.init(file) where file is a filename (Existing file will be deleted.). Output verbosity is controlled by Output.verboselevel_display : int ref and Output.verboselevel_logfile : int ref which must have values below 5 if you do not want to see the full output returned by the external tools.