This file is indexed.

/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"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="script_5.html#SEC32" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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>&nbsp;</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>&lt;root&gt;&lt;suffix&gt;</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"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="script_5.html#SEC32" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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>