This is the command SPASS that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

**PROGRAM:**

**NAME**

SPASS - automated theorem prover for full first-order logic with equality

**SYNOPSIS**

SPASS [

**options**] [

__inputfile__]

**DESCRIPTION**

SPASS is an automated theorem prover for full sorted first-order logic with equality that

extends superposition by sorts and a splitting rule for case analysis. SPASS can also be

used as a modal logic and description logic theorem prover.

**OPTIONS**

Command line options in SPASS are implemented via modifications to the GNU command line

option package for C. Just giving the option sets its value to 1 and means enabling the

option. In order to disable an option the value has to be set to 0 by declaring -

__Option__=0.

The following options are currently supported by SPASS:

-Auto

Enables/disables the auto mode where SPASS configures itself automatically. The

inference/reduction rules, the sort technology, the ordering and precedence as well as

the splitting and selection strategy are set. In auto mode SPASS is complete. Mixing

the auto mode with user defined options may destroy completeness. Default is 1.

-Stdin

Enables/disables input in SPASS via stdin. The file argument is ignored. Default is 0.

-Interactive

Enables/disables the interactive mode. First, SPASS is given a set of axioms and then

the prover accepts subsequent proof tasks. Default is 0.

-Flotter

Enables/disables the CNF translation mode of SPASS. If the option is set, SPASS only

performs a clause normal form translation. If no output file argument is given SPASS

prints the CNF to stdout. Default is 0.

-SOS

Enables/disables the set of support strategy. Default is 0.

-Splits=

__n__

Sets the number of possible splitting applications to

__n__. If

__n__=-1 then the number of

splits is not limited. Default is 0.

-Memory=

__n__

Sets the amount of memory available to SPASS for the proof search to

__n__bytes. The

memory needed to startup SPASS cannot be restricted. Default is -1 meaning that

memory allocations is only restricted by available memory.

-TimeLimit=

__n__

Sets a time limit for the proof search to

__n__seconds. Default is -1 meaning that SPASS

may run forever. The time limit is polled when SPASS selects a new clause for

inferences. If a single inference step causes an explosion to the number of generated

clauses it may therefore happen that a given time limit is significantly exceeded.

-DocSST

Enables/disables documentation output for static soft typing. The used sort theory as

well as the (failed) proof attempt for the sort constraint is printed. Default is 0.

-DocProof

Enables/disables proof documentation. If SPASS finds a proof it is eventually printed.

If SPASS finds a saturation, the saturated set of clauses is eventually printed.

Enabling proof documentation may significantly decrease SPASS's performance, because

the prover must store clauses that can be thrown away otherwise. Default is 0.

-DocSplit

Sets the documentation of split backtracking steps. If set to 1, the current

backtracking level is printed. If set to 2, it also prints in case of a split

backtrack the backtracked clauese. Default is 0.

-Loops

Sets the maximal number of mainloop iterations for SPASS. Default is -1.

-PSub

Enables/disables printing of subsumed clauses. Default is 0.

-PRew

Enables/disables printing of simple rewrite applications. Default is 0.

-PCon

Enables/disables printing of condensation applications. Default is 0.

-PTaut

Enables/disables printing of tautology deletion applications. Default is 0.

-PObv

Enables/disables printing of obvious reduction applications. Default is 0.

-PSSi

Enables/disables printing of sort simplification applications. Default is 0.

-PSST

Enables/disables printing of static soft typing applications. All deleted clauses are

printed. Default is 0.

-PMRR

Enables/disables printing of matching replacement resolution applications. Default is

0.

-PUnC

Enables/disables printing of unit conflict applications. Default is 0.

-PAED

Enables/disables printing of clauses where redundant equations have been removed

(assignment equation deletion).

-PDer

Enables/disables printing of clauses derived by inferences. Default is 0.

-PGiven

Enables/disables printing of the given clause, selected to perform inferences.

Default is 0.

-PLabels

Enables/disables printing of labels. If the -DocProof is set and no labels for

formulae are provided by the input, SPASS generates generic labels that are then

printed by enabling this option. Default is 0.

-PKept

Enables/disables printing of kept clauses. These are clauses generated by inferences

(backtracking) that are not redundant. Clauses derived during input

reduction/saturation are not printed. Default is 0.

-PProblem

Enables/disables printing of the input clause set. Default is 1.

-PEmptyClause

Enables/disables printing of derived empty clauses. Default is 0.

-PStatistic

Enables/disables printing of a final statistics on derived/backtracked/kept clauses,

performed splits, used time and used space. Default is 1.

-FPModel

Enables/disables the output of an eventually found model to a file. If set to 1, all

clauses in the final set are printed. If set to 2, only potentially productive clauses

are printed, that are clauses with no selected negative literal and a maximal positive

one. If <problemfile> is the name of the input problem and the eventually generated

set is saturated, the saturation is printed to the file <problemfile>.model, for

otherwise to <problemfile>.clauses. The latter case may, e.g., be caused by a time

limit. Default is 0.

-FPDFGProof

Enables/disables the output of an eventually found proof to a file. Using this option

requires to set the option -DocProof. If <problemfile> is the name of the input

problem the proof is printed to <problemfile>.prf. Default is 0.

-PFlags

Enables/disables the output of all flag values. The flag settings are printed at the

end of a SPASS run in form of a DFG-Syntax input section. Default is 0.

-POptSkolem

Enables/disables the output of optimized Skolemization applications. Default is 0.

-PStrSkolem

Enables/disables the output of strong Skolemization applications. Default is 0.

-PBDC

Enables/disables the output of clauses deleted because of bound restrictions. Default

is 0.

-PBInc

Enables/disables the output of bound restriction changes. Default is 0.

-PApplyDefs

Enables/disables printing of expansions of atom definitions. Default is 0.

-Select

Sets the selection strategy for SPASS. If set to 0 no selection of negative literals

is done. If set to any other value, at most one negative literal in a clause is

selected. If set to 1 negative literals in clauses with more than one maximal literal

are selected. Either a negative literal with a predicate from the selection list (see

below) is chosen or if no such negative literal is available, a negative literal with

maximal weight is chosen. If set to 2 negative literals are always selected. Again,

either a negative literal with a predicate from the selection list (see below) is

chosen or if no such negative literal is available, a negative literal with maximal

weight is chosen. The latter case results in an ordered hyperresolution like behavior

of ordered resolution. If set to 3 any negative literal with a predicate specified by

the selection list (see below) is selected. Default is 1.

-RInput

Enables/disables the reduction of the initial clause set. Default is 1.

-Sorts

Determines the monadic literals that built the sort constraint for the initial clause

set. If set to 0, no sort constraint is built. If set to 1, all negative monadic

literals with a variable as argument form the sort constraint. If set to 2, all

negative monadic literals form the sort constraint. Setting -Sorts to 2 may harm

completeness, since sort constraints are subject to the basic strategy and to static

soft typing. Default is 1.

-SatInput

Enables/disables input saturation. The saturation is incomplete but is guaranteed to

terminate. Default is 0.

-WDRatio

Sets the ratio between given clauses selected by weight or the depth in the search

space. The weight is the sum of all symbol weights determined by the -FuncWeight and

-VarWeight options. The depth of all initial clauses is 0 and clauses generated by

inferences get the maximal depth of a parent clause plus 1. Default is 5, meaning

that 4 clauses are selected by weight and the fifth clause is selected by depth.

-PrefCon

Sets the ratio to compute the weight for conjecture clauses and therefore allows to

prefer those. Default is 0 meaning that the weight computation for conjecture clauses

is not changed.

-FullRed

Enables/disables full reduction. If set to 0, only the set of worked off clauses is

completely inter-reduced. If set to 1, all currently hold clauses (worked off and

usable) are completely inter-reduced. Default is 1.

-FuncWeight

Sets the weight of function/predicate symbols. The weight of clauses is the sum of all

symbol weights. This weight is considered for the selection of the given clause.

Default is 1.

-VarWeight

Sets the weight of variable symbols (see -FuncWeight). Default is 1.

-PrefVar

Enables/disables the preference for clauses with many variables. While clauses are

selected by weight, if this option is set and two clauses have the same weight, the

clause with more variable occurrences is preferred. Default is 0.

-BoundMode

Selects the mode for bound restrictions. Mode 0 means no restriction, if set to 1 all

newly generated clauses are restricted by weight (see -BoundStart) and if set to 2

clauses are restricted by depth. Default is 0.

-BoundStart

The start restriction of the selected bound mode. For example, if bound mode is 1 and

bound start set to 5, all clauses with a weight larger than 5 are deleted until the

set is saturated. This causes an increase of the used bound value that is determined

by the minimal increase saving a before deleted clause. Default is -1 meaning no bound

restriction.

-BoundLoops

The number of loops applying the actions restrictions/increasing bound. If the number

of loops is exceeded all bound restrictions are cancelled. Default is 1.

-ApplyDefs

Sets the maximal number of applications of atom definitions to input formulae.

Default is 0, meaning no applications at all.

-Ordering

Sets the term ordering. If 0 then KBO is selected, if 1 the RPOS is selected. Default

is 0.

-CNFQuantExch

If set, non-constant Skolem terms in the clausal form of the conjecture are replaced

by constants. Will automatically be set for the optimized functional translation of

modal or description logic formulae. Default is 0.

-CNFOptSkolem

Enables/disables optimized Skolemization. Default is 1.

-CNFStrSkolem

Enables/disables Strong Skolemization. Default is 1.

-CNFProofSteps

Sets the maximal number of proof steps in an optimized Skolemization proof attempt.

Default is 100.

-CNFSub

Enables/disables subsumption on the clauses generated by the CNF procedure. Default

is 1.

-CNFCon

Enables/disables condensing on the clauses generated by the CNF procedure. Default is

1.

-CNFRedTime

Sets the overall amount of time in seconds to be spend on reduction during CNF

transformation. Affected reductions are optimized Skolemization, condensing, and

subsumption. Default is -1 meaning that the reduction time is not limited at all.

-CNFRenaming

Enables/disables formula renaming. If set to 1 optimized renaming is enabled that

minimizes the number of eventually generated clauses. If set to 2 complex renaming is

enabled that introduces a new Skolem predicate for every complex formula, i.e., any

formula that is not a literal. If set to 3 quantification renaming is enabled that

introduces a new Skolem predicate for every subformula starting with a quantifier.

Default is 1.

-CNFRenMatch

If set, renaming variant subformulae are replaced by the same Skolem literal. Default

is 1.

-CNFPRenaming

Enables/disables the printing of formula renaming applications. Default is 0.

-CNFFEqR

Enables/disables certain equality reduction techniques on the formula level. Default

is 1.

-IEmS

Enables/disables the inference rule Empty Sort. Default is 0.

-ISoR

Enables/disables the inference rule Sort Resolution. Default is 0.

-IEqR

Enables/disables the inference rule Equality Resolution. Default is 0.

-IERR

Enables/disables the inference rule Reflexivity Resolution. Default is 0.

-IEqF

Enables/disables the inference rule Equality Factoring. Default is 0.

-IMPm

Enables/disables the inference rule Merging Paramodulation. Default is 0.

-ISpR

Enables/disables the inference rule Superposition Right. Default is 0.

-IOPm

Enables/disables the inference rule Ordered Paramodulation. Default is 0.

-ISPm

Enables/disables the inference rule Standard Paramodulation. Default is 0.

-ISpL

Enables/disables the inference rule Superposition Left. Default is 0.

-IORe

Enables/disables the inference rule Ordered Resolution. If set to 1, Ordered

Resolution is enabled but no resolution inferences with equations are generated. If

set to 2, equations are considered for Ordered Resolution steps as well. Default is

0.

-ISRe

Enables/disables the inference rule Standard Resolution. If set to 1, Standard

Resolution is enabled but no resolution inferences with equations are generated. If

set to 2, equations are considered for Standard Resolution steps as well. Default is

0.

-ISHy

Enables/disables the inference rule Standard Hyper-Resolution. Default is 0.

-IOHy

Enables/disables the inference rule Ordered Hyper-Resolution. Default is 0.

-IURR

Enables/disables the inference rule Unit Resulting Resolution. Default is 0.

-IOFc

Enables/disables the inference rule Ordered Factoring. If set to 1, Ordered Factoring

is enabled but only factoring inferences with positive literals are generated. If set

to 2, negative literals are considered for inferences as well. Default is 0.

-ISFc

Enables/disables the inference rule Standard Factoring. Default is 0.

-IUnR

Enables/disables the inference rule Unit Resolution. Default is 0.

-IBUR

Enables/disables the inference rule Bounded Depth Unit Resolution. Default is 0.

-IDEF

Enables/disables the inference rule Apply Definitions. Currently not supported.

Default is 0.

-RFRew

Enables/disables the reduction rule Forward Rewriting. If set to 1 unit rewriting and

non-unit rewriting based on a subsumption test is activated. If set to 2 in addition

to unit and non-unit rewriting local contextual rewriting is activated. If set to 3

in addition to unit and non-unit rewriting subterm contextual rewriting is

activiated. Subterm contextual rewriting subsumes local contextual rewriting. If set

to 4 in addition of the rewriting rules of 3, subterm contextual rewriting also tests

for negative literal elimination. Default is 0.

-RBRew

Enables/disables the reduction rule Backward Rewriting. Same values and meaning as

for flag -RFRew but used in backward direction. Default is 0.

-RFMRR

Enables/disables the reduction rule Forward Matching Replacement Resolution. Default

is 0.

-RBMRR

Enables/disables the reduction rule Backward Matching Replacement Resolution. Default

is 0.

-RObv

Enables/disables the reduction rule Obvious Reduction. Default is 0.

-RUnC

Enables/disables the reduction rule Unit Conflict. Default is 0.

-RTer

Enables/disables the terminator by setting the maximal number of non-unit clauses to

be used during the search. Default is 0.

-RTaut

Enables/disables the reduction rule Tautology Deletion. If set to 1, only syntactic

tautologies are detected and deleted. If set to 2, additionally semantic tautologies

are removed. Default is 0.

-RSST

Enables/disables the reduction rule Static Soft Typing. Default is 0.

-RSSi

Enables/disables the reduction rule Sort Simplification. Default is 0.

-RFSub

Enables/disables the reduction rule Forward Subsumption Deletion. Default is 0.

-RBSub

Enables/disables the reduction rule Backward Subsumption Deletion. Default is 0.

-RAED

Enables/disables the reduction rule Assignment Equation Deletion. This rule removes

particular occurrences of equations from clauses. If set to 1, the reduction is

guaranteed to be sound. If set to 2, the reduction is only sound if any potential

model of the considered problem has a non-trivial domain. Default is 0.

-RCon

Enables/disables the reduction rule Condensation. Default is 0.

-TDfg2OtterOptions

Enables/disables the inclusion of an Otter options header. This option only applies to

dfg2otter. If set to 1 it includes a setting that makes Otter nearly complete. If set

to 2 it activates auto modus and if set to 3 it activates the auto2 modus. Default is

0.

-EML

A special EML flag for modal logic or description logic formulae. Never needs to be

set explicitly. Is set during parsing.

-EMLAuto

Intended for EML Autonomous mode, as yet not functional. Default is 0.

-EMLTranslation

Determines the translation method used for modal logic or description logic formulae.

If set to 0, the standard relational translation method (which is determined by the

usual Kripke semantics) is used. If set to 1, the functional translation method is

used. If set to 2, the optimised functional translation method is used. If set to 3,

the semi-functional translation method is used. A variation of the optimised

functional translation method is used, when the following settings are specified:

-EMLTranslation=2 -EMLFuncNary=1. The translation will be in terms of n-ary

predicates instead of unary predicates and paths. In the current implementation the

standard relational translation method is most general. Some restrictions apply to the

other methods. The functional translation method and semi-functional translation

methods are available only for the basic multi-modal logic K(m) possibly with serial

(total) modalities (-EMLTheory=1), plus nominals (ABox statements), terminological

axioms and general inclusion and equivalence axioms. The optimised functional

translation methods are implemented only for K(m), possibly with serial modalities.

Default is 0.

-EML2Rel

If set, propositional/Boolean-type formulae are converted to relational formulae

before they are translated to first-order logic. Default is 0.

-EMLTheory

Determines which background theory is assumed. If set to 0, the background theory is

empty. If set to 1, then seriality (the background theory for KD) is added for all

modalities. If set to 2, then reflexivity (the background theory for KT) is added for

all modalities. If set to 3, then symmetry (the background theory for KB) is added

for all modalities. If set to 4, then transitivity (the background theory for K4) is

added for all modalities. If set to 5, then Euclideanness (the background theory for

K5) is added for all modalities. If set to 6, then transitivity and Euclideanness

(the background theory for S4) is added for all modalities. If set to 7, then

reflexivity, transitivity and Euclideanness (the background theory for S5) is added

for all modalities. Default is 0.

-EMLFuncNdeQ

If set, diamond formulae are translated according to tr(dia(phi),s) = nde(s) /\ exists

x tr(phi,[s x]) (a nde / quantifier formula), otherwise the translation is in

accordance with tr(dia(phi),s) = exists x nde(s) /\ tr(phi,[s x]) (a quantifier / nde

formula). The transltion for box formulae is defined dually. Setting this flag is

only meaningful when the flag for the functional or semi functional translation method

is set. Default is 1.

-EMLFuncNary

If set, the functional translation into fluted logic is used. This means n-ary

predicate symbols are used instead of unary predicate symbols and paths. Setting this

flag is only meaningful for testing local satisfiability/validity in multi-modal K.

Default is 0.

-EMLFFSorts

If set, sorts for terms are used. Default is 0.

-EMLElimComp

If set, try to eliminate relational composition in modal parameters. Default is 0.

-EMLPTrans

If set, the EML to first-order logic translation is documented. Default is 0.

-TPTP

If set, SPASS expects an input file in TPTP syntax. Default is 0.

-rf If set, SPASS deletes the input file before termination. Default is 0.

**EXAMPLES**

To run SPASS on a single file without options:

SPASS I<filename>

To disable all SPASS output except for the final result:

SPASS -PGiven=0 -PProblem=0 I<filename>

**NOTES**

You can also specify options for SPASS in the input problem. In the DFG syntax, you would

use

list_of_settings(SPASS).

{*

set_flag(DocProof,1).

*}

end_of_list.

to set the DocProof flag.

There are three types of options you can set in the input:

set_flag(<flag>,<value>).

Sets a flag to a value. Valid flags and values are described in the OPTIONS section.

set_precedence(<comma-separated list of function and/or predicate symbols>).

Sets the precedence for the listed symbols. The precedence is decreasing from left to

right, i.e. the leftmost symbol has the highest precedence.

Every entry in the list has the form

SYMBOL | (SYMBOL, WEIGHT [, {l, r, m}])

You can use the second form to assign weights to symbols (for KBO) or a status (for

RPOS). Status is either @t{l} for left-to-right, @t{m} for multiset, or @t{r} for

right-to-left. Weight is given as an integer.

set_DomPred(<comma-separated list of predicate symbols>).

Listed predicate (

__DomPred__for dominant predicate) symbols are first ordered according

to their precedence, not according to their argument lists. Only in case of equal

predicates, the arguments are examined. For example, if we add the option

set_DomPred(P).

then in the clause

-> R(f(x,y),a), P(x,a).

the atom

__P(x,a)__is strictly maximal. Predicates listed by the

__set_DomPred__option are

compared according to the precedence.

set_selection(<comma-separated list of predicate symbols>).

Sets the selection list that can be employed by the Select flag (see above).

set_ClauseFormulaRelation(<comma separated list auf tuples (<clause number>, sequence of

axiom name strings)).

This list is in particular set by FLOTTER and enables SPASS for an eventually found

proof to show the relation between the clauses used in the proof and the input

formulas. If combined with option DocProof, then there needs to be an entry for every

clause number. Otherwise an error is reported.

set_ClauseFormulaRelation((1,ax2),(2,ax1),(3,ax3,ax1)).

Use SPASS online using onworks.net services