/usr/share/doc/prover9-doc/html/clause-properties.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 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: Clause Properties</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>Clause Properties (Advanced)</h1>
Several Prover9 features
(<a href="white-black.html">keep/delete rules</a> and
<a href="select2.html">given-selection rules</a>)
allow the user to specify subsets of
clauses by using a simple language. Examples are clauses to keep,
clauses to discard, and clauses to be selected as given clauses.
For example, to specify Horn clauses with more than three literals,
one can write the rule
<pre class="my_file">
horn & literals>3.
</pre>
<h3>Basic Properties:</h3>
<p>
<table "border" cellpadding="5">
<tr>
<td><tt>positive</tt> <td> all literals are positive
<tr>
<td><tt>negative</tt> <td> all literals are negative
<tr>
<td><tt>mixed</tt> <td> contains positive literals and negative literals
<tr>
<td><tt>unit</tt> <td> exactly one literal
<tr>
<td><tt>horn</tt> <td> the clause has at most one positive literal
<tr>
<td><tt>definite</tt> <td> the clause has exactly one positive literal
<tr>
<td><tt>has_equality</tt> <td> contains a positive or negative equality literal
<tr>
<td><tt>true</tt> <td> true in interpretations(s)
<tr>
<td><tt>false</tt> <td> false in interpretations(s)
<tr>
<td><tt>hint</tt> <td> the clause matches a hint
<tr>
<td><tt>initial</tt> <td> the clause was present before the selection of the first given clause
<tr>
<td><tt>resolvent</tt> <td> the clause is a (binary) resolvent
<tr>
<td><tt>hyper_resolvent</tt> <td> the clause is a hyperresolvent
<tr>
<td><tt>ur_resolvent</tt> <td> the clause is a unit-resulting (UR) resolvent
<tr>
<td><a href="process-inf.html#factor"><tt><b>factor</b></tt></a> <td> the clause is a (binary) factor
<tr>
<td><tt>paramodulant</tt> <td> the clause is a paramodulant
<tr>
<td><tt>back_demodulant</tt> <td> the clause is a back demodulant
<tr>
<td><tt>subsumer</tt> <td> the clause back subsumed another clause
<tr>
<td><tt>all</tt> <td> all clauses have this property
</table>
<h3>Integral Properties</h3>
The following properties are used with relations <, <=, =, >=, >.
<p>
<table "border" cellpadding="5">
<tr>
<td><tt>weight</tt> <td> weight of the clause
<tr>
<td><tt>literals</tt> <td> number of literals in the clause
<tr>
<td><tt>variables</tt> <td> number of (distinct) variables in the clause
<tr>
<td><tt>depth</tt> <td> depth of the deepest term in the clause
<tr>
<td><tt>level</tt> <td> level of the clause (derivation distance from input)
</table>
<h3>Boolean Combinations</h3>
Non-atomic expressions are constructed in the same way as ordinary formulas,
with the following operations.
<p>
<table "border" cellpadding="5">
<tr>
<td><tt>&</tt> <td> conjunction
<tr>
<td><tt>|</tt> <td> disjunction
<tr>
<td><tt>-</tt> <td> negation
</table>
<!--
<hr>
Next Section:
<a href="goals.html">Goals and Denials</a>
-->
</body>
</html>
|