SPASS - Online en la nube

PROGRAMA:

NOMBRE

SPASS: demostrador automatizado de teoremas para lógica completa de primer orden con igualdad

SINOPSIS

ESPACIO [opciones] [fichero de entrada]

DESCRIPCIÓN

SPASS es un demostrador de teoremas automatizado para lógica de primer orden ordenada completa con igualdad que
extiende la superposición por géneros y una regla de división para el análisis de casos. SPASS también puede ser
utilizado como demostrador de teoremas de lógica modal y lógica descriptiva.

OPCIONES

Las opciones de la línea de comando en SPASS se implementan mediante modificaciones a la línea de comando GNU
paquete de opciones para C.Sólo dar la opción establece su valor en 1 y significa habilitar el
opción. Para deshabilitar una opción, el valor debe establecerse en 0 declarando:Opción= 0.
Actualmente, SPASS admite las siguientes opciones:

-auto
Habilita / deshabilita el modo automático donde SPASS se configura automáticamente. los
reglas de inferencia / reducción, la tecnología de clasificación, el orden y la precedencia, así como
la estrategia de división y selección está establecida. En el modo automático, SPASS está completo. Mezclar
el modo automático con opciones definidas por el usuario puede destruir la integridad. El valor predeterminado es 1.

-Estándar
Habilita / deshabilita la entrada en SPASS a través de stdin. Se ignora el argumento del archivo. El valor predeterminado es 0.

-Interactivo
Activa / desactiva el modo interactivo. Primero, a SPASS se le da un conjunto de axiomas y luego
el probador acepta tareas de prueba posteriores. El valor predeterminado es 0.

-Flotador
Activa / desactiva el modo de traducción CNF de SPASS. Si la opción está configurada, solo SPASS
realiza una traducción de forma normal de cláusula. Si no se proporciona ningún argumento de archivo de salida SPASS
imprime el CNF en stdout. El valor predeterminado es 0.

-LLAMADA DE SOCORRO
Habilita / deshabilita el conjunto de estrategias de soporte. El valor predeterminado es 0.

-Splits =n
Establece el número de posibles aplicaciones de división para n. Si n= -1 entonces el número de
las divisiones no están limitadas. El valor predeterminado es 0.

-Memoria =n
Establece la cantidad de memoria disponible para SPASS para la búsqueda de prueba en n bytes. La
la memoria necesaria para iniciar SPASS no se puede restringir. El valor predeterminado es -1, lo que significa que
Las asignaciones de memoria solo están restringidas por la memoria disponible.

-TimeLimit =n
Establece un límite de tiempo para la búsqueda de pruebas para n segundos. El valor predeterminado es -1, lo que significa que SPASS
puede correr para siempre. El límite de tiempo se consulta cuando SPASS selecciona una nueva cláusula para
inferencias. Si un solo paso de inferencia provoca una explosión en el número de generados
cláusulas, por lo tanto, puede suceder que se exceda significativamente un límite de tiempo determinado.

-DocSST
Habilita / deshabilita la salida de documentación para escritura suave estática. La teoría de género utilizada como
así como se imprime el intento de prueba (fallido) para la restricción de clasificación. El valor predeterminado es 0.

-Documento
Activa / desactiva la documentación de prueba. Si SPASS encuentra una prueba, finalmente se imprime.
Si SPASS encuentra una saturación, finalmente se imprime el conjunto saturado de cláusulas.
Habilitar la documentación de prueba puede disminuir significativamente el rendimiento de SPASS, porque
el probador debe almacenar cláusulas que de otro modo se pueden desechar. El valor predeterminado es 0.

-Documento dividido
Establece la documentación de los pasos de retroceso divididos. Si se establece en 1, la corriente
Se imprime el nivel de retroceso. Si se establece en 2, también se imprime en caso de una división
dar marcha atrás a los clauese retrocedidos. El valor predeterminado es 0.

-Bucles
Establece el número máximo de iteraciones de mainloop para SPASS. El valor predeterminado es -1.

-Psub
Habilita / deshabilita la impresión de cláusulas subsumidas. El valor predeterminado es 0.

-PRew
Habilita / deshabilita la impresión de aplicaciones de reescritura simple. El valor predeterminado es 0.

-PCon
Activa / desactiva la impresión de aplicaciones de condensación. El valor predeterminado es 0.

-PTaut
Habilita / deshabilita la impresión de aplicaciones de eliminación de tautología. El valor predeterminado es 0.

-PObv
Activa / desactiva la impresión de aplicaciones de reducción obvias. El valor predeterminado es 0.

-PSSi
Habilita / deshabilita la impresión de aplicaciones de simplificación de clasificación. El valor predeterminado es 0.

-PSST
Habilita / deshabilita la impresión de aplicaciones estáticas de escritura suave. Todas las cláusulas eliminadas son
impreso. El valor predeterminado es 0.

-PMRR
Habilita / deshabilita la impresión de aplicaciones de resolución de reemplazo coincidentes. El valor predeterminado es
0.

-PUnc
Habilita / deshabilita la impresión de aplicaciones de conflicto de unidades. El valor predeterminado es 0.

-PAED
Habilita / deshabilita la impresión de cláusulas donde se han eliminado ecuaciones redundantes
(eliminación de la ecuación de asignación).

-PDer
Habilita / deshabilita la impresión de cláusulas derivadas de inferencias. El valor predeterminado es 0.

-PDado
Habilita / deshabilita la impresión de la cláusula dada, seleccionada para realizar inferencias.
El valor predeterminado es 0.

-Plantillas
Activa / desactiva la impresión de etiquetas. Si se establece -DocProof y no hay etiquetas para
Las fórmulas son proporcionadas por la entrada, SPASS genera etiquetas genéricas que luego se
impreso habilitando esta opción. El valor predeterminado es 0.

-PMantenido
Habilita / deshabilita la impresión de cláusulas guardadas. Estas son cláusulas generadas por inferencias
(retroceso) que no son redundantes. Cláusulas derivadas durante la entrada
la reducción / saturación no se imprimen. El valor predeterminado es 0.

-PProblema
Habilita / deshabilita la impresión del conjunto de cláusulas de entrada. El valor predeterminado es 1.

-PemptyClause
Habilita / deshabilita la impresión de cláusulas vacías derivadas. El valor predeterminado es 0.

-PEstadística
Habilita / deshabilita la impresión de estadísticas finales sobre cláusulas derivadas / retrocedidas / mantenidas,
fraccionamientos realizados, tiempo usado y espacio usado. El valor predeterminado es 1.

-FPModelo
Habilita / deshabilita la salida de un modelo eventualmente encontrado a un archivo. Si se establece en 1, todos
Se imprimen las cláusulas del conjunto final. Si se establece en 2, solo las cláusulas potencialmente productivas
se imprimen, que son cláusulas sin literal negativo seleccionado y un máximo positivo
uno. Si es el nombre del problema de entrada y el eventualmente generado
el conjunto está saturado, la saturación se imprime en el archivo .modelo, para
de lo contrario a .cláusulas. El último caso puede, por ejemplo, ser causado por un tiempo
límite. El valor predeterminado es 0.

-FPDFGPrueba
Habilita / deshabilita la salida de una prueba encontrada finalmente en un archivo. Usando esta opción
requiere establecer la opción -DocProof. Si es el nombre de la entrada
problema en el que se imprime la prueba .prf. El valor predeterminado es 0.

-PBanderas
Habilita / deshabilita la salida de todos los valores de la bandera. Los ajustes de la bandera se imprimen en la
final de una ejecución de SPASS en forma de una sección de entrada de sintaxis DFG. El valor predeterminado es 0.

-POptSkolem
Habilita / deshabilita la salida de aplicaciones optimizadas de Skolemización. El valor predeterminado es 0.

-PStrSkolem
Habilita / deshabilita la salida de aplicaciones fuertes de Skolemización. El valor predeterminado es 0.

-PBDC
Habilita / deshabilita la salida de cláusulas eliminadas debido a restricciones vinculadas. Defecto
es 0.

-PBInc
Habilita / deshabilita la salida de cambios de restricción vinculados. El valor predeterminado es 0.

-PAplicarDefs
Habilita / deshabilita la impresión de expansiones de definiciones de átomos. El valor predeterminado es 0.

-Seleccione
Establece la estrategia de selección para SPASS. Si se establece en 0, no hay selección de literales negativos
está hecho. Si se establece en cualquier otro valor, como máximo un literal negativo en una cláusula es
seleccionado. Si se establece en 1 literal negativo en cláusulas con más de un literal máximo
están seleccionados. O un literal negativo con un predicado de la lista de selección (ver
a continuación) o si no hay tal literal negativo disponible, se elige un literal negativo con
se elige el peso máximo. Si se establece en 2, siempre se seleccionan los literales negativos. De nuevo,
ya sea un literal negativo con un predicado de la lista de selección (ver más abajo) es
elegido o si no hay tal literal negativo disponible, un literal negativo con máxima
se elige el peso. El último caso da como resultado un comportamiento similar a una hiperresolución ordenada
de resolución ordenada. Si se establece en 3 cualquier literal negativo con un predicado especificado por
se selecciona la lista de selección (ver más abajo). El valor predeterminado es 1.

-R Entrada
Habilita / deshabilita la reducción del conjunto de cláusulas inicial. El valor predeterminado es 1.

-Ordena
Determina los literales monádicos que construyeron la restricción de clasificación para la cláusula inicial.
colocar. Si se establece en 0, no se crea ninguna restricción de clasificación. Si se establece en 1, todo monádico negativo
los literales con una variable como argumento forman la restricción de clasificación. Si se establece en 2, todos
los literales monádicos negativos forman la restricción de clasificación. Establecer -Sorts en 2 puede dañar
completitud, ya que las restricciones de ordenación están sujetas a la estrategia básica y a
escritura suave. El valor predeterminado es 1.

-Entrada satelital
Activa / desactiva la saturación de entrada. La saturación es incompleta pero se garantiza que
Terminar. El valor predeterminado es 0.

-WDRatio
Establece la relación entre las cláusulas dadas seleccionadas por peso o profundidad en la búsqueda
espacio. El peso es la suma de todos los pesos de los símbolos determinados por -FuncWeight y
-Opciones de VarWeight. La profundidad de todas las cláusulas iniciales es 0 y las cláusulas generadas por
las inferencias obtienen la profundidad máxima de una cláusula principal más 1. El valor predeterminado es 5, lo que significa
que 4 cláusulas se seleccionan por peso y la quinta cláusula se selecciona por profundidad.

-PrefCon
Establece la razón para calcular el peso de las cláusulas de conjetura y, por lo tanto, permite
prefiero esos. El valor predeterminado es 0, lo que significa que el cálculo del peso para las cláusulas de conjetura
No se cambia.

-FullRed
Activa / desactiva la reducción completa. Si se establece en 0, solo el conjunto de cláusulas resueltas es
completamente inter-reducido. Si se establece en 1, todas las cláusulas de retención actualmente (trabajadas y
utilizables) están completamente inter-reducidos. El valor predeterminado es 1.

-FuncPeso
Establece el peso de los símbolos de función / predicado. El peso de las cláusulas es la suma de todos
pesos de símbolo. Este peso se considera para la selección de la cláusula dada.
El valor predeterminado es 1.

-VarPeso
Establece el peso de los símbolos de variable (consulte -FuncWeight). El valor predeterminado es 1.

-VarPref
Habilita / deshabilita la preferencia por cláusulas con muchas variables. Mientras que las cláusulas son
seleccionado por peso, si esta opción está configurada y dos cláusulas tienen el mismo peso, la
Se prefiere una cláusula con ocurrencias más variables. El valor predeterminado es 0.

-Modo enlazado
Selecciona el modo de restricciones limitadas. El modo 0 significa que no hay restricción, si se establece en 1 todos
las cláusulas recién generadas están restringidas por peso (consulte -BoundStart) y si se establecen en 2
las cláusulas están restringidas por la profundidad. El valor predeterminado es 0.

-BoundStart
La restricción de inicio del modo enlazado seleccionado. Por ejemplo, si el modo enlazado es 1 y
inicio enlazado establecido en 5, todas las cláusulas con un peso superior a 5 se eliminan hasta que el
el conjunto está saturado. Esto provoca un aumento del valor límite utilizado que se determina
por el aumento mínimo que guarda una cláusula antes eliminada. El valor predeterminado es -1, lo que significa que no hay límite
restricción.

-Bucles enlazados
El número de bucles que aplican las restricciones de acciones / límite creciente. Si el numero
de bucles se superan todas las restricciones de límite se cancelan. El valor predeterminado es 1.

-AplicarDefs
Establece el número máximo de aplicaciones de definiciones de átomos para ingresar fórmulas.
El valor predeterminado es 0, lo que significa que no hay aplicaciones en absoluto.

-Ordenar
Establece el término ordenamiento. Si se selecciona 0, entonces se selecciona KBO, si se selecciona 1, se selecciona el RPOS. Defecto
es 0.

-CNFQuantExch
Si se establece, los términos de Skolem no constantes en la forma clausal de la conjetura se reemplazan
por constantes. Se configurará automáticamente para la traducción funcional optimizada de
fórmulas lógicas modales o descriptivas. El valor predeterminado es 0.

-CNFOptSkolem
Habilita / deshabilita la Skolemización optimizada. El valor predeterminado es 1.

-CNFStrSkolem
Habilita / deshabilita la Skolemización fuerte. El valor predeterminado es 1.

-CNFProofSteps
Establece el número máximo de pasos de prueba en un intento de prueba de Skolemización optimizado.
El valor predeterminado es 100.

-CNFSub
Habilita / deshabilita la subsunción de las cláusulas generadas por el procedimiento CNF. Defecto
es 1.

-CNFCon
Habilita / deshabilita la condensación en las cláusulas generadas por el procedimiento CNF. El valor predeterminado es
1.

-CNFRTiempoRojo
Establece la cantidad total de tiempo en segundos que se dedicará a la reducción durante el CNF
transformación. Las reducciones afectadas son Skolemization optimizado, condensación y
subsunción. El valor predeterminado es -1, lo que significa que el tiempo de reducción no está limitado en absoluto.

-CNFRenombrar
Habilita / deshabilita el cambio de nombre de fórmulas. Si se establece en 1, se habilita el cambio de nombre optimizado que
minimiza el número de cláusulas eventualmente generadas. Si se establece en 2, el cambio de nombre complejo es
habilitado que introduce un nuevo predicado Skolem para cada fórmula compleja, es decir, cualquier
fórmula que no es literal. Si se establece en 3, el cambio de nombre de cuantificación está habilitado
introduce un nuevo predicado de Skolem para cada subfórmula que comienza con un cuantificador.
El valor predeterminado es 1.

-CNFRenMatch
Si se establece, las subformulas variantes de cambio de nombre se reemplazan por el mismo literal de Skolem. Defecto
es 1.

-CNFPRenombrar
Activa / desactiva la impresión de aplicaciones de cambio de nombre de fórmulas. El valor predeterminado es 0.

-CNFFEqR
Habilita / deshabilita ciertas técnicas de reducción de igualdad en el nivel de fórmula. Defecto
es 1.

-IEmS
Habilita / deshabilita la regla de inferencia Orden vacío. El valor predeterminado es 0.

-ISOR
Habilita / deshabilita la resolución de clasificación de la regla de inferencia. El valor predeterminado es 0.

-IEqR
Habilita / deshabilita la resolución de igualdad de la regla de inferencia. El valor predeterminado es 0.

-IERR
Habilita / deshabilita la resolución de reflexividad de la regla de inferencia. El valor predeterminado es 0.

-IEqF
Habilita / deshabilita la regla de inferencia Equality Factoring. El valor predeterminado es 0.

-IMPm
Habilita / deshabilita la regla de inferencia Fusionando paramodulación. El valor predeterminado es 0.

-ISpR
Habilita / deshabilita la regla de inferencia Superposición derecha. El valor predeterminado es 0.

-PIOm
Habilita / deshabilita la regla de inferencia Paramodulación ordenada. El valor predeterminado es 0.

-ISPm
Habilita / deshabilita la regla de inferencia paramodulación estándar. El valor predeterminado es 0.

-ISpL
Habilita / deshabilita la regla de inferencia Superposición a la izquierda. El valor predeterminado es 0.

-IORe
Habilita / deshabilita la resolución ordenada de la regla de inferencia. Si se establece en 1, ordenado
La resolución está habilitada pero no se generan inferencias de resolución con ecuaciones. Si
establecido en 2, las ecuaciones también se consideran para los pasos de resolución ordenada. El valor predeterminado es
0.

-ISRe
Habilita / deshabilita la resolución estándar de la regla de inferencia. Si se establece en 1, estándar
La resolución está habilitada pero no se generan inferencias de resolución con ecuaciones. Si
establecido en 2, las ecuaciones también se consideran para los pasos de Resolución estándar. El valor predeterminado es
0.

-Soy tímido
Habilita / deshabilita la regla de inferencia Hiperresolución estándar. El valor predeterminado es 0.

-IOHy
Habilita / deshabilita la regla de inferencia Hiperesolución ordenada. El valor predeterminado es 0.

-IURR
Habilita / deshabilita la resolución resultante de la unidad de la regla de inferencia. El valor predeterminado es 0.

-IOFc
Habilita / deshabilita la regla de inferencia Factorización ordenada. Si se establece en 1, factorización ordenada
está habilitado, pero solo se generan inferencias de factorización con literales positivos. Si está configurado
a 2, los literales negativos también se consideran para las inferencias. El valor predeterminado es 0.

-ISFc
Habilita / deshabilita la regla de inferencia Factorización estándar. El valor predeterminado es 0.

-IUnR
Habilita / deshabilita la resolución de la unidad de la regla de inferencia. El valor predeterminado es 0.

-IBUR
Habilita / deshabilita la regla de inferencia Resolución de unidad de profundidad limitada. El valor predeterminado es 0.

-IDEF
Habilita / deshabilita la regla de inferencia Aplicar definiciones. Actualmente no es compatible.
El valor predeterminado es 0.

-RFRew
Habilita / deshabilita la regla de reducción Reescritura hacia adelante. Si se establece en 1 unidad reescritura y
Se activa la reescritura no unitaria basada en una prueba de subsunción. Si se establece en 2 además
a reescritura de unidades y no unidades se activa la reescritura contextual local. Si se establece en 3
Además de la reescritura de unidades y no unidades, la reescritura contextual es
activado. La reescritura contextual subtérmino incluye la reescritura contextual local. Si está configurado
a 4 además de las reglas de reescritura de 3, la reescritura contextual del subtermo también prueba
para la eliminación literal negativa. El valor predeterminado es 0.

-RBRew
Habilita / deshabilita la regla de reducción Reescritura hacia atrás. Mismos valores y significado que
para flag -RFRew pero usado en dirección hacia atrás. El valor predeterminado es 0.

-RFMRR
Habilita / deshabilita la regla de reducción de la resolución de reemplazo de correspondencia directa. Defecto
es 0.

-RBMRRR
Habilita / deshabilita la regla de reducción Resolución de reemplazo de coincidencia hacia atrás. Defecto
es 0.

-RObv
Habilita / deshabilita la regla de reducción Obvious Reduction. El valor predeterminado es 0.

-RUNC
Habilita / deshabilita la regla de reducción Unit Conflict. El valor predeterminado es 0.

-RTer
Habilita / deshabilita el terminador estableciendo el número máximo de cláusulas no unitarias en
ser utilizado durante la búsqueda. El valor predeterminado es 0.

-RTaut
Habilita / deshabilita la eliminación de tautología de la regla de reducción. Si se establece en 1, solo sintáctico
se detectan y eliminan tautologías. Si se establece en 2, además tautologías semánticas
son removidos. El valor predeterminado es 0.

-RSST
Habilita / deshabilita la regla de reducción Static Soft Typing. El valor predeterminado es 0.

-RSSi
Habilita / deshabilita la regla de reducción Clasificar Simplificación. El valor predeterminado es 0.

-RFSub
Habilita / deshabilita la regla de reducción Eliminación de subsunción anticipada. El valor predeterminado es 0.

-RBSub
Habilita / deshabilita la regla de reducción Supresión de subsunción hacia atrás. El valor predeterminado es 0.

-RAED
Habilita / deshabilita la eliminación de la ecuación de asignación de la regla de reducción. Esta regla elimina
ocurrencias particulares de ecuaciones de cláusulas. Si se establece en 1, la reducción es
garantizado para ser sólido. Si se establece en 2, la reducción solo es sólida si existe algún potencial
El modelo del problema considerado tiene un dominio no trivial. El valor predeterminado es 0.

-RCon
Habilita / deshabilita la regla de reducción Condensación. El valor predeterminado es 0.

-TDfg2OtterOptions
Habilita / deshabilita la inclusión de un encabezado de opciones de Otter. Esta opción solo se aplica a
dfg2otter. Si se establece en 1, incluye una configuración que hace que Otter esté casi completo. Si está configurado
a 2 activa el modo automático y si se establece en 3 activa el modo auto2. El valor predeterminado es
0.

-EML
Una bandera EML especial para fórmulas de lógica modal o lógica descriptiva. Nunca necesita ser
establecer explícitamente. Se establece durante el análisis.

-EMLAuto
Destinado al modo autónomo EML, aún no funcional. El valor predeterminado es 0.

-EMLTraducción
Determina el método de traducción utilizado para la lógica modal o las fórmulas de lógica descriptiva.
Si se establece en 0, el método de traducción relacional estándar (que está determinado por el
semántica habitual de Kripke). Si se establece en 1, el método de traducción funcional es
usó. Si se establece en 2, se utiliza el método de traducción funcional optimizado. Si se establece en 3,
Se utiliza el método de traducción semifuncional. Una variación de lo optimizado
Se utiliza el método de traducción funcional cuando se especifican las siguientes configuraciones:
-EMLTranslation = 2 -EMLFuncNary = 1. La traducción será en términos de n-ary
predicados en lugar de predicados y caminos unarios. En la implementación actual el
El método estándar de traducción relacional es el más general. Se aplican algunas restricciones al
otros metodos. El método de traducción funcional y la traducción semifuncional
Los métodos están disponibles solo para la lógica multimodal básica. K(m) posiblemente con serial
(total) modalidades (-EMLTheory = 1), más nominales (declaraciones ABox), terminológicas
axiomas y axiomas generales de inclusión y equivalencia. El funcional optimizado
Los métodos de traducción se implementan solo para K(m), posiblemente con modalidades seriadas.
El valor predeterminado es 0.

-EML2Rel
Si se establece, las fórmulas proposicionales / de tipo booleano se convierten en fórmulas relacionales
antes de que se traduzcan a la lógica de primer orden. El valor predeterminado es 0.

-EMLTeoría
Determina qué teoría de fondo se asume. Si se establece en 0, la teoría de fondo es
vacío. Si se establece en 1, entonces la serialidad (la teoría de fondo para KD) se agrega para todos
modalidades. Si se establece en 2, entonces la reflexividad (la teoría de fondo para KT) se agrega para
todas las modalidades. Si se establece en 3, se agrega simetría (la teoría de fondo para KB)
para todas las modalidades. Si se establece en 4, entonces la transitividad (la teoría de fondo para K4) es
agregado para todas las modalidades. Si se establece en 5, entonces euclidiana (la teoría de fondo para
K5) se agrega para todas las modalidades. Si se establece en 6, entonces transitividad y euclídea
(la teoría de fondo para S4) se agrega para todas las modalidades. Si se establece en 7, entonces
Se agrega reflexividad, transitividad y euclidismo (la teoría de fondo para S5).
para todas las modalidades. El valor predeterminado es 0.

-EMLFuncNdeQ
Si se establece, las fórmulas de diamante se traducen de acuerdo con tr (dia (phi), s) = nde (s) / \ existe
x tr (phi, [sx]) (una fórmula nde / cuantificador), de lo contrario, la traducción está en
de acuerdo con tr (dia (phi), s) = existe x nde (s) / \ tr (phi, [sx]) (un cuantificador / nde
fórmula). La traducción de las fórmulas de caja se define de forma doble. Establecer esta bandera es
solo tiene sentido cuando la bandera del método de traducción funcional o semifuncional
Está establecido. El valor predeterminado es 1.

-EMLFuncNario
Si se establece, se utiliza la traducción funcional a lógica estriada. Esto significa n-ary
Se utilizan símbolos de predicado en lugar de rutas y símbolos de predicado unario. Configurando esto
La bandera solo es significativa para probar la satisfacibilidad / validez local en K.
El valor predeterminado es 0.

-EMLFFTipos
Si se establece, se utilizan ordenamientos por términos. El valor predeterminado es 0.

-EMLElimComp
Si está configurado, intente eliminar la composición relacional en los parámetros modales. El valor predeterminado es 0.

-EMLPTrans
Si se establece, se documenta la EML a la traducción lógica de primer orden. El valor predeterminado es 0.

-TPTP
Si se establece, SPASS espera un archivo de entrada en sintaxis TPTP. El valor predeterminado es 0.

-rf Si se establece, SPASS elimina el archivo de entrada antes de la terminación. El valor predeterminado es 0.

EJEMPLOS

Para ejecutar SPASS en un solo archivo sin opciones:

SPASS I

Para deshabilitar todas las salidas de SPASS excepto el resultado final:

SPASS -PGiven = 0 -PProblem = 0 I

NOTAS

También puede especificar opciones para SPASS en el problema de entrada. En la sintaxis DFG, debería
use

lista_de_configuraciones (SPASS).
{*
set_flag (DocProof, 1).
*}
fin_de_la_lista.

para configurar el indicador DocProof.

Hay tres tipos de opciones que puede configurar en la entrada:

establecer bandera( , ).
Establece un indicador en un valor. Los indicadores y valores válidos se describen en la sección OPCIONES.

set_precedence ( ).
Establece la precedencia de los símbolos enumerados. La precedencia está disminuyendo de izquierda a
derecha, es decir, el símbolo más a la izquierda tiene la mayor prioridad.

Cada entrada en la lista tiene la forma

SÍMBOLO | (SÍMBOLO, PESO [, {l, r, m}])

Puede utilizar el segundo formulario para asignar pesos a los símbolos (para KBO) o un estado (para
RPOS). El estado es @t {l} para izquierda a derecha, @t {m} para multiset o @t {r} para
De derecha a izquierda. El peso se da como un número entero.

set_DomPred ( ).
Predicado enumerado (DomPred para el predicado dominante) los símbolos se ordenan primero de acuerdo con
a su precedencia, no de acuerdo con sus listas de argumentos. Solo en caso de igual
predicados, se examinan los argumentos. Por ejemplo, si agregamos la opción

set_DomPred (P).

luego en la cláusula

-> R (f (x, y), a), P (x, a).

el átomo P (x, a) es estrictamente máxima. Predicados enumerados por el set_DomPred las opciones son
comparado según la precedencia.

set_selection ( ).
Establece la lista de selección que puede utilizar el indicador Seleccionar (ver más arriba).

set_ClauseFormulaRelation ( , secuencia de
cadenas de nombres de axiomas)).
Esta lista la establece en particular FLOTTER y habilita SPASS para una eventual
prueba para mostrar la relación entre las cláusulas utilizadas en la prueba y la entrada
fórmulas. Si se combina con la opción DocProof, entonces debe haber una entrada para cada
número de cláusula. De lo contrario, se informa de un error.

set_ClauseFormulaRelation((1,ax2),(2,ax1),(3,ax3,ax1)).

Utilice SPASS en línea utilizando los servicios de onworks.net