Il s'agit de la commande prouver9 qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks à l'aide de 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
prouveur9 - prouveur de théorème de résolution/paramodulation
SYNOPSIS
prouve9 [Options] fichier-entrée > fichier de sortie
prouve9 [Options] -F fichier-entrée > fichier de sortie
DESCRIPTION
Cette page de manuel documente brièvement les prouve9 commander.
prouve9 est un prouveur de théorèmes automatisé pour la logique du premier ordre et équationnelle. C'est un
successeur du loutre(1) prouveur. prouve9 utilise les techniques d'inférence de
résolution et paramodulation avec sélection littérale.
OPTIONS
Un résumé des options est inclus ci-dessous.
-h Affichez une liste d'options de ligne de commande.
-x Active un mode automatique amélioré expérimental. Pour plus d'informations consultez le
prouve9 manuel.
-p Sortie entièrement entre parenthèses.
-t n Contraindre la recherche à durer environ n secondes. Pour les systèmes de type UNIX, l'utilisateur
Le temps CPU est utilisé.
-f filet
Recueillir les commentaires de filet au lieu de l'entrée standard.
Utilisez prouver9 en ligne en utilisant les services onworks.net