Il s'agit de la commande dfg2dfg 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
dfg2dfg - calcule des approximations de problèmes
SYNOPSIS
dfg2dfg [-corne] [-monadique] [-linéaire] [-shallow] [dans le fichier] [fichier de sortie]
DESCRIPTION
dfg2dfg est un programme qui lit les clauses d'un fichier d'entrée en syntaxe DFG. Alors
calcule une approximation de l'ensemble de clauses en fonction des options de la ligne de commande.
Enfin, il écrit la clause approchée définie dans la syntaxe DFG dans un fichier.
Si ni l'un ni l'autre dans le fichier ni fichier de sortie sont donnés, dfg2dfg lit depuis l'entrée standard et écrit sur
sortie standard. Si un nom de fichier est donné, il lit à partir de ce fichier et écrit la sortie
à la sortie standard. Si plus d'un nom de fichier est donné, dfg2dfg lit depuis le premier
fichier et écrit dans le second.
Les approximations sont décrites en détail technique dans le document séparé dfg2dfg.ps
inclus dans la distribution SPASS.
OPTIONS
dfg2dfg a quatre options de ligne de commande différentes qui peuvent être combinées.
-klaxon
Cette option permet la transformation des clauses non-horn en clauses horn. Chaque
clause sans corne avec n les littéraux positifs sont transformés en n clauses de corne, où le
i-ème clause contient le i-ième littéral positif et tous les littéraux négatifs du non-
clause de corne. Voir aussi la section 3 du document.
-monadique[=n]
Avec cette option, les atomes avec des symboles de prédicat non monadiques sont transformés en symboles monadiques
les atomes. Si n est omis ou n=1 un codage de terme est appliqué, c'est-à-dire tous les non-monadiques
les prédicats sont déplacés au niveau du terme. Avec n=2 une projection est appliquée. Tous les non-
les atomes monadiques sont remplacés par leurs projections d'arguments monadiques. Voir rubrique 4.1
section 4.2 du document pour plus de détails.
-linéaire
Cette approximation transforme une clause avec des littéraux monadiques et une variable non linéaire
occurrences dans les atomes successifs, dans une nouvelle clause avec peut-être plus négative
littéraux, qui ne contient aucune variable non linéaire dans le successeur. Voir section
5 du document pour plus de détails.
-peu profond[=n]
Cette transformation essaie de réduire la profondeur des termes en littéraux positifs. Les
la transformation est appliquée aux clauses horn avec des littéraux monadiques uniquement. Si n est omis
or n=1 une transformation stricte est appliquée, c'est-à-dire préservant l'équivalence, cependant.
Pour n=2 certaines conditions préalables sont supprimées. Cela permet d'appliquer la transformation
plus souvent, mais la transformation ne préserve plus l'équivalence. Pour n=3
encore plus de conditions préalables sont supprimées. Jetez un œil à la section 6.n du papier pour le
détails de l'option de ligne de commande -monadique=n.
Utilisez dfg2dfg en ligne en utilisant les services onworks.net
