Este es el comando prover9 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
prover9 - prover del teorema de resolución / paramodulación
SINOPSIS
prover9 [opciones] fichero de entrada > archivo de salida
prover9 [opciones] -f fichero de entrada > archivo de salida
DESCRIPCIÓN
Esta página de manual documenta brevemente la prover9 mando.
prover9 es un demostrador automatizado de teoremas para lógica de primer orden y ecuaciones. Es un
sucesor del nutria(1) probador. prover9 utiliza las técnicas de inferencia de ordenadas
resolución y paramodulación con selección literal.
OPCIONES
Un resumen de las opciones se incluye a continuación.
-h Vea una lista de opciones de la línea de comandos.
-x Habilita un modo automático mejorado experimental. Para más información consulte el
prover9 manual.
-p Entre paréntesis por completo la salida.
-t n Restrinja la búsqueda para que dure aproximadamente n segundos. Para sistemas similares a UNIX, el `usuario
Se usa el tiempo de la CPU.
-f presentar
Toma información de presentar en lugar de la entrada estándar.
Utilice prover9 en línea utilizando los servicios de onworks.net
