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
|
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: References</title>
<link rel="stylesheet" href="manual.css">
</head>
<body>
<!-- Site navigation menu -->
<ul class="navbar">
<li><a href="index.html">Introduction</a>
<li><a href="install.html">Installation</a>
<li><a href="running.html">Running Prover9</a>
<li><a href="input.html">Input Files</a>
<li><a href="syntax.html">Clauses & Formulas</a>
<li>Search Prep
<ul class="navbar2">
<li><a href="auto.html">Auto Modes</a>
<li><a href="term-order.html">Term Ordering</a>
<li><a href="more-prep.html">More Prep</a>
<li><a href="limits.html">Search Limits</a>
</ul>
<li>Inference
<ul class="navbar2">
<li><a href="loop.html">The Loop</a>
<li><a href="select.html">Select Given</a>
<li><a href="inf-rules.html">Inference Rules</a>
<li><a href="process-inf.html">Process Inferred</a>
</ul>
<li><a href="output.html">Output Files</a>
<li>More Features
<ul class="navbar2">
<li><a href="weight.html">Weighting</a>
<li><a href="attributes.html">Attributes</a>
<li><a href="actions.html">Actions</a>
<li><a href="fof-reduction.html">FOF Reduction</a>
<li><a href="goals.html">Goals</a>
<li><a href="hints.html">Hints</a>
<li><a href="semantics.html">Semantics</a>
</ul>
<li>Related Programs
<ul class="navbar2">
<li><a href="prooftrans.html">Prooftrans</a>
<li><a href="mace4.html">Mace4</a>
</ul>
<li>Ending
<ul class="navbar2">
<li><a href="options.html">All Options</a>
<li><a href="glossary.html">Glossary</a>
<li><a href="manual-index.html">Index</a>
<li><a href="references.html">References</a>
</ul>
</ul>
<div class="header">Prover9 Manual Version June-2006</div>
<!-- Main content -->
<h1>References</h1>
<i>Not done yet.</i>
<dl class = "references">
<a name="Champeaux-miniscope">
<dt>[Champeaux-miniscope]</dt>
<dd>
D. Champeaux.
Sub-problem finder and instance checker, two cooperating modules for
theorem provers.
<I>J. ACM</I>, 33(4):633--657, 1986.
</dd>
<a name="Dershowitz-termination">
<dt>[Dershowitz-termination]</dt>
<dd>
N. Dershowitz.
Termination of rewriting.
<I>J. Symbolic Computation</I>, 3:69-116, 1987.
</dd>
<a name="McCune-Otter33">
<dt>[McCune-Otter33]</dt>
<dd>
W. McCune.
Otter 3.3 Reference Manual.
Tech. Memo ANL/MCS-TM-263, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, August 2003.
</dd>
<a name="McCune-Mace4">
<dt>[McCune-Mace4]</dt>
<dd>
W. McCune.
Mace4 Reference Manual and Guide.
Tech. Memo ANL/MCS-TM-264, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, August 2003.
</dd>
<a name="RV-lrs">
<dt>[RV-lrs]</dt>
<dd>
A. Riazanov and A. Voronkov.
Limited resource strategy in resolution theorem proving.
<I>J. Symbolic Computation</I>, 36(1-2):101-115, 2003.
</dd>
<a name="Veroff-hints">
<dt>[Veroff-hints]</dt>
<dd>
R. Veroff.
Using hints to increase the effectiveness of an automated reasoning
program: Case studies.
<I>J. Automated Reasoning</I>, 16(3):223--239, 1996.
</dd>
<a name="Veroff-sketches">
<dt>[Veroff-sketches]</dt>
<dd>
R. Veroff.
Solving open questions and other challenge problems using proof
sketches.
<I>J. Automated Reasoning</I>, 27(2):157--174, 2001.
</dd>
</dl>
</body>
</html>
|
