This is the command prooftrans that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
PROGRAM:
NAME
prooftrans - tool for transforming Prover9 proofs
SYNOPSIS
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]
prooftrans tagged [-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.
tagged Produce proofs in a structured tagged format.
-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.
Use prooftrans online using onworks.net services
