The Incredible Logic Tool
The main window
here you can do everything you want to do on your way to model-building and call clause-evaluation.
You can create a new problem-file or open an existing one.
Of course you can add, edit or remove a component (clause, formula, comment) to/from the file.
Depending on the fileformat you can add different objects to the file. For instance you can add a clause-, comment-, include- or an other object to a tptp-clauses-file.
With 'Edit component' you can edit the selected component of the file.
'Remove component' removes the selected component of the file.
Available tools are:
- run SPASS
- run Otter
- build a model
- evaluate a clause
Depending on the file-format different conversions are available
TPTP 2 Dfg / TPTP 2 Otter
Here you can set all tptp2X-flags, save or load them. Cancel closes the window, start calls tptp2X with the given flags.
DFG 2 CNF
Here you can set all Flotter-flags, save or load them. Cancel closes the window, start calls Flotter with the given flags.
The file is checked for the classes pvd and pvd-equal. Possibly the literals have to be renamed.
This calls SPASS with the flags set in 'Flag Settings'
This calls Otter with the flags set in 'Flag Settings'
Depending on the mode you choose 'Build model' does different things:
- Automatic-Mode: 'Build model' test if the problem lies in the classes pvd or pvd-equal. Depending on the result either model-bulding using SPASS or Otter is started.
- Standard (Otter): model-building is done using the standard algorithm presented bei Fermüller/Leitsch. First the algorithm using otter is invoked. Then a finite model is generated. From this finite model the final ARM is extracted.
- Experimantal (SPASS): model-building is done using SPASS. First SPASS is called, then a finite model is generated. From this finite model the final ARM is extracted.
- 'Choose interactively': here you can choose between the two available algorithms. If you choose the standard algorithm, the flags set in 'Set Flags' are not considered. If you choose SPASS, the set SPASS-Flags are used.
'Evaluate Clause' opens an independant window.
Here you can load or save models and sets of clauses which should be evaluated, or you can add, edit and delete single clauses:
When you push the 'check'-button all clauses listed in 'Clauses' are evaluated one after another.
Here you can set the Flags for SPASS or Otter. The flag-settings are inly applied with 'Run SPASS' or 'Run Otter'. They have no effect on 'Build model'.
Both Windows for Flag-Setting have a Setting-Menu, which allows you to load and save the flag-setting, load the standard-setting and cancel and accept the changes.
Here you can set all SPASS-flags. 'Load Standard' loads the flag-setting used by 'Build model'.
Here you can set all Otter-flags. 'Load Standard' loads the otter-default setting.
Tilt has four different modes
- In the first three (Automatic, Standard and Experimantal) only the tools 'Build model' and 'Evaluate clause' are available:
- In the fourth mode (Choose interactively) all tools are available: here you can convert the file, classify it, run SPASS or Otter and set their flags, build the model and evaluate clauses.
You can set the directories used.
You can set following directories:
with OK you accept the setting.
- Main - directory for generated files
- Classify - directory for prolog-files used for classification
- Clause Evaluation - directory for prolog-files used clause evaluation
- Finite Model - directory for prolog-files used to generate to build the ARM
- Experimental part - directory for prolog-files used for modelbuilding in connection with SPASS
- Standard Part - directory for prolog-files used for modelbuilding in connection with Otter
- Source - Python files (interface)
- SPASS - directory to save the SPASS-flag-settings
- Flotter - directory to save the Flotter-flag-settings
- Otter - directory to save the Otter-flag-settings
- TPTP2X - directory to save the TPTP2X-flag-settings
- Models - directory to save the models to
- Clauses - directory to save the clause-sets to
Last modified: Mon Feb 19 14:24:36 CET 2001