The Incredible Logic Tool

Usage

The main window

here you can do everything you want to do on your way to model-building and call clause-evaluation.

File

You can create a new problem-file or open an existing one.

Edit

Of course you can add, edit or remove a component (clause, formula, comment) to/from the file.

Add component

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.

Edit component

With 'Edit component' you can edit the selected component of the file.

Remove component

'Remove component' removes the selected component of the file.

Tools

Available tools are:

• convert
• classify
• run SPASS
• run Otter
• build a model
• evaluate a clause

Convert:

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.

Classify

The file is checked for the classes pvd and pvd-equal. Possibly the literals have to be renamed.

Run SPASS

This calls SPASS with the flags set in 'Flag Settings'

Run Otter

This calls Otter with the flags set in 'Flag Settings'

Build model

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

'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.

SetFlags

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.

SPASS

Here you can set all SPASS-flags. 'Load Standard' loads the flag-setting used by 'Build model'.

Otter

Here you can set all Otter-flags. 'Load Standard' loads the otter-default setting.

Mode

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.

Preferences

You can set the directories used.

Directory

You can set following directories:

• 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

with OK you accept the setting.