/usr/share/doc/prover9-doc/html/references.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 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: References</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>References</h1>
<i>Not done yet.</i>
<dl class = "references">
<a name="Bachmair-Ganzinger-res">
<dt>[Bachmair-Ganzinger-res]</dt>
<dd>
L. Bachmair and H. Ganzinger.
"Resolution Theorem Proving".
Chapter 2 in
<i>Handbook of Automated Reasoning</i>
(ed. A. Robinson and A. Voronkov), 2001.
<a href="http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1997-2-005">Preliminary version.</a>
</dd>
<a name="Nieuwenhuis-Rubio-para">
<dt>[Nieuwenhuis-Rubio-para]</dt>
<dd>
R. Nieuwenhuis and A. Rubio.
"Paramodulation-Based Theorem Proving".
Chapter 7 in
<i>Handbook of Automated Reasoning</i>
(ed. A. Robinson and A. Voronkov), 2001.
</dd>
<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.
<i>Otter 3.3 Reference Manual</i>.
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.
<i>Mace4 Reference Manual and Guide</i>.
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>
|