/usr/share/doc/prover9-doc/html/others.html is in prover9-doc 0.0.200902a-2.
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 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: Other LADR Prograns</title>
<link rel="stylesheet" href="manual.css">
</head>
<body>
<hr>
<table width="100%">
<tr>
<colgroup>
<col width="33%">
<col width="34%">
<col width="33%">
</colgroup>
<td align="left"><i>Prover9 Manual</i>
<td align="center"><img src="prover9-5a-256t.gif">
<td align="right"><i>Version 2009-02A</i>
</table>
<hr>
<!-- Main content -->
<h1>Other LADR Prograns</h1>
The page describes several other programs that have constructed
with the same code base (LADR) as
<a href="intro.html">Prover9</a>,
<a href="prooftrans.html">Prooftrans</a>,
<a href="mace4.html">Mace4</a>, and
<a href="mace4.html#interpformat">Interpformat</a>.
<p>
When we write that a program takes a "stream" of objects, we mean
that it reads them from the standard input, and the objects are
<i>not</i> enclosed in <tt>objects(..)</tt> and <tt>end_of_list</tt>.
<p>
When we write that a program takes a "set" of objects, we mean
that the filename containing the objects is an argument to
the program, and the objects are <i>not</i> enclosed in
<tt>objects(..)</tt> and <tt>end_of_list</tt>.
<p>
When we write that a program takes a "list" of objects, we mean
that the filename containing the objects is an argument to
the program, and the objects are enclosed in
<tt>objects(..)</tt> and <tt>end_of_list</tt>.
<p>
Contents
<ul>
<li><a href="#clausefilter">Clausefilter</a> -- filter formulas with models
<li><a href="#clausetester">Clausetester</a> -- check formulas in models
<li><a href="#interpfilter">Interpfilter</a> -- filter models with formulas
<li><a href="#rewriter">Rewriter</a> -- demodulate terms
<li><a href="#tptp_to_ladr">TPTP_to_LADR</a> -- translate TPTP formulas to LADR formulas
<li><a href="#ladr_to_tptp">LADR_to_TPTP</a> -- translate LADR formulas to TPTP formulas
</ul>
<hr>
<h2><a name="clausefilter">Clausefilter</a></h2>
Given a set of interpretations, a test to perform,
and a stream of formulas, this program outputs the formulas
that pass the test. (If non-clausal formulas with free
variables are given, their universal closures are used and output.)
<p>
The accepted tests are
<tt>true_in_all</tt>, <tt>true_in_some</tt>,
<tt>false_in_all</tt>, and <tt>false_in_some</tt>.
<p>
Example: given a set of non-modular orthomodular lattices
and a stream of identities, print the identities that
are false in all of the lattices. This job was used
when searching for modular ortholattice (MOL)
single axioms: any MOL single axiom is false in all non MOLs.
<pre class="my_job">
clausefilter <a href="../examples/non-MOL-OML.interps">non-MOL-OML.interps</a> false_in_all < <a href="../examples/MOL-cand.296">MOL-cand.296</a> > <a href="../examples/MOL-cand.238">MOL-cand.238</a>
</pre>
<hr>
<h2><a name="clausetester">Clausetester</a></h2>
This program takes a set of interpretations and stream of
formulas. For each formula, the interpretations in
which the formula is true are shown, and at the end
the number of formulas true in each interpretation is
shown. (If non-clausal formulas with free
variables are given, their universal closures are used and output.)
<p>
Example:
<pre class="my_job">
clausetester <a href="../examples/uc-18.interps">uc-18.interps</a> < <a href="../examples/uc-hunt.clauses">uc-hunt.clauses</a> > <a href="../examples/uc-hunt.out">uc-hunt.out</a>
</pre>
<hr>
<h2><a name="interpfilter">Interpfilter</a></h2>
Given a set of formulas, a test to perform,
and a stream of interpretations, this program
outputs the interpretations that pass the test.
(If non-clausal formulas with free
variables are given, their universal closures are used.)
<p>
The accepted tests are
<tt>all_true</tt>, <tt>some_true</tt>,
<tt>all_false</tt>, and <tt>some_false</tt>.
<p>
Example: from a list of quasigroups, extract the associative-commutaive ones.
<pre class="my_job">
interpfilter <a href="../examples/assoc-comm.clauses">assoc-comm.clauses</a> all_true < <a href="../examples/qg4.interps">qg4.interps</a> > <a href="../examples/qg4-ac.interps">qg4-ac.interps</a> </pre>
<hr>
<h2><a name="rewriter">Rewriter</a></h2>
Rewrite a stream of terms with a list of demodulators.
The demodulators are used left-to-right as given, and
they are not checked for termination.
<p>
Basic example that canonicalizes group expressions:
<pre class="my_job">
rewriter <a href="../examples/group.demods">group.demods</a> < <a href="../examples/group-terms.in">group-terms.in</a> > <a href="../examples/group-terms.out">group-terms.out</a>
</pre>
This example canonicalizes Boolean ring expressions.
It uses associative-commutative (AC) operations and
the op command to change the parsing rules.
<pre class="my_job">
rewriter <a href="../examples/bool-ring.demods">bool-ring.demods</a> < <a href="../examples/bool-ring.in">bool-ring.in</a> > <a href="../examples/bool-ring.out">bool-ring.out</a>
</pre>
This example rewrites identities in terms of {meet,join,complementation}
into the Sheffer stroke.
<pre class="my_job">
rewriter <a href="../examples/BA-Sheffer.demods">BA-Sheffer.demods</a> < <a href="../examples/BA4.in">BA4.in</a> > <a href="../examples/BA4.out">BA4.out</a>
</pre>
<hr>
<h2>TPTP Translators</h2>
The <a href="http://www.cs.miami.edu/~tptp/">TPTP Problem Library</a> contains
thousands of problems for theorem provers, and the
<a href="http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html">TPTP Language</a>
is widely used in the community.
LADR has two programs to translate between the LADR and TPTP languages.
These programs are new and experimenal, and they do not support all of the
language features.
<h3><a name="tptp_to_ladr">TPTP_to_LADR</a></h2>
This program takes a TPTP problem file and produces a bare input file
suitable for input to Prover9 or Mace4. For example,
<pre class="my_job">
tptp_to_ladr < <a href="../examples/PUZ031-1.tptp">PUZ031-1.tptp</a> > <a href="../examples/PUZ031-1.in">PUZ031-1.in</a>
prover9 -f <a href="../examples/PUZ031-1.in">PUZ031-1.in</a> > <a href="../examples/PUZ031-1.out">PUZ031-1.out</a>
</pre>
If you prefer, those two processes can be piped together:
<pre class="my_job">
tptp_to_ladr < <a href="../examples/PUZ031-1.tptp">PUZ031-1.tptp</a> | prover9 > <a href="../examples/PUZ031-1.out2">PUZ031-1.out2</a>
</pre>
Some of the TPTP language features that are <i>not yet supported</i>
are comment blocks, system comments, real numbers, natural
numbers as distinct objects, and distinct objects with double quotes.
<p>
Some future version of LADR will likely support direct input of TPTP
files to Prover9 and Mace4, without having to invoke a translator.
<h3><a name="ladr_to_tptp">LADR_to_TPTP</a></h2>
This program takes a Prover9 input file and produces a TPTP problem file.
A difficulty with this kind of translation is that TPTP accepts
a more restriced class of function and predicate symbols. When the
translator sees symbols that are not accepted by TPTP, it introduces
new symbols, and it gives the symbol mapping as comments in the output.
Ordinary TPTP constant, function, and predicate symbols must
start with lower case a-z, and any remaining characters must be
alphanumeric or _ (underscore). That is, they must match the
(Unix-style) regular expression "<tt>[a-z][a-zA-Z0-9_]*</tt>".
<p>
Here is an example that contains several unacceptable symbols.
<pre class="my_job">
ladr_to_tptp < <a href="../examples/RBA-2.in">RBA-2.in</a> > <a href="../examples/RBA-2.tptp">RBA-2.tptp</a>
</pre>
Instead of introducing new symbols such as <tt>tptp0</tt>,
you can tell ladr_to_tptp to put single quotes around
unacceptable symbols by using the command-line option -q.
See the following example.
<pre class="my_job">
ladr_to_tptp -q < <a href="../examples/RBA-2.in">RBA-2.in</a> > <a href="../examples/RBA-2q.tptp">RBA-2q.tptp</a>
</pre>
<hr>
Next Section:
<a href="options.html">All Options</a>
</body>
</html>
|