Este é o comando dfg2dfg que pode ser executado no provedor de hospedagem gratuita OnWorks usando uma de nossas várias estações de trabalho online gratuitas, como Ubuntu Online, Fedora Online, emulador online do Windows ou emulador online do MAC OS
PROGRAMA:
NOME
dfg2dfg - calcular aproximações de problemas
SINOPSE
dfg2dfg [-horn] [-monadic] [-linear] [-shallow] [no arquivo] [arquivo de saída]
DESCRIÇÃO
dfg2dfg é um programa que lê cláusulas de um arquivo de entrada na sintaxe DFG. Isso então
calcula uma aproximação da cláusula definida, dependendo das opções da linha de comando.
Finalmente, ele grava a cláusula aproximada definida na sintaxe DFG em um arquivo.
Se nenhum no arquivo nem arquivo de saída são dados, dfg2dfg lê a entrada padrão e escreve para
saída padrão. Se um nome de arquivo é fornecido, ele lê esse arquivo e grava a saída
para a saída padrão. Se mais de um nome de arquivo for fornecido, dfg2dfg lê desde o primeiro
arquivo e grava no segundo.
As aproximações são descritas em detalhes técnicos no artigo separado dfg2dfg.ps
incluído na distribuição do SPASS.
OPÇÕES
dfg2dfg tem quatro opções de linha de comando diferentes que podem ser combinadas.
-chifre
Esta opção permite a transformação de cláusulas que não sejam de trompa em cláusulas de trompa. Cada
cláusula não-chifre com n literais positivos são transformados em n cláusulas de trompa, onde o
i-th cláusula contém o i-ésimo literal positivo e todos os literais negativos do não
cláusula do chifre. Consulte também a seção 3 do artigo.
-monadic [= n]
Com esta opção, átomos com símbolos de predicados não monádicos são transformados em símbolos monádicos
átomos. Se n é omitido ou n= 1 um termo codificação é aplicado, ou seja, todos não monádicos
os predicados são movidos para o nível do termo. Com n= 2 uma projeção é aplicada. Todos não
átomos monádicos são substituídos por suas projeções de argumentos monádicos. Consulte a seção 4.1
seção 4.2 do artigo para mais detalhes.
-linear
Esta aproximação transforma uma cláusula com literais monádicos e variável não linear
ocorrências em átomos sucessivos, em uma nova cláusula com possivelmente mais
literais, que não contém nenhuma variável não linear no sucessor. Veja a seção
5 do papel para detalhes.
-shallow [= n]
Essa transformação tenta reduzir a profundidade dos termos em literais positivos. o
a transformação é aplicada a cláusulas de chifre apenas com literais monádicos. Se n é omitido
or n= 1 uma transformação estrita é aplicada, isto é, preservação da equivalência, no entanto.
Escolha n= 2 algumas pré-condições são removidas. Isso permite que a transformação seja aplicada
com mais frequência, mas a transformação não preserva mais a equivalência. Para n=3
ainda mais pré-condições são removidas. Dê uma olhada na seção 6.n do papel para o
detalhes da opção de linha de comando -monadic = n.
Use dfg2dfg online usando serviços onworks.net
