Il s'agit de la commande otter 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
otter - prouveur de théorème de style résolution
SYNOPSIS
loutre < fichier-entrée > fichier de sortie
DESCRIPTION
Cette page de manuel documente brièvement les loutre commander.
loutre est un programme de démonstration de théorème de style résolution pour la logique du premier ordre avec égalité.
loutre inclut les règles d'inférence résolution binaire, hyperrésolution, résolution UR et
paramodulation binaire. Certaines de ses autres capacités et fonctionnalités sont la conversion du premier
ordonner les formules aux clauses, subsomption avant et arrière, affacturage, pondération, réponse
littéraux, ordre des termes, démodulation avant et arrière, fonctions évaluables et
les prédicats, la complétion Knuth-Bendix et la stratégie des indices.
OPTIONS
Aucune option de ligne de commande n'est acceptée ; toutes les options sont données dans le fichier d'entrée.
Utilisez Otter en ligne en utilisant les services onworks.net
