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 2008-06A</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>
|