~ubuntu-branches/ubuntu/trusty/spass/trusty

.\" Automatically generated by Pod::Man v1.3, Pod::Parser v1.13

.\"

.\" Standard preamble:

.\" ========================================================================

.de Sh \" Subsection heading

.br

.if t .Sp

.ne 5

.PP

\fB\\$1\fR

.PP

..

.de Sp \" Vertical space (when we can't use .PP)

.if t .sp .5v

.if n .sp

..

.de Vb \" Begin verbatim text

.ft CW

.nf

.ne \\$1

..

.de Ve \" End verbatim text

.ft R

 

.fi

..

.\" Set up some character translations and predefined strings.  \*(-- will

.\" give an unbreakable dash, \*(PI will give pi, \*(L" will give a left

.\" double quote, and \*(R" will give a right double quote.  | will give a

.\" real vertical bar.  \*(C+ will give a nicer C++.  Capital omega is used to

.\" do unbreakable dashes and therefore won't be available.  \*(C` and \*(C'

.\" expand to `' in nroff, nothing in troff, for use with C<>.

.tr \(*W-|\(bv\*(Tr

.ds C+ C\v'-.1v'\h'-1p'\s-2+\h'-1p'+\s0\v'.1v'\h'-1p'

.ie n \{\

.    ds -- \(*W-

.    ds PI pi

.    if (\n(.H=4u)&(1m=24u) .ds -- \(*W\h'-12u'\(*W\h'-12u'-\" diablo 10 pitch

.    if (\n(.H=4u)&(1m=20u) .ds -- \(*W\h'-12u'\(*W\h'-8u'-\"  diablo 12 pitch

.    ds L" ""

.    ds R" ""

.    ds C` ""

.    ds C' ""

'br\}

.el\{\

.    ds -- \|\(em\|

.    ds PI \(*p

.    ds L" ``

.    ds R" ''

'br\}

.\"

.\" If the F register is turned on, we'll generate index entries on stderr for

.\" titles (.TH), headers (.SH), subsections (.Sh), items (.Ip), and index

.\" entries marked with X<> in POD.  Of course, you'll have to process the

.\" output yourself in some meaningful fashion.

.if \nF \{\

.    de IX

.    tm Index:\\$1\t\\n%\t"\\$2"

..

.    nr % 0

.    rr F

.\}

.\"

.\" For nroff, turn off justification.  Always turn off hyphenation; it makes

.\" way too many mistakes in technical documents.

.hy 0

.if n .na

.\"

.\" Accent mark definitions (@(#)ms.acc 1.5 88/02/08 SMI; from UCB 4.2).

.\" Fear.  Run.  Save yourself.  No user-serviceable parts.

.    \" fudge factors for nroff and troff

.if n \{\

.    ds #H 0

.    ds #V .8m

.    ds #F .3m

.    ds #[ \f1

.    ds #] \fP

.\}

.if t \{\

.    ds #H ((1u-(\\\\n(.fu%2u))*.13m)

.    ds #V .6m

.    ds #F 0

.    ds #[ \&

.    ds #] \&

.\}

.    \" simple accents for nroff and troff

.if n \{\

.    ds ' \&

.    ds ` \&

.    ds ^ \&

.    ds , \&

.    ds ~ ~

.    ds /

.\}

.if t \{\

.    ds ' \\k:\h'-(\\n(.wu*8/10-\*(#H)'\'\h"|\\n:u"

.    ds ` \\k:\h'-(\\n(.wu*8/10-\*(#H)'\`\h'|\\n:u'

.    ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'^\h'|\\n:u'

.    ds , \\k:\h'-(\\n(.wu*8/10)',\h'|\\n:u'

.    ds ~ \\k:\h'-(\\n(.wu-\*(#H-.1m)'~\h'|\\n:u'

.    ds / \\k:\h'-(\\n(.wu*8/10-\*(#H)'\z\(sl\h'|\\n:u'

.\}

.    \" troff and (daisy-wheel) nroff accents

.ds : \\k:\h'-(\\n(.wu*8/10-\*(#H+.1m+\*(#F)'\v'-\*(#V'\z.\h'.2m+\*(#F'.\h'|\\n:u'\v'\*(#V'

.ds 8 \h'\*(#H'\(*b\h'-\*(#H'

.ds o \\k:\h'-(\\n(.wu+\w'\(de'u-\*(#H)/2u'\v'-.3n'\*(#[\z\(de\v'.3n'\h'|\\n:u'\*(#]

.ds d- \h'\*(#H'\(pd\h'-\w'~'u'\v'-.25m'\f2\(hy\fP\v'.25m'\h'-\*(#H'

.ds D- D\\k:\h'-\w'D'u'\v'-.11m'\z\(hy\v'.11m'\h'|\\n:u'

.ds th \*(#[\v'.3m'\s+1I\s-1\v'-.3m'\h'-(\w'I'u*2/3)'\s-1o\s+1\*(#]

.ds Th \*(#[\s+2I\s-2\h'-\w'I'u*3/5'\v'-.3m'o\v'.3m'\*(#]

.ds ae a\h'-(\w'a'u*4/10)'e

.ds Ae A\h'-(\w'A'u*4/10)'E

.    \" corrections for vroff

.if v .ds ~ \\k:\h'-(\\n(.wu*9/10-\*(#H)'\s-2\u~\d\s+2\h'|\\n:u'

.if v .ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'\v'-.4m'^\v'.4m'\h'|\\n:u'

.    \" for low resolution devices (crt and lpr)

.if \n(.H>23 .if \n(.V>19 \

\{\

.    ds : e

.    ds 8 ss

.    ds o a

.    ds d- d\h'-1'\(ga

.    ds D- D\h'-1'\(hy

.    ds th \o'bp'

.    ds Th \o'LP'

.    ds ae ae

.    ds Ae AE

.\}

.rm #[ #] #H #V #F C

.\" ========================================================================

.\"

.IX Title "PCS 1"

.TH PCS 1 "2003-04-29" "perl v5.6.1" "SPASS"

.UC

.SH "NAME"

pcs \- checks \s-1SPASS\s0 proofs

.SH "SYNOPSIS"

.IX Header "SYNOPSIS"

\&\fBpcs\fR [ \-cdfrstv] file

.SH "DESCRIPTION"

.IX Header "DESCRIPTION"

\&\fBpcs\fR is a Perl script that supports automatic checking of proofs specified in 

\&\fB\s-1DFG\s0\fR syntax with the theorem prover \s-1OTTER\s0. 

It uses 

.IP "\(bu" 4

the C\-program \fBpgen\fR, which generates proof tasks corresponding to inference steps for each proof step of a \fB\s-1DFG\s0\fR proof and checks the tableau structure.

.IP "\(bu" 4

the C\-program \fB\s-1SPASS\s0\fR with the \-Flotter option for converting

\&\fB\s-1DFG\s0\fR syntax files with formulas into \fB\s-1DFG\s0\fR syntax files with

clauses.

.IP "\(bu" 4

the C\-program dfg2otter, which transforms files in \fB\s-1DFG\s0\fR syntax with

clauses only into files for \s-1OTTER\s0 syntax.

.PP

\&\fBpcs\fR checks that:

.IP "\(bu" 4

The conclusion in each proof step is a logical consequence

of the assumptions in that proof step.

.IP "\(bu" 4

Each clause in a subtableau uses only parents clauses that are 

visible at this point in the tableau.

.IP "\(bu" 4

Each clause, except for split clauses, has the maximum

split level of its parents.

.IP "\(bu" 4

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.

.IP "\(bu" 4

The tableau is complete and closed.

.PP

The second condition is verified by checking the unsatisfiability

.PP

.Vb 1

\&        Assumptions \ewedge \eneg Conclusion

.Ve

for each proof step (inference rule application) by running \s-1OTTER\s0

for a limited time. The appropriate \fB\s-1DFG\s0\fR files for these problems

are generated by \fBpgen\fR. \s-1OTTER\s0 may fail to terminate

within this time, leaving the correctness of a proof step undecided,

which leads to the three possible results of \fBpcs\fR:

.IP "\(bu" 4

The proof is correct: Both conditions are satisfied for all proof steps.

.IP "\(bu" 4

The proof is not correct: One condition is definitely violated for 

at least one proof step.        

.IP "\(bu" 4

Correctness is undecided: The first condition is satisfied,

but the second condition could not be verified nor falsified for at least

one proof step.

.PP

\&\fBpcs\fR uses a working directory, in which all proof tasks corresponding to the proof steps

are generated using the \fBpgen\fR program. These tasks are subsequently

checked using \s-1OTTER\s0. 

.SH "OPTIONS"

.IX Header "OPTIONS"

Several options control the behavior

of \fBpcs\fR when it fails to verify a proof step, its output and the

naming of generated files and the working directory:

.ie n .IP """\-c""" 4

.el .IP "\f(CW\-c\fR" 4

.IX Item "-c"

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

.ie n .IP """\-d \f(CIsuffix\f(CW""" 4

.el .IP "\f(CW\-d \f(CIsuffix\f(CW\fR" 4

.IX Item "-d suffix"

Suffix of created working directory. For an input file

\&\fIroot.ext\fR, the working directory \fI<root><suffix>\fR is created. If \fIsuffix\fR does not end with a backslash, it is taken as a \fIprefix\fR for files generated by \fBpgen\fR, which are then created in the current working directory. Default is '_SubProofs/'.

.ie n .IP """\-f""" 4

.el .IP "\f(CW\-f\fR" 4

.IX Item "-f"

Overwrite working directory if it already exists. Default 'off'.

.ie n .IP """\-o""" 4

.el .IP "\f(CW\-o\fR" 4

.IX Item "-o"

Use \fB\s-1SPASS\s0\fR as proof checker instead of \s-1OTTER\s0. This option is

especially useful when checking proofs generated by a different prover.

Default is 'off'.

.ie n .IP """\-p \f(CIpath\f(CW""" 4

.el .IP "\f(CW\-p \f(CIpath\f(CW\fR" 4

.IX Item "-p path"

Location of \fB\s-1DFG\s0\fR prover to be used instead of the default one. If \-o is

specified, then it overrides this option, and \fB\s-1SPASS\s0\fR is used

instead. If a \fB\s-1DFG\s0\fR converter is specified, then a prover must be

specified as well. Default is \s-1OTTER\s0.

.ie n .IP """\-q""" 4

.el .IP "\f(CW\-q\fR" 4

.IX Item "-q"

Be quiet and do not print program paths. This option is especially useful inside \fBcheckstat\fR. Default is 'off'.

.ie n .IP """\-r""" 4

.el .IP "\f(CW\-r\fR" 4

.IX Item "-r"

Clean up all generated files at the end, even if the proof is not valid.

Default 'off'.

.ie n .IP """\-s \f(CIsuffix\f(CW""" 4

.el .IP "\f(CW\-s \f(CIsuffix\f(CW\fR" 4

.IX Item "-s suffix"

Suffix of files generated by \fBpgen\fR. Default is '.dfg'.

.ie n .IP """\-t \f(CIlimit\f(CW """ 4

.el .IP "\f(CW\-t \f(CIlimit\f(CW \fR" 4

.IX Item "-t limit "

Number of seconds for each proof attempt

for each proof step. Default is 3 seconds.

.ie n .IP """\-v""" 4

.el .IP "\f(CW\-v\fR" 4

.IX Item "-v"

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

.ie n .IP """\-w \f(CIpath\f(CW""" 4

.el .IP "\f(CW\-w \f(CIpath\f(CW\fR" 4

.IX Item "-w path"

Location of \fB\s-1DFG\s0\fR converter to be used instead of the default one.

If a \fB\s-1DFG\s0\fR converter is specified, then a prover must be

specified as well. Default is \fBdfg2otter.pl\fR.

.SH "SEE ALSO"

.IX Header "SEE ALSO"

\&\fIcheckstat\fR\|(1), \fIfilestat\fR\|(1), \fIpgen\fR\|(1), \fIrescmp\fR\|(1), \fItpform\fR\|(1), \fItpget\fR\|(1), \fIdeprose\fR\|(1), \fIdfg2otter\fR\|(1), \fIdfg2otterpl\fR\|(1), \s-1\fISPASS\s0\fR\|(1)

.SH "AUTHORS"

.IX Header "AUTHORS"

Thorsten Engel and Christian Theobalt.

.PP

Contact : Thomas Hillenbrand <hillen@mpi\-sb.mpg.de>

          Christoph Weidenbach <weidenb@mpi\-sb.mpg.de>