1 SPASS
*******

1.1 NAME
========

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

1.2 SYNOPSIS
============

SPASS [`options'] [INPUTFILE]

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

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

1.5 SETTINGS
============

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 l for left-to-right, m for
     multiset, or 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)).

1.6 EXAMPLES
============

To run SPASS on a single file without options:
     SPASS  filename
   To disable all SPASS output except for the final result:
     SPASS  -PGiven=0 -PProblem=0 filename

1.7 AUTHORS
===========

Contact : spass@mpi-inf.mpg.de

1.8 SEE ALSO
============

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

2 checkstat
***********

2.1 NAME
========

checkstat - checks SPASS behavior on problem files

2.2 SYNOPSIS
============

*checkstat* [`-cdFiklmopPrstTuvVwx'] DIR_1/FILE_1 ... DIR_N/FILE_N

2.3 DESCRIPTION
===============

The *checkstat* script is intended for automatically checking the
declared state of a theorem proving problem, specified in *DFG*
syntax, against the state computed by the *SPASS* theorem prover. The
script is written in *Perl*.

For using the proof and model checking facilities, the *pcs* and
*rescmp* programs must exist in the same directory as *checkstat*, or
the corresponding environment variables *PCS* and *RESCMP* must be set
to their paths.

*checkstat* examines the set of files that is given by all specified
files and all files in the specified directories that have a '.cnf',
'.frm', or '.dfg' extension. *checkstat* evokes *SPASS* on each file
and compares its result with the problem state specified in the
'status' field of the *DFG*  problem description. Optionally (see
below), *SPASS* proofs can be verified by a proof checker, and *SPASS*
completions can be checked against reference completions. If *SPASS*
outputs memory check information in the format produced by the 'CHECK'
compile time variable, then *checkstat* verifies that all memory has
been cleaned up at the end of the *SPASS* run.

*checkstat* continues as long as no critical events occur, which are
(besides standard system errors, e.g. in file access):

   * A problem state is declared satisfiable (unsatisfiable), and
     *SPASS* computes unsatisfiable (satisfiable).

   * *SPASS* returns an invalid proof (only if proof checking is
     enabled).

   * The *SPASS* completion and the reference completion differ (if
     completion checking is enabled, and a reference file is present).

   * *SPASS* reports that not all memory has been cleaned up.

   * *SPASS* memory use reporting is inconsistent:  Either *SPASS*
     gives memory use information for the current file, but has not
     given it for the previous files, or vice versa, gives no memory
     information for the current file, but has done this for previous
     files.

   * The problem state could not be extracted from the problem file.

   * No problem state could be extracted from the *SPASS* output, for
     example due to a segmentation fault.

These errors are reported, and *checkstat* stops. All other possible
events are classified as uncritical. They are fully reported in the
moment of their occurrence only if the *-v* option has been activated.
Their occurrence is always mentioned in a final event statistic, but
not with the associated problem files. Uncritical events are:
   * *SPASS* runs out of time or out of memory.

   * *SPASS* decides a problem whose state is declared 'unknown'.
   If a file 'filename.dfg' is in the set of specified files, and there
exists corresponding corresponding '.cnf' file 'filename.cnf' in the
same directory,  then this file is passed to *SPASS*, even if it is not
a parameter to *checkstat*. I.e.,
     *checkstat* test.dfg
   passes the file 'test.cnf' to *SPASS* if it exists in the current
working directory.

2.4 OPTIONS
===========

The following options are supported by *checkstat*:

`-v'
     Verbose mode. Prints information on the currently checked
     directory, file, and uncritical events.  Default is 'off'.

`-V'
     Very verbose mode. Enables verbose mode, and prints output of
     proof checker *pcs*.

`-p prover'
     Specify prover. Can be used for setting *SPASS* options, see
     examples below. Default is value of the environment variable
     'SPASS'.

`-t limit'
     Specify a time limit for *SPASS* (in seconds). Default is 10
     seconds.

`-c'
     Specify time limit for proof checker *pcs*.

`-l'
     Log *SPASS* result for each file 'filename.cnf' in 'filename.log'.
     Default is 'off'. This option is to be used with care, as a *Perl*
     variable with the same size as the *SPASS* output is created in
     the memory.

`-u'
     Check *SPASS* proofs for correctness ('u' for 'unsatisfiable').

`-s'
     Check *SPASS* completions against reference completions.  The
     reference completion corresponding to a problem file filename
     .ext', where ext is some *DFG*  file extension, is 'filename.mod'
     and must be located in the same directory as the problem file.
     ('s' is for 'satisfiable).

`-r'
     Run. Continue after errors.

`-w'
     Print warning if model checking is enabled, a model has been found,
     but the reference does not exist.

`-P'
     Specify *SPASS* options. Enclose in single quotes to protect from
     shell please.

`-T limit'
     Enable timing by shell. Stops in time even if *SPASS* timing does
     not work.

`-c limit'
     Specify time limit in seconds for proof checker. This is the time
     available for verifying one proof step in a proof.

`-d'
     Debug. Lots of output about intermediate results etc.

`-k'
     Keep. Keep generated temporary files.

`-o'
     Use *SPASS* instead of OTTER for proof checking.

`-x'
     Extension. Process all file parameters, regardless of extension.
     Normally, files with unknown extensions are ignored.

`-i'
     Interactive. Reads file names from standard input.

`-m'
     Mode. Print out command line.

2.5 EXAMPLES
============

To check a single file with some extra *SPASS* options:
     *checkstat* -p 'SPASS options' filename
   To check all files with '.cnf' suffix in directory 'Test':
     *checkstat* Test/*.cnf

2.6 AUTHORS
===========

Thorsten Engel and Christian Theobalt

   Contact : spass@mpi-inf.mpg.de

2.7 SEE ALSO
============

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

3 filestat
**********

3.1 NAME
========

filestat - compares SPASS results with status in problem files

3.2 SYNOPSIS
============

*filestat* [ -vc] file_1 ... file_n

3.3 DESCRIPTION
===============

Like *checkstat*, *filestat* is a script for automatically comparing a
set of *SPASS* results against reference results. Unlike *checkstat*,
*SPASS* is not actually run on the problems. Instead, input to
*filestat* are *SPASS* result files, which contain concatenations of
*SPASS* outputs, describing the input file and the result. *filestat*
compares the problem status in each of these input files with the
problem status computed by *SPASS* and outputs differences.

3.4 OPTIONS
===========

The following options are supported by *filestat*:
`-c'
     Continue after status differences. Default: 'Off'.

`-v'
     Report in detail. Especially, print out which *SPASS* result file
     is currently processed. Default: 'Off'.

3.5 AUTHORS
===========

Thorsten Engel and Christian Theobalt

   Contact : spass@mpi-inf.mpg.de

3.6 SEE ALSO
============

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

4 pcs
*****

4.1 NAME
========

pcs - checks SPASS proofs

4.2 SYNOPSIS
============

*pcs* [ -cdfrstv] file

4.3 DESCRIPTION
===============

*pcs* is a Perl script that supports automatic checking of proofs
specified in *DFG* syntax with the theorem prover OTTER.  It uses
   * the C-program *pgen*, which generates proof tasks corresponding to
     inference steps for each proof step of a *DFG* proof and checks
     the tableau structure.

   * the C-program *SPASS* with the -Flotter option for converting
     *DFG* syntax files with formulas into *DFG* syntax files with
     clauses.

   * the C-program dfg2otter, which transforms files in *DFG* syntax
     with clauses only into files for OTTER syntax.
   *pcs* checks that:
   * The conclusion in each proof step is a logical consequence of the
     assumptions in that proof step.

   * Each clause in a subtableau uses only parents clauses that are
     visible at this point in the tableau.

   * Each clause, except for split clauses, has the maximum split level
     of its parents.

   * If the first half of a split was ground, then negations of its
     literals can be used in the tableau branch corresponding to the
     second half of the split.

   * The tableau is complete and closed.
   The second condition is verified by checking the unsatisfiability
     Assumptions \wedge \neg Conclusion
   for each proof step (inference rule application) by running OTTER
for a limited time. The appropriate *DFG* files for these problems are
generated by *pgen*. OTTER may fail to terminate within this time,
leaving the correctness of a proof step undecided, which leads to the
three possible results of *pcs*:
   * The proof is correct: Both conditions are satisfied for all proof
     steps.

   * The proof is not correct: One condition is definitely violated for
     at least one proof step.

   * Correctness is undecided: The first condition is satisfied, but
     the second condition could not be verified nor falsified for at
     least one proof step.

*pcs* uses a working directory, in which all proof tasks corresponding
to the proof steps are generated using the *pgen* program. These tasks
are subsequently checked using OTTER.

4.4 OPTIONS
===========

Several options control the behavior of *pcs* when it fails to verify a
proof step, its output and the naming of generated files and the
working directory:

`-c'
     Continue even if a single proof step could not be verified.
     Default 'off'.

`-d suffix'
     Suffix of created working directory. For an input file root.ext,
     the working directory <root><suffix> is created. If suffix does
     not end with a backslash, it is taken as a prefix for files
     generated by *pgen*, which are then created in the current working
     directory. Default is '_SubProofs/'.

`-f'
     Overwrite working directory if it already exists. Default 'off'.

`-o'
     Use *SPASS* as proof checker instead of OTTER. This option is
     especially useful when checking proofs generated by a different
     prover.  Default is 'off'.

`-p path'
     Location of *DFG* prover to be used instead of the default one. If
     -o is specified, then it overrides this option, and *SPASS* is used
     instead. If a *DFG* converter is specified, then a prover must be
     specified as well. Default is OTTER.

`-q'
     Be quiet and do not print program paths. This option is especially
     useful inside *checkstat*. Default is 'off'.

`-r'
     Clean up all generated files at the end, even if the proof is not
     valid.  Default 'off'.

`-s suffix'
     Suffix of files generated by *pgen*. Default is '.dfg'.

`-t limit'
     Number of seconds for each proof attempt for each proof step.
     Default is 3 seconds.

`-v'
     (verbose) Give some progress information. Default is 'off'.

`-w path'
     Location of *DFG* converter to be used instead of the default one.
     If a *DFG* converter is specified, then a prover must be specified
     as well. Default is *dfg2otter.pl*.

4.5 AUTHORS
===========

Thorsten Engel and Christian Theobalt.

   Contact : spass@mpi-inf.mpg.de

4.6 SEE ALSO
============

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

5 pgen
******

5.1 NAME
========

pgen - generates single step proof obligations out of a DFG (SPASS)
proof

5.2 SYNOPSIS
============

*pgen*  [ -dstqjnr] [-vinci -xvcg] filename

5.3 DESCRIPTION
===============

¢ man begin DESCRIPTION *pgen* is a C-program that checks the tableau
structure of SPASS tableau proofs and generates proof tasks
corresponding to proof steps. Before the proof tasks are generated, the
tableau is reduced in two steps:
  1. If an empty clause exists in a subtableau, all successors of the
     subtableau are deleted.

  2. If a subtableau has a single successor subtableau, the successor
     is deleted.
        After the reduction, *pgen* checks that
   * Each clause in a subtableau uses only parents clauses that are
     visible at this point in the tableau.

   * Each clause, except for split clauses, has the maximum split level
     of its parents.

   * If the first half of a split was ground, then negations of its
     literals can be used in the tableau branch corresponding to the
     second half of the split.

   * The tableau is complete and closed.

Generated filenames have the form <prefix><filename><suffix>, where
suffix and prefix are specified by the *-d* and *-s* option.

*pgen* can generate graph representations of the tableau before and
after the reduction using the *-n* and *-r* options. These
representations can be written to a text file in either *daVinci* or
*xvcg* format. See section daVinci and VCG, for these graph
visualization programs.

5.4 OPTIONS
===========

The following options are supported by *pgen*:
`-j'
     Do not generate proof files.

`-q'
     Quiet mode.

`-d prefix'
     Prefix of generated files. The option name was chosen because the
     prefix is probably a directory.

`-t limit'
     Number of seconds for each proof attempt for each proof step.
     Default is 3 seconds.

`-s suffix'
     Suffix of files generated by *pgen*. Default is '.dfg'.

`-r filename'
     Write representation of the reduced tableau to <filename>.

`-n filename'
     Write representation of the non-reduced tableau to <filename>.

`-vinci'
     Write tableau representation in daVinci format.

`-xvcg'
     Write tableau representation in xvcg format.

5.5 DAVINCI AND  VCG
====================

*VCG* is a public domain tool intended for visualizing compiler graphs.
It is developed by Georg Sander at the University of Saarbruecken. It
is available via anonymous ftp at
     ftp.cs.uni-sb.de
   in the directory pub/graphics/vcg. Or visit
     http://rw4.cs.uni-sb.de/~sander/html/gsvcg1.html.
   *daVinci* is another public domain graph visualizing tool. Get it at
     ftp.tzi.de
   in the directory /tzi/biss/daVinci. The WWW address is
     http://www.informatik.uni-bremen.de/daVinci/.

5.6 AUTHORS
===========

Thorsten Engel and Christian Theobalt.

   Contact : spass@mpi-inf.mpg.de

5.7 SEE ALSO
============

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

6 rescmp
********

6.1 NAME
========

rescmp - tests subsumption relation between clause sets

6.2 SYNOPSIS
============

*rescmp* [ -v] file

6.3 DESCRIPTION
===============

*rescmp* is a C-program that compares two clause sets specified by two
*DFG* files.  It tries to find, for each clause in the first set, a
corresponding clause in the second set such that both clauses mutually
subsume. It reports success only if there is a one-to-one mapping
between the two sets under this condition.

6.4 OPTIONS
===========

The following options are supported by *rescmp*:
`-v'
     prints out unmapped clauses - that is clauses that have no
     corresponding clause - in both sets.

6.5 AUTHORS
===========

Thorsten Engel and Christian Theobalt.

   Contact : spass@mpi-inf.mpg.de

   cc man end

6.6 SEE ALSO
============

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

7 tpform
********

7.1 NAME
========

tpform - transforms SPASS output statements into TPTP style format

7.2 SYNOPSIS
============

*tpform* [ -tb] [infile] [outfile]

7.3 DESCRIPTION
===============

The *tpform* script transforms a list of SPASS outputs into a TPTP
result file or another simple file format. Both formats are a list of
problem file names annotated with information, like the logical status
of the problem and time needed to decide the status etc.

If no file arguments are given, *tpform* reads from stdin and writes to
stdout. If one file argument is given, *tpform* read from that file, and
if a second argument is present, *tpform* writes to it.

7.4 OPTIONS
===========

The following options are supported by *tpform*:
`-b'
     Selects simple output format instead of TPTP format

`-t'
     If -b is selected, print *SPASS* running time at the end of each
     output line, eg: `SteamRoller + 00:00:05.28'

7.5 FORMATS
===========

We take the following *SPASS* output as an example:

     SPASS V0.78
     SPASS beiseite: Proof found.
     Problem: Tests/Pelletier/problem1.dfg
     SPASS derived 0 clauses, backtracked 0 clauses and kept 3 clauses.
     SPASS allocated 165 KBytes.
     SPASS spent     0:00:00.01 on the problem.
                     0:00:00.00 for the input.
                     0:00:00.00 for the FLOTTER CNF translation.
                     0:00:00.00 for inferences.
                     0:00:00.00 for the backtracking.

The TPTP format for this information is:

     problem1.dfg  P     1        0.01   165     3        -      -
                   ^     ^        ^^^^   ^^^     ^        ^      ^
                   P/M   # proofs time   memory  clauses  proof  proof
                   or error                               length depth
                   message

The simple format is for this example:

     problem1.dfg +

and in general:

     filename {+|-|0} [time]

where '+' marks problems for which *SPASS* found a proof, '0' stands
for found completions and '-' marks undecided problems. The time
information is given if the -t option is used.

7.6 AUTHORS
===========

Thorsten Engel and Christian Theobalt.

   Contact : spass@mpi-inf.mpg.de

7.7 SEE ALSO
============

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

8 tpget
*******

8.1 NAME
========

tpget - selects problems from a library

8.2 SYNOPSIS
============

*tpget* [-l libdir] file_1 ... file_n target

8.3 DESCRIPTION
===============

*tpget* reads lists of theorem proving problems in TPTP format (TPTP
scripts) and assembles the problem files specifying these problems into
a target directory . The problem files are taken from the library
specified by the -l option (see example below). If a problem file
already exists in the target directory it is not copied again.

   The files file_1 ... file_n have to contain one short problem name
per line.  Examples for short problem names are `SYN313-1.001:002' or
`LCL354+1'.

8.4 OPTIONS
===========

The following option is required by *tpget*:

`-l'
     Specifies the library where problem files are taken from.

8.5 EXAMPLES
============

To assemble all problem files specified by file into Dir, using the
library /foo/bar:
     *tpget* -l /foo/bar file Dir

8.6 AUTHORS
===========

Thorsten Engel, Enno Keen and Christian Theobalt.

   Contact : spass@mpi-inf.mpg.de

8.7 SEE ALSO
============

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

9 deprose
*********

9.1 NAME
========

deprose - condenses checkstat error output

9.2 SYNOPSIS
============

*deprose* [infile] [outfile]

9.3 DESCRIPTION
===============

*deprose* is a *Perl* script for condensing *checkstat* error output.
As input, it gets an arbitrary text containing messages of the
following form:

     *  Problem 'xy':
     *  SPASS computes problem state 'satisfiable'
     *  which is declared 'unsatisfiable'

*deprose* outputs an annotated list of the files in which errors
occurred. Each file in this list is annotated with '+', if *SPASS*
found a proof on this file, or '-', if *SPASS* found a model.

If no file arguments are given, *deprose* reads from stdin and writes to
stdout. If one file argument is given, *deprose* reads from that file,
and if a second argument is given, *deprose* writes to that file.

9.4 AUTHORS
===========

Thorsten Engel and Christian Theobalt

   Contact : spass@mpi-inf.mpg.de

9.5 SEE ALSO
============

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

10 dfg2ascii
************

10.1 NAME
=========

dfg2ascii - transforms DFG files into pretty printed ASCII files

10.2 SYNOPSIS
=============

*dfg2ascii* <infile>

10.3 DESCRIPTION
================

*dfg2ascii* is a program to convert a problem input file in *DFG*
format into pretty-printed ASCII text. It prints out the axioms and the
conjectures, in that order.

10.4 AUTHORS
============

Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach.

   Contact : spass@mpi-inf.mpg.de

10.5 SEE ALSO
=============

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

11 dfg2otter
************

11.1 NAME
=========

dfg2otter - transforms DFG clause files into Otter format

11.2 SYNOPSIS
=============

*dfg2otter* [options] <infile> <outfile>

11.3 DESCRIPTION
================

*dfg2otter* is a C-program to transform problem input files in *DFG*
syntax into *Otter* syntax. It accepts all options from *SPASS*,
although only a subset has an effect on translation.

   *dfg2otter* negates conjecture formulae of the *SPASS* input file
before printing the Otter usable list. The *SPASS* conjecture formula
list is translated into a disjunction of the negated single conjectures.
If the *SPASS* input file consits of clauses, these are not modified.

11.4 AUTHORS
============

Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach

   Contact : spass@mpi-inf.mpg.de

11.5 SEE ALSO
=============

checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1),
tpget(1), deprose(1), dfg2otter.pl(1), SPASS(1)

12 dfg2otter.pl
***************

12.1 NAME
=========

dfg2otter.pl - transforms DFG clause files into Otter format including
Otter options

12.2 SYNOPSIS
=============

*dfg2otter.pl* [options] [infile] [outfile]

12.3 DESCRIPTION
================

*dfg2otter.pl* is a *Perl* wrapper for the *dfg2otter*. Mainly, it adds
a set of OTTER parameters to the transformation result of *dfg2otter*.
Additionally, input/output redirection is simpler: If no file arguments
are given, *dfg2otter.pl* reads from stdin and writes to stdout. If one
file argument is given, *dfg2otter.pl* read from that file, and if a
second argument is present, *dfg2otter.pl* writes to it.

12.4 OPTIONS
============

`-t n'
     Sets the time limit for the OTTER proof attempt to n seconds.

12.5 AUTHORS
============

Thorsten Engel and Christian Theobalt.

   Contact : spass@mpi-inf.mpg.de

12.6 SEE ALSO
=============

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

13 dfg2dfg
**********

13.1 NAME
=========

dfg2dfg - calculate approximations of problems

13.2 SYNOPSIS
=============

*dfg2dfg* [-horn] [-monadic] [-linear] [-shallow] [INFILE] [OUTFILE]

13.3 DESCRIPTION
================

*dfg2dfg* is a program that reads clauses from an input file in DFG
syntax.  It then calculates an approximation of the clause set
depending on the command line options.  Finally it writes the
approximated clause set in DFG syntax to a file.

   If neither INFILE nor OUTFILE are given, *dfg2dfg* reads from
standard input and writes to standard output.  If one file name is
given, it reads from that file and writes the output to standard output.
If more than one file name is given, *dfg2dfg* reads from the first
file and writes to the second.

   The approximations are described in technical detail in the separate
paper *dfg2dfg.ps* included in the SPASS distribution.

13.4 OPTIONS
============

*dfg2dfg* has four different command line options that may be combined.
`-horn'
     This option enables the transformation of non-horn clauses into
     horn clauses.  Each non-horn clause with _n_ positive literals is
     transformed into _n_ horn clauses, where the _i_-th clause
     contains the _i_-th positive literal and all negative literals of
     the non-horn clause.  See also section 3 of the paper.

`-monadic[=n]'
     With this option atoms with non-monadic predicate symbols are
     transformed into monadic atoms.  If _n_ is omitted or _n_=1 a term
     encoding is applied, i.e., all non-monadic predicates are moved to
     the term level.  With _n_=2 a projection is applied. All
     non-monadic atoms are replaced by their monadic argument
     projections.  See section 4.1 section 4.2 of the paper for more
     details.

`-linear'
     This approximation transforms a clause with monadic literals and
     non-linear variable occurrences in succedent atoms, into a new
     clause with possibly more negative literals, that doesn't contain
     any non-linear variables in the succedent.  See section 5 of the
     paper for details.

`-shallow[=n]'
     This transformation tries to reduce the depth of the terms in
     positive literals.  The transformation is applied to horn clauses
     with monadic literals only.  If _n_ is omitted or _n_=1 a strict
     transformation is applied, that is equivalence preserving, however.
     For _n_=2 some preconditions are removed.  This allows the
     transformation to be applied more often, but the transformation
     isn't equivalence preserving any more.  For _n_=3 even more
     preconditions are removed.  Take a look at section 6._n_ of the
     paper for the details of the command line option _-monadic=n_.

13.5 AUTHORS
============

Enno Keen

   Contact : spass@mpi-inf.mpg.de

13.6 SEE ALSO
=============

SPASS(1)

14 dfg2tptp
***********

14.1 NAME
=========

dfg2tptp - transforms DFG files into TPTP files.

14.2 SYNOPSIS
=============

*dfg2tptp* <input-file> <output-file>

14.3 DESCRIPTION
================

*dfg2tptp* is a program which converts a problem input file in *DFG*
format into a problem input file in *TPTP* format.  The *TPTP* problem
format is used by the TPTP library of test problems for automated
theorem proving, available at *http://www.math.miami.edu/~tptp/*.
Various tools exist to convert problems in *TPTP* format into input
files for other theorem provers.

14.4 AUTHORS
============

Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach

   Contact : spass@mpi-inf.mpg.de

14.5 SEE ALSO
=============

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

15 tptp2dfg
***********

15.1 NAME
=========

tptp2dfg - transforms DFG files into TPTP files.

15.2 SYNOPSIS
=============

*tptp2dfg* [-include] <input-file> <output-file>

15.3 DESCRIPTION
================

*tptp2dfg* is a program which converts a problem input file in *TPTP*
format into a problem input file in *DFG* format.  The *TPTP* problem
format is used by the TPTP library of test problems for automated
theorem proving, available at *http://www.math.miami.edu/~tptp/*.

15.4 OPTIONS
============

*tptp2dfg* supports the following command line options.
`-include'
     This option enables the expansion of include directives in tptp
     files.  If set all TPTP include directives in hte input-file are
     replaced by the respective file content during translation. If not
     set the TPTP include directives are translated into DFG include
     directives.  Default is off.

15.5 AUTHORS
============

Martin Suda and Christoph Weidenbach

   Contact : spass@mpi-inf.mpg.de

15.6 SEE ALSO
=============

dfg2tptp(1), dfg2otter(1), SPASS(1)

16 spassfaq
***********

16.1 QUESTIONS
==============

Q:      How can I get an answer substitution?

16.2 ANSWERS
============

A:      There are no meta predicates in SPASS available. Hence,
this functionality is not directly supported. However it         can be
achieved by a trick. The idea is to add a new literal         to the
conjecture clause that carries the substitution and         will
definitely be resolved away in the final step of the proof.
For example: let x be the variable where we are         interested in
the subsitution. Let x occur in the single         conjecture clause C.
Then extend this clause to C,P(x,a,y)         and add the clause
-P(z,u,b), where P is new, and a,b are         constants. Furthermore
make P a minimal predicate using         a set_DomPred declaration (see
the SPASS man page). This         will force that the final step in the
proof is the one that         eliminates the P literal and the x will
be instantiated accordingly.          To make this work it may be
necessary to turn off certain reduction         rules of SPASS. To get
it rid of that, a trick is to extend all         predicates in C by a
further argument with the variable y and all         other occurrences
of these predicate with fresh variables.

16.3 AUTHORS
============

Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach

   Contact : spass@mpi-inf.mpg.de

16.4 SEE ALSO
=============

SPASS(1)