Il s'agit de la commande prooftrans qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS
PROGRAMME:
Nom
prooftrans - outil de transformation des preuves Prover9
SYNOPSIS
preuvetrans [parents_seulement] [expand] [renuméroter] [étiquettes à bande] [-f filet]
preuvetrans XML [expand] [renuméroter] [étiquettes à bande] [-f filet]
preuvetrans lierre [renuméroter] [-f filet]
preuvetrans conseils [-étiquette étiquette] [expand] [étiquettes à bande] [-f filet]
preuvetrans tagué [-f filet]
DESCRIPTION
Cette page de manuel documente brièvement les preuvetrans commander.
preuvetrans peut extraire des preuves de prouve9(1) les fichiers de sortie et les transformer en divers
façons.
OPTIONS
Un résumé des options est inclus ci-dessous.
renuméroter
Renuméroter les étapes.
parents_seulement
Simplifiez les justifications en ne listant que les parents.
expand Développez toutes les étapes en transformant les justifications secondaires en étapes explicites.
xml Produire des preuves en XML.
lierre Produire des épreuves pour vérification par le vérificateur d'épreuves IVY.
indices Produire des conseils pour guider les recherches ultérieures.
tagged Produisez des épreuves dans un format étiqueté structuré.
-étiquette étiquette
Attachez les attributs d'étiquette aux clauses d'indication constituées de la chaîne étiquette et
numéro de séquence généré par preuvetrans.
-f filet
Recueillir les commentaires de filet au lieu de l'entrée standard.
Utilisez preuvetrans en ligne en utilisant les services onworks.net
