Jest to polecenie dfg2dfg, które można uruchomić w bezpłatnym dostawcy hostingu OnWorks przy użyciu jednej z naszych wielu bezpłatnych stacji roboczych online, takich jak Ubuntu Online, Fedora Online, emulator online systemu Windows lub emulator online systemu MAC OS
PROGRAM:
IMIĘ
dfg2dfg - oblicza przybliżenia problemów
STRESZCZENIE
dfg2dfg [-róg] [-monadyczny] [-liniowy] [-płytki] [w pliku] [plik wyjściowy]
OPIS
dfg2dfg to program czytający klauzule z pliku wejściowego w składni DFG. to wtedy
oblicza przybliżenie zestawu klauzul w zależności od opcji wiersza poleceń.
Na koniec zapisuje do pliku przybliżoną klauzulę ustawioną w składni DFG.
Jeśli nie w pliku ani plik wyjściowy są podane, dfg2dfg czyta ze standardowego wejścia i zapisuje na nim
standardowe wyjście. Jeśli podana jest jedna nazwa pliku, odczytuje z tego pliku i zapisuje wynik
na standardowe wyjście. Jeżeli podano więcej niż jedną nazwę pliku, dfg2dfg czyta od pierwszego
plik i zapisuje do drugiego.
Przybliżenia opisano szczegółowo pod względem technicznym w osobnym artykule dfg2dfg.ps
zawarte w dystrybucji SPAS.
OPCJE
dfg2dfg ma cztery różne opcje wiersza poleceń, które można łączyć.
-róg
Opcja ta umożliwia przekształcenie zdań innych niż rogowe w zdania rogowe. Każdy
Klauzula bez rogu z n Literały dodatnie są przekształcane w n klauzule rogowe, gdzie
i-ta klauzula zawiera i-ty literał dodatni i wszystkie literały ujemne nie-
klauzula rogowa. Zobacz także sekcję 3 artykułu.
-monadyczny[=n]
Dzięki tej opcji atomy z niemonadycznych symboli predykatów są przekształcane w monadyczne
atomy. Gdyby n jest pominięty lub n=1 stosowane jest kodowanie terminów, tj. wszystkie niemonadyczne
predykaty przenoszone są na poziom terminów. Z n=2 zastosowano projekcję. Wszystkie nie-
atomy monadyczne są zastępowane przez ich monadyczne projekcje argumentów. Patrz sekcja 4.1
więcej szczegółów znajdziesz w sekcji 4.2 artykułu.
-liniowy
To przybliżenie przekształca klauzulę za pomocą literałów monadycznych i zmiennej nieliniowej
wystąpienia w kolejnych atomach, w nowe zdanie z możliwie większą liczbą negatywów
literały, które nie zawierają w następcy żadnych zmiennych nieliniowych. Patrz sekcja
5 artykułu, aby uzyskać szczegółowe informacje.
-płytki[=n]
Ta transformacja próbuje zmniejszyć głębokość terminów w literałach dodatnich. The
transformacja jest stosowana do klauzul rogu zawierających tylko literały monadyczne. Jeśli n jest pominięty
or n=1 stosowana jest ścisła transformacja, czyli z zachowaniem równoważności.
W razie zamówieenia projektu n=2 niektóre warunki wstępne zostały usunięte. Pozwala to na zastosowanie transformacji
częściej, ale transformacja nie zachowuje już równoważności. Dla n=3
usunięto jeszcze więcej warunków wstępnych. Spójrz na sekcję 6.n papieru dla
szczegóły opcji wiersza poleceń -monadyczny=rzecz.
Użyj dfg2dfg online, korzystając z usług onworks.net
