path: root/sci-mathematics/prover9/files/LADR-2009-11A-manpages.patch

--- /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).