| --- /dev/null 2012-01-07 09:10:22.797165727 +1100 |
| +++ LADR-2009-11A/manpages/clausefilter.1 2012-01-07 19:30:44.311801364 +1100 |
| @@ -0,0 +1,43 @@ |
| +.TH CLAUSEFILTER 1 "January 20, 2007" |
| +.SH NAME |
| +clausefilter - filter formulas with models |
| +.SH SYNOPSIS |
| +.B clausefilter |
| +.RI < interpretations-file > |
| +.RI < test > |
| +< |
| +.RI < formulas-file > |
| +> |
| +.RI < passing-formulas-file > |
| +.SH DESCRIPTION |
| +This manual page documents briefly the |
| +.B clausefilter |
| +command. |
| +.PP |
| +Given a set of \fIinterpretations\fP, a \fItest\fP to perform, and a |
| +stream of \fIformulas\fP, \fBclausefilter\fP outputs the formulas |
| +that pass the test. |
| +.SH TESTS |
| +The following tests are available. |
| +.TP |
| +.B true_in_all |
| +Formula true in all interpretations. |
| +.TP |
| +.B true_in_some |
| +Formula true in some interpretation. |
| +.TP |
| +.B false_in_all |
| +Formula false in all interpretations. |
| +.TP |
| +.B false_in_some |
| +Formula false in some interpretation. |
| +.SH SEE ALSO |
| +.BR prover9 (1), |
| +.BR mace4 (1). |
| +.br |
| +Full documentation for \fBclausefilter\fP is found in the \fBprover9\fP manual, available on Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP. |
| +.SH AUTHOR |
| +\fBclausefilter\fP was written by William McCune <mccune@cs.unm.edu> |
| +.PP |
| +This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, |
| +for the Debian project (but may be used by others). |
| --- /dev/null 2012-01-07 09:10:22.797165727 +1100 |
| +++ LADR-2009-11A/manpages/clausetester.1 2012-01-07 19:30:44.312801386 +1100 |
| @@ -0,0 +1,29 @@ |
| +.TH CLAUSETESTER 1 "January 20, 2007" |
| +.SH NAME |
| +clausetester - check formulas in models |
| +.SH SYNOPSIS |
| +.B clausetester |
| +.RI < interpretations-file > |
| +< |
| +.RI < formulas-file > |
| +> |
| +.RI < annotated-formulas-file > |
| +.SH DESCRIPTION |
| +This manual page documents briefly the |
| +.B clausetester |
| +command. |
| +.PP |
| +This program takes a set of \fIinterpretations\fP and stream of |
| +\fIformulas\fP. 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. |
| +.SH SEE ALSO |
| +.BR prover9 (1), |
| +.BR mace4 (1). |
| +.br |
| +Full documentation for \fBclausetester\fP is found in the \fBprover9\fP manual, available on Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP. |
| +.SH AUTHOR |
| +\fBclausetester\fP was written by William McCune <mccune@cs.unm.edu> |
| +.PP |
| +This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, |
| +for the Debian project (but may be used by others). |
| --- /dev/null 2012-01-07 09:10:22.797165727 +1100 |
| +++ LADR-2009-11A/manpages/interpfilter.1 2012-01-07 19:30:44.312801386 +1100 |
| @@ -0,0 +1,43 @@ |
| +.TH INTERPFILTER 1 "January 20, 2007" |
| +.SH NAME |
| +interpfilter - filter models with formulas |
| +.SH SYNOPSIS |
| +.B interpfilter |
| +.RI < formulas-file > |
| +.RI < test > |
| +< |
| +.RI < interpretations-file > |
| +> |
| +.RI < passing-interpretations-file > |
| +.SH DESCRIPTION |
| +This manual page documents briefly the |
| +.B interpfilter |
| +command. |
| +.PP |
| +Given a set of \fIformulas\fP, a \fItest\fP to perform, and a |
| +stream of \fIinterpretations\fP, \fBinterpfilter\fP outputs the interpretations |
| +that pass the test. |
| +.SH TESTS |
| +The following tests are available. |
| +.TP |
| +.B all_true |
| +All formulas true in given interpretation. |
| +.TP |
| +.B some_true |
| +Some formula true in given interpretation. |
| +.TP |
| +.B all_false |
| +All formulas false in given interpretation. |
| +.TP |
| +.B some_false |
| +Some formula false in given interpretation. |
| +.SH SEE ALSO |
| +.BR prover9 (1), |
| +.BR mace4 (1). |
| +.br |
| +Full documentation for \fBinterpfilter\fP is found in the \fBprover9\fP manual, available on Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP. |
| +.SH AUTHOR |
| +\fBinterpfilter\fP was written by William McCune <mccune@cs.unm.edu> |
| +.PP |
| +This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, |
| +for the Debian project (but may be used by others). |
| --- /dev/null 2012-01-07 09:10:22.797165727 +1100 |
| +++ LADR-2009-11A/manpages/interpformat.1 2012-01-07 19:30:44.313801403 +1100 |
| @@ -0,0 +1,65 @@ |
| +.TH INTERPFORMAT 1 "January 20, 2007" |
| +.SH NAME |
| +interpformat \- tool for transforming |
| +.BR mace4 (1) |
| +models |
| +.SH SYNOPSIS |
| +.B interpformat |
| +.RI [ options ] |
| +.RI < transformation > |
| +\-f |
| +.I input-file |
| +> |
| +.I output-file |
| +.br |
| +.B interpformat |
| +.RI [ options ] |
| +.RI < transformation > |
| +< |
| +.I input-file |
| +> |
| +.I output-file |
| +.SH DESCRIPTION |
| +The models (structures) in |
| +.BR mace4 (1) |
| +output files can be transformed in various ways with the program \fBinterpformat\fP. |
| +.SH TRANSFORMATIONS |
| +The transformations are listed here. |
| +.TP |
| +.B standard |
| +one line per operation |
| +.TP |
| +.B standard2 |
| +standard, with binary operations in a square (default) |
| +.TP |
| +.B portable |
| +list of lists, suitable for parsing by Python, GAP, etc. |
| +.TP |
| +.B tabular |
| +as nice tables |
| +.TP |
| +.B raw |
| +similar to standard, but without punctuation |
| +.TP |
| +.B cooked |
| +as terms, e.g., f(0,1)=2 |
| +.TP |
| +.B tex |
| +formatted for LaTeX |
| +.TP |
| +.B xml |
| +XML |
| +.SH OPTIONS |
| +A summary of options is included below. |
| +.TP |
| +.B output \fI<operations> |
| +Output only the listed \fIoperations\fP. |
| +.SH SEE ALSO |
| +.BR mace4 (1). |
| +.br |
| +Full documentation for \fBinterpformat\fP is found in the \fBprover9\fP manual, available on Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP. |
| +.SH AUTHOR |
| +\fBinterpformat\fP was written by William McCune <mccune@cs.unm.edu> |
| +.PP |
| +This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, |
| +for the Debian project (but may be used by others). |
| --- /dev/null 2012-01-07 09:10:22.797165727 +1100 |
| +++ LADR-2009-11A/manpages/isofilter.1 2012-01-07 19:30:44.313801403 +1100 |
| @@ -0,0 +1,65 @@ |
| +.TH ISOFILTER 1 "January 20, 2007" |
| +.SH NAME |
| +isofilter - removes isomorphic structures from |
| +.BR mace4 (1) |
| +models |
| +.SH SYNOPSIS |
| +.B isofilter |
| +.RI [ options ] |
| +< |
| +.I input-file |
| +> |
| +.I output-file |
| +.br |
| +.B isofilter0 |
| +.RI [ options ] |
| +< |
| +.I input-file |
| +> |
| +.I output-file |
| +.br |
| +.B isofilter2 |
| +.RI [ options ] |
| +< |
| +.I input-file |
| +> |
| +.I output-file |
| +.SH DESCRIPTION |
| +This manual page documents briefly the \fBisofilter\fP, \fBisofilter0\fP and \fBisofilter2\fP commands. |
| +.PP |
| +If |
| +.BR mace4 (1) |
| +produces more than one structure, some of them are very likely to be |
| +isomorphic to others. The program \fBisofilter\fP can be used to remove isomorphic |
| +structures. |
| +.SH ALGORITHM |
| +There are multiple \fBisofilter\fP variants providing alternative algorithms. |
| +.TP |
| +.B isofilter |
| +Uses Occurrence Profiles algorithm. |
| +.TP |
| +.B isofilter2 |
| +Uses Canonical Forms algorithm. |
| +.SH OPTIONS |
| +A summary of options is included below. |
| +.TP |
| +.B ignore_constants |
| +Ignore all constants during the isomorphism tests. |
| +.TP |
| +.B check \fI<operations> |
| +Consider only the listed \fIoperations\fP in the isomorphism tests. |
| +.TP |
| +.B output \fI<operations> |
| +Output only the listed \fIoperations\fP. |
| +.TP |
| +.B wrap |
| +Enclose the resulting structures in \fBlist(interpretations). ... end_of_list.\fP |
| +.SH SEE ALSO |
| +.BR mace4 (1). |
| +.br |
| +Full documentation for \fBisofilter\fP is found in the \fBprover9\fP manual, available on Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP. |
| +.SH AUTHOR |
| +\fBisofilter\fP was written by William McCune <mccune@cs.unm.edu> |
| +.PP |
| +This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, |
| +for the Debian project (but may be used by others). |
| --- LADR-2009-11A-orig/manpages/mace4.1 2007-12-31 15:43:54.000000000 +1100 |
| +++ LADR-2009-11A/manpages/mace4.1 2012-01-07 19:55:18.746508266 +1100 |
| @@ -76,11 +76,11 @@ |
| .SH SEE ALSO |
| .BR prover9 (1). |
| .br |
| -Full documentation for \fBmace4\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP. |
| +Full documentation for \fBmace4\fP is found in the \fBprover9\fP manual, available on Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP. |
| .br |
| The original \fBmace4\fP manual, which can be downloaded at http://www.cs.unm.edu/~mccune/prover9/mace4.pdf |
| .SH AUTHOR |
| -\fBmace4\fP ws written by William McCune <mccune@cs.unm.edu> |
| +\fBmace4\fP was written by William McCune <mccune@cs.unm.edu> |
| .PP |
| This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, |
| for the Debian project (but may be used by others). |
| --- /dev/null 2012-01-07 09:10:22.797165727 +1100 |
| +++ LADR-2009-11A/manpages/prooftrans.1 2012-01-07 19:30:44.314801424 +1100 |
| @@ -0,0 +1,73 @@ |
| +.TH PROOFTRANS 1 "January 20, 2007" |
| +.SH NAME |
| +prooftrans - tool for transforming Prover9 proofs |
| +.SH SYNOPSIS |
| +.B prooftrans |
| +.RI [ parents_only ] |
| +.RI [ expand ] |
| +.RI [ renumber ] |
| +.RI [ striplabels ] |
| +[\fI-f file\fP] |
| +.br |
| +.B prooftrans |
| +xml |
| +.RI [ expand ] |
| +.RI [ renumber ] |
| +.RI [ striplabels ] |
| +[\fI-f file\fP] |
| +.br |
| +.B prooftrans |
| +ivy |
| +.RI [ renumber ] |
| +[\fI-f file\fP] |
| +.br |
| +.B prooftrans |
| +hints |
| +[\fI-label label\fP] |
| +.RI [ expand ] |
| +.RI [ striplabels ] |
| +[\fI-f file\fP] |
| +.SH DESCRIPTION |
| +This manual page documents briefly the |
| +.B prooftrans |
| +command. |
| +.PP |
| +\fBprooftrans\fP can extract proofs from |
| +.BR prover9 (1) |
| +output files and transform them in various ways. |
| + |
| +.SH OPTIONS |
| +A summary of options is included below. |
| +.TP |
| +.B renumber |
| +Renumber steps. |
| +.TP |
| +.B parents_only |
| +Simplify justifications by listing only parents. |
| +.TP |
| +.B expand |
| +Expand all steps, turning secondary justifications into explicit steps. |
| +.TP |
| +.B xml |
| +Produce proofs in XML. |
| +.TP |
| +.B ivy |
| +Produce proofs for checking by the IVY proof checker. |
| +.TP |
| +.B hints |
| +Produce hints for guiding subsequent searches. |
| +.TP |
| +.B \-label \fIlabel\fP |
| +Attach label attributes to the hint clauses consisting of the string \fIlabel\fP and a sequence number generated by prooftrans. |
| +.TP |
| +.B \-f \fIfile |
| +Take input from \fIfile\fP instead of from standard input. |
| +.SH SEE ALSO |
| +.BR prover9 (1). |
| +.br |
| +Full documentation for \fBprooftrans\fP is found in the \fBprover9\fP manual, available on Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP. |
| +.SH AUTHOR |
| +\fBprooftrans\fP was written by William McCune <mccune@cs.unm.edu> |
| +.PP |
| +This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, |
| +for the Debian project (but may be used by others). |
| --- LADR-2009-11A-orig/manpages/prover9.1 2007-12-31 15:43:54.000000000 +1100 |
| +++ LADR-2009-11A/manpages/prover9.1 2012-01-07 19:54:30.928968388 +1100 |
| @@ -11,7 +11,7 @@ |
| .br |
| .B prover9 |
| .RI [ options ] |
| --f |
| +\-f |
| .I input-file |
| > |
| .I output-file |
| @@ -38,15 +38,15 @@ |
| .B \-t \fIn |
| Constrain the search to last about \fIn\fP seconds. For UNIX-like systems, the `user CPU' time is used. |
| .TP |
| -.B \-f \fIfiles |
| -Take input from \fIfiles\fP instead of from standard input. |
| +.B \-f \fIfile |
| +Take input from \fIfile\fP instead of from standard input. |
| .SH SEE ALSO |
| .BR mace4 (1), |
| .BR otter (1). |
| .br |
| -On Debian systems, the manual is found in the \fIprover9-doc\fP package, at \fI/usr/share/doc/prover9-doc/manual/index.html\fP. |
| +On Gentoo systems, the manual is found at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP. |
| .SH AUTHOR |
| -\fBprover9\fP ws written by William McCune <mccune@cs.unm.edu> |
| +\fBprover9\fP was written by William McCune <mccune@cs.unm.edu> |
| .PP |
| This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, |
| for the Debian project (but may be used by others). |
| --- /dev/null 2012-01-07 09:10:22.797165727 +1100 |
| +++ LADR-2009-11A/manpages/prover9-apps.1 2012-01-07 19:30:44.315801449 +1100 |
| @@ -0,0 +1,17 @@ |
| +.TH PROVER9-APPS 1 "June 18, 2008" |
| +.SH NAME |
| +prover9-apps \- undocumented Prover9 applications |
| +.SH DESCRIPTION |
| +Some programs in the \fBprover9-apps\fP package currently have no manual |
| +pages. You can obtain documentation on some of these applications via the |
| +\fBprover9\fP manual, which is available |
| +at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP. |
| +Alternatively invoking the application with the \fB-help\fP option may |
| +produce documentation. Patches to add manual pages are welcome, and may |
| +be sent to the Debian package maintainer, whose details are listed below. |
| +.SH AUTHOR |
| +The applications were written by William McCune <mccune@cs.unm.edu>. |
| +.PP |
| +This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, |
| +for the Debian project (but may be used by others) and modified for Fedora |
| +by Tim Colles <timc@inf.ed.ac.uk>. |
| --- /dev/null 2012-01-07 09:10:22.797165727 +1100 |
| +++ LADR-2009-11A/manpages/rewriter.1 2012-01-07 19:30:44.315801449 +1100 |
| @@ -0,0 +1,60 @@ |
| +.de Sp \" Vertical space (when we can't use .PP) |
| +.if t .sp .5v |
| +.if n .sp |
| +.. |
| +.de Vb \" Begin verbatim text |
| +.ft CW |
| +.nf |
| +.ne \\$1 |
| +.. |
| +.de Ve \" End verbatim text |
| +.ft R |
| +.fi |
| +.. |
| +.TH REWRITER 1 "January 20, 2007" |
| +.SH NAME |
| +rewriter - demodulate terms |
| +.SH SYNOPSIS |
| +.B rewriter |
| +.RI < demodulators-file > |
| +< |
| +.RI < terms-file > |
| +> |
| +.RI < rewritten-terms-file > |
| +.SH DESCRIPTION |
| +This manual page documents briefly the |
| +.B rewriter |
| +command. |
| +.PP |
| +Rewrite a stream of \fIterms\fP with a list of \fIdemodulators\fP. The |
| +demodulators are used left-to-right as given, and they are not checked |
| +for termination. |
| +.SH SYNTAX |
| +The file of demodulators contains optional commands |
| +then a list of demodulators. The commands can be used to |
| +declare infix operations and associativity/commutativity. |
| +Example file of demodulators: |
| +.Sp |
| +.Vb 10 |
| +\& op(400, infix, ^). |
| +\& op(400, infix, v). |
| +\& assoc_comm(^). |
| +\& assoc_comm(v). |
| +\& formulas(demodulators). |
| +\& x ^ x = x. |
| +\& x ^ (x v y) = x. |
| +\& x v x = x. |
| +\& x v (x ^ y) = x. |
| +\& end_of_list. |
| +.Ve |
| +.Sp |
| +.SH SEE ALSO |
| +.BR prover9 (1), |
| +.BR mace4 (1). |
| +.br |
| +Full documentation for \fBrewriter\fP is found in the \fBprover9\fP manual, available on Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP. |
| +.SH AUTHOR |
| +\fBrewriter\fP was written by William McCune <mccune@cs.unm.edu> |
| +.PP |
| +This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, |
| +for the Debian project (but may be used by others). |