Man Linux: Main Page and Category List

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.

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"
           Enables/disables the documentation of split backtracking steps
           where the current backtracking level is printed.  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 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, 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 1 negative literals in clauses
           with more than one maximal literal are selected, if set to 2
           negative literals are always selected. The latter case results in
           an ordered hyperresolution like behavior of ordered resolution.
           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.

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

       "-CNFRenaming  "
           Enables/disables formula renaming.  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.  Default is
           0.

       "-RBRew"
           Enables/disables the reduction rule Backward Rewriting.  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.

EXAMPLES

       To run SPASS on a single file without options:

               SPASS  I<filename>

       To disable all SPASS output expect 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.

SEE ALSO

       checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1),
       tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), dfg2dfg(1)

AUTHORS

       Contact : Thomas Hillenbrand <hillen@mpi-sb.mpg.de>
                 Christoph Weidenbach <weidenb@mpi-sb.mpg.de>