dfg2dfg – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

dfg2dfg – Approximationen von Problemen berechnen

ZUSAMMENFASSUNG

dfg2dfg [-horn] [-monadic] [-linear] [-shallow] [im Ordner] [Outfile]

BESCHREIBUNG

dfg2dfg ist ein Programm, das Klauseln aus einer Eingabedatei in DFG-Syntax liest. Es dann
berechnet abhängig von den Befehlszeilenoptionen eine Annäherung an den Klauselsatz.
Abschließend schreibt es den in der DFG-Syntax gesetzten Näherungssatz in eine Datei.

Wenn weder im Ordner noch Outfile sind gegeben, dfg2dfg Liest von der Standardeingabe und schreibt darauf
Standardausgabe. Wenn ein Dateiname angegeben wird, liest es aus dieser Datei und schreibt die Ausgabe
zur Standardausgabe. Wenn mehr als ein Dateiname angegeben wird, dfg2dfg liest sich von Anfang an
Datei und schreibt in die zweite.

Die Näherungen werden im separaten Dokument technisch ausführlich beschrieben dfg2dfg.ps
in der SPASS-Distribution enthalten.

OPTIONAL

dfg2dfg verfügt über vier verschiedene Befehlszeilenoptionen, die kombiniert werden können.

-Horn
Diese Option ermöglicht die Umwandlung von Nicht-Horn-Sätzen in Horn-Sätze. Jede
Nicht-Horn-Satz mit n positive Literale werden umgewandelt in n Hornsätze, wobei die
i-te Klausel enthält die i-tes positives Literal und alle negativen Literale des Nicht-
Hornklausel. Siehe auch Abschnitt 3 des Papiers.

-monadisch[=n]
Mit dieser Option werden Atome mit nicht-monadischen Prädikatssymbolen in monadische umgewandelt
Atome. Wenn n weggelassen wird oder n=1 Es wird eine Termkodierung angewendet, also alles nicht-monadisch
Prädikate werden auf die Termebene verschoben. Mit n=2 Es wird eine Projektion angewendet. Alle nicht-
monadische Atome werden durch ihre monadischen Argumentprojektionen ersetzt. Siehe Abschnitt 4.1
Weitere Einzelheiten finden Sie in Abschnitt 4.2 des Dokuments.

-linear
Diese Näherung transformiert eine Klausel mit monadischen Literalen und nichtlinearen Variablen
Vorkommen in aufeinanderfolgenden Atomen, in einen neuen Satz mit möglicherweise mehr Negativität
Literale, die im Nachfolger keine nichtlinearen Variablen enthalten. Siehe Sektion
Einzelheiten finden Sie auf Seite 5 des Papiers.

-shallow[=n]
Diese Transformation versucht, die Tiefe der Begriffe in positiven Literalen zu reduzieren. Der
Die Transformation wird nur auf Hornsätze mit monadischen Literalen angewendet. Wenn n wurde weggelassen
or n=1 wird eine strikte Transformation angewendet, die jedoch äquivalenzerhaltend ist.
Aussichten für n=2 einige Vorbedingungen werden entfernt. Dadurch kann die Transformation angewendet werden
häufiger, aber die Transformation ist nicht mehr gleichwertig. Für n=3
noch mehr Voraussetzungen werden entfernt. Schauen Sie sich Abschnitt 6 an.n des Papiers für die
Einzelheiten zur Befehlszeilenoption -monadisch=n.

Verwenden Sie dfg2dfg online über die Dienste von onworks.net