Este es el comando dfg2dfg que se puede ejecutar en el proveedor de alojamiento gratuito de OnWorks utilizando una de nuestras múltiples estaciones de trabajo en línea gratuitas, como Ubuntu Online, Fedora Online, emulador en línea de Windows o emulador en línea de MAC OS.
PROGRAMA:
NOMBRE
dfg2dfg - calcular aproximaciones de problemas
SINOPSIS
dfg2dfg [-cuerno] [-monádico] [-lineal] [-superficial] [en archivo] [archivar]
DESCRIPCIÓN
dfg2dfg es un programa que lee cláusulas de un archivo de entrada en sintaxis DFG. Entonces
calcula una aproximación del conjunto de cláusulas en función de las opciones de la línea de comandos.
Finalmente, escribe la cláusula aproximada establecida en sintaxis DFG en un archivo.
Si ninguno en archivo ni archivar son dados, dfg2dfg lee desde la entrada estándar y escribe en
salida estándar. Si se da un nombre de archivo, lee de ese archivo y escribe la salida
a salida estándar. Si se proporciona más de un nombre de archivo, dfg2dfg lee desde el primero
archivo y escribe en el segundo.
Las aproximaciones se describen en detalle técnico en el documento separado. dfg2dfg.ps
incluido en la distribución SPASS.
CAMPUS
dfg2dfg tiene cuatro opciones de línea de comando diferentes que se pueden combinar.
-cuerno
Esta opción permite la transformación de cláusulas sin cuerno en cláusulas con cuerno. Cada
cláusula sin cuerno con n literales positivos se transforma en n cláusulas de cuerno, donde el
i-th cláusula contiene el i-th literal positivo y todos los literales negativos del no-
cláusula de cuerno. Consulte también la sección 3 del documento.
-monádico [= n]
Con esta opción, los átomos con símbolos predicados no monádicos se transforman en monádicos.
átomos. Si n se omite o n= 1 se aplica un término de codificación, es decir, todos los no monádicos
los predicados se mueven al nivel del término. Con n= 2 se aplica una proyección. Todos los no
los átomos monádicos son reemplazados por sus proyecciones de argumentos monádicos. Ver sección 4.1.
sección 4.2 del documento para obtener más detalles.
-lineal
Esta aproximación transforma una cláusula con literales monádicos y variable no lineal
apariciones en átomos sucesivos, en una nueva cláusula con posiblemente más negativos
literales, que no contienen variables no lineales en el sucesivo. Mira la sección
5 del documento para obtener más detalles.
-shallow [= n]
Esta transformación intenta reducir la profundidad de los términos en literales positivos. los
La transformación se aplica a cláusulas de cuerno con literales monádicos únicamente. Si n se omite
or n= 1 se aplica una transformación estricta, es decir, preservando la equivalencia.
n= 2 se eliminan algunas condiciones previas. Esto permite aplicar la transformación.
más a menudo, pero la transformación ya no conserva la equivalencia. Para n=3
se eliminan aún más condiciones previas. Eche un vistazo a la sección 6.n del papel para el
detalles de la opción de línea de comando -monádico = n.
Utilice dfg2dfg en línea utilizando los servicios de onworks.net