/usr/share/spass/html/script_4.html is in spass 3.7-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html401/loose.dtd">
<html>
<!-- Created on February, 23 2010 by texi2html 1.78 -->
<!--
Written by: Lionel Cons <Lionel.Cons@cern.ch> (original author)
Karl Berry <karl@freefriends.org>
Olaf Bachmann <obachman@mathematik.uni-kl.de>
and many others.
Maintained by: Many creative people.
Send bugs and suggestions to <texi2html-bug@nongnu.org>
-->
<head>
<title>frequently asked questions about SPASS: 4. pcs</title>
<meta name="description" content="frequently asked questions about SPASS: 4. pcs">
<meta name="keywords" content="frequently asked questions about SPASS: 4. pcs">
<meta name="resource-type" content="document">
<meta name="distribution" content="global">
<meta name="Generator" content="texi2html 1.78">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css">
<!--
a.summary-letter {text-decoration: none}
pre.display {font-family: serif}
pre.format {font-family: serif}
pre.menu-comment {font-family: serif}
pre.menu-preformatted {font-family: serif}
pre.smalldisplay {font-family: serif; font-size: smaller}
pre.smallexample {font-size: smaller}
pre.smallformat {font-family: serif; font-size: smaller}
pre.smalllisp {font-size: smaller}
span.roman {font-family:serif; font-weight:normal;}
span.sansserif {font-family:sans-serif; font-weight:normal;}
ul.toc {list-style: none}
-->
</style>
</head>
<body lang="en" bgcolor="#FFFFFF" text="#000000" link="#0000FF" vlink="#800080" alink="#FF0000">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="script_3.html#SEC18" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="script_5.html#SEC32" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="script.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[Contents]</td>
<td valign="middle" align="left">[Index]</td>
<td valign="middle" align="left">[<a href="script_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<hr size="2">
<a name="pcs"></a>
<a name="SEC25"></a>
<h1 class="chapter"> 4. pcs </h1>
<hr size="6">
<a name="SEC26"></a>
<h2 class="section"> 4.1 NAME </h2>
<p>pcs - checks SPASS proofs
</p>
<hr size="6">
<a name="SEC27"></a>
<h2 class="section"> 4.2 SYNOPSIS </h2>
<p><strong>pcs</strong> [ -cdfrstv] file
</p>
<hr size="6">
<a name="SEC28"></a>
<h2 class="section"> 4.3 DESCRIPTION </h2>
<p><strong>pcs</strong> is a Perl script that supports automatic checking of proofs specified in
<strong>DFG</strong> syntax with the theorem prover <small>OTTER</small>.
It uses
</p><ul>
<li>
the C-program <strong>pgen</strong>, which generates proof tasks corresponding to inference steps for each proof step of a <strong>DFG</strong> proof and checks the tableau structure.
</li><li>
the C-program <strong>SPASS</strong> with the -Flotter option for converting
<strong>DFG</strong> syntax files with formulas into <strong>DFG</strong> syntax files with
clauses.
</li><li>
the C-program dfg2otter, which transforms files in <strong>DFG</strong> syntax with
clauses only into files for <small>OTTER</small> syntax.
</li></ul>
<p><strong>pcs</strong> checks that:
</p><ul>
<li>
The conclusion in each proof step is a logical consequence
of the assumptions in that proof step.
</li><li>
Each clause in a subtableau uses only parents clauses that are
visible at this point in the tableau.
</li><li>
Each clause, except for split clauses, has the maximum
split level of its parents.
</li><li>
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.
</li><li>
The tableau is complete and closed.
</li></ul>
<p>The second condition is verified by checking the unsatisfiability
</p><table><tr><td> </td><td><pre class="example"><em>Assumptions \wedge \neg Conclusion</em>
</pre></td></tr></table>
<p>for each proof step (inference rule application) by running <small>OTTER</small>
for a limited time. The appropriate <strong>DFG</strong> files for these problems
are generated by <strong>pgen</strong>. <small>OTTER</small> may fail to terminate
within this time, leaving the correctness of a proof step undecided,
which leads to the three possible results of <strong>pcs</strong>:
</p><ul>
<li>
The proof is correct: Both conditions are satisfied for all proof steps.
</li><li>
The proof is not correct: One condition is definitely violated for
at least one proof step.
</li><li>
Correctness is undecided: The first condition is satisfied,
but the second condition could not be verified nor falsified for at least
one proof step.
</li></ul>
<p><strong>pcs</strong> uses a working directory, in which all proof tasks corresponding to the proof steps
are generated using the <strong>pgen</strong> program. These tasks are subsequently
checked using <small>OTTER</small>.
</p>
<hr size="6">
<a name="SEC29"></a>
<h2 class="section"> 4.4 OPTIONS </h2>
<p>Several options control the behavior
of <strong>pcs</strong> when it fails to verify a proof step, its output and the
naming of generated files and the working directory:
</p>
<dl compact="compact">
<dt> <kbd>-c</kbd></dt>
<dd><p>Continue even if a single proof step could not be verified. Default 'off'.
</p></dd>
<dt> <kbd>-d <i>suffix</i></kbd></dt>
<dd><p>Suffix of created working directory. For an input file
<i>root.ext</i>, the working directory <i><root><suffix></i> is created. If <i>suffix</i> does not end with a backslash, it is taken as a <i>prefix</i> for files generated by <strong>pgen</strong>, which are then created in the current working directory. Default is '_SubProofs/'.
</p></dd>
<dt> <kbd>-f</kbd></dt>
<dd><p>Overwrite working directory if it already exists. Default 'off'.
</p></dd>
<dt> <kbd>-o</kbd></dt>
<dd><p>Use <strong>SPASS</strong> as proof checker instead of <small>OTTER</small>. This option is
especially useful when checking proofs generated by a different prover.
Default is 'off'.
</p></dd>
<dt> <kbd>-p <i>path</i></kbd></dt>
<dd><p>Location of <strong>DFG</strong> prover to be used instead of the default one. If -o is
specified, then it overrides this option, and <strong>SPASS</strong> is used
instead. If a <strong>DFG</strong> converter is specified, then a prover must be
specified as well. Default is <small>OTTER</small>.
</p></dd>
<dt> <kbd>-q</kbd></dt>
<dd><p>Be quiet and do not print program paths. This option is especially useful inside <strong>checkstat</strong>. Default is 'off'.
</p></dd>
<dt> <kbd>-r</kbd></dt>
<dd><p>Clean up all generated files at the end, even if the proof is not valid.
Default 'off'.
</p></dd>
<dt> <kbd>-s <i>suffix</i></kbd></dt>
<dd><p>Suffix of files generated by <strong>pgen</strong>. Default is '.dfg'.
</p></dd>
<dt> <kbd>-t <i>limit</i></kbd> </dt>
<dd><p>Number of seconds for each proof attempt
for each proof step. Default is 3 seconds.
</p></dd>
<dt> <kbd>-v</kbd></dt>
<dd><p>(verbose) Give some progress information. Default is 'off'.
</p></dd>
<dt> <kbd>-w <i>path</i></kbd></dt>
<dd><p>Location of <strong>DFG</strong> converter to be used instead of the default one.
If a <strong>DFG</strong> converter is specified, then a prover must be
specified as well. Default is <strong>dfg2otter.pl</strong>.
</p>
</dd>
</dl>
<hr size="6">
<a name="SEC30"></a>
<h2 class="section"> 4.5 AUTHORS </h2>
<p>Thorsten Engel and Christian Theobalt.
</p>
<p>Contact : spass@mpi-inf.mpg.de
</p>
<hr size="6">
<a name="SEC31"></a>
<h2 class="section"> 4.6 SEE ALSO </h2>
<p>checkstat(1), filestat(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
</p>
<hr size="6">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#SEC25" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="script_5.html#SEC32" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="script.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[Contents]</td>
<td valign="middle" align="left">[Index]</td>
<td valign="middle" align="left">[<a href="script_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<p>
<font size="-1">
This document was generated by <em>Christoph Weidenbach</em> on <em>February, 23 2010</em> using <a href="http://www.nongnu.org/texi2html/"><em>texi2html 1.78</em></a>.
</font>
<br>
</p>
</body>
</html>
|