Rechercher une page de manuel
prover9-prooftrans
Langue: en
Version: 149160 (fedora - 04/07/09)
Section: 1 (Commandes utilisateur)
NAME
prooftrans - tool for transforming Prover9 proofsSYNOPSIS
prooftrans [parents_only] [expand] [renumber] [striplabels] [-f file]prooftrans xml [expand] [renumber] [striplabels] [-f file]
prooftrans ivy [renumber] [-f file]
prooftrans hints [-label label] [expand] [striplabels] [-f file]
DESCRIPTION
This manual page documents briefly the prooftrans command.prooftrans can extract proofs from prover9(1) output files and transform them in various ways.
OPTIONS
A summary of options is included below.- renumber
- Renumber steps.
- parents_only
- Simplify justifications by listing only parents.
- expand
- Expand all steps, turning secondary justifications into explicit steps.
- xml
- Produce proofs in XML.
- ivy
- Produce proofs for checking by the IVY proof checker.
- hints
- Produce hints for guiding subsequent searches.
- -label label
- Attach label attributes to the hint clauses consisting of the string label and a sequence number generated by prooftrans.
- -f file
- Take input from file instead of from standard input.
SEE ALSO
prover9(1).Full documentation for prooftrans is found in the prover9 manual, available on Debian systems in the prover9-doc package at /usr/share/doc/prover9-doc/manual/index.html.
AUTHOR
prooftrans was written by William McCune <mccune@cs.unm.edu>This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, for the Debian project (but may be used by others).
Contenus ©2006-2024 Benjamin Poulain
Design ©2006-2024 Maxime Vantorre