dfg2dfg - Online nel cloud

PROGRAMMA:

NOME

dfg2dfg - calcola approssimazioni di problemi

SINOSSI

dfg2dfg [-corno] [-monadica] [-lineare] [-superficiale] [infilare] [file di uscita]

DESCRIZIONE

dfg2dfg è un programma che legge le clausole da un file di input nella sintassi DFG. Allora
calcola un'approssimazione del set di clausole in base alle opzioni della riga di comando.
Infine scrive la clausola approssimata impostata nella sintassi DFG in un file.

Se nessuno dei due infilare né file di uscita sono dati, dfg2dfg legge dallo standard input e scrive su
uscita standard. Se viene dato un nome di file, legge da quel file e scrive l'output
all'uscita standard. Se viene fornito più di un nome di file, dfg2dfg si legge dal primo
file e scrive nel secondo.

Le approssimazioni sono descritte in dettaglio tecnico nel documento separato dfg2dfg.ps
inclusi nella distribuzione SPASS.

VERSIONI

dfg2dfg ha quattro diverse opzioni della riga di comando che possono essere combinate.

-corno
Questa opzione consente la trasformazione delle clausole non di corno in clausole di corno. Ogni
clausola non corno con n i letterali positivi si trasformano in n clausole di corno, dove la
i-esima clausola contiene la i-esimo letterale positivo e tutti i letterali negativi del non-
clausola di corno. Vedi anche la sezione 3 del documento.

-monadico[=n]
Con questa opzione gli atomi con simboli predicati non monadici vengono trasformati in monadici
atomi. Se n è omesso o n=1 viene applicata una codifica a termine, ovvero tutto non monadico
i predicati vengono spostati al livello dei termini. Insieme a n=2 viene applicata una proiezione. Tutti non-
gli atomi monadici sono sostituiti dalle loro proiezioni di argomenti monadici. Vedere la sezione 4.1
sezione 4.2 del documento per maggiori dettagli.

-lineare
Questa approssimazione trasforma una clausola con letterali monadici e variabile non lineare
occorrenze in atomi succedenti, in una nuova clausola con possibilmente più negativi
letterali, che non contengono variabili non lineari nel succedente. Vedi sezione
5 della carta per i dettagli.

-superficiale[=n]
Questa trasformazione cerca di ridurre la profondità dei termini in letterali positivi. Il
la trasformazione viene applicata solo alle clausole di corno con letterali monadici. Se n è omesso
or n=1 viene applicata una trasformazione rigorosa, che tuttavia preserva l'equivalenza.
Nel n=2 vengono rimosse alcune precondizioni. Ciò consente di applicare la trasformazione
più spesso, ma la trasformazione non è più la preservazione dell'equivalenza. Per n=3
vengono rimosse ancora più precondizioni. Dai un'occhiata alla sezione 6.n della carta per il
dettagli dell'opzione della riga di comando -monadica=n.

Usa dfg2dfg online utilizzando i servizi onworks.net