Demostrador Automático para la Logica de Primer Orden

2 Comments Add your own

• 1. Orlando A. Pereira  |  Enero 11, 2007 at 2:58 am

  Hola Juan.

  Saludos.
  Soy de Venezuela.
  En lo actuales momentos estoy investigando sobre el Demostrador Automático Otter3.0. Debo utilizarlo para demostrar la validez de una argumentación sin igualdad, en la versión para ambiente Window. Entiendo la lógica del Demostrador, pero sin embargo tengo dudas en la creación del archivo de entrada. ¿Qué tipo de archivo es?. ¿cómo crearlo?. Cómo hacer la ejecución del programa?

• 2. dalpo  |  Enero 11, 2007 at 11:45 am

  Hola Orlando,

  no me he bajado la última versión de Otter pero en cualquier caso no creo que su uso cambie mucho con respecto a las anteriores. Debes escribir en un archivo (de texto por ejemplo) las fórmulas de entrada de tu argumentación. Este archivo debe tener una estructura determinada, creo que la conoces, en cualquier caso te pongo un pequeño ejemplo:

  %resolucion binaria
  set(binary_res).
  %formulas a refutar
  formula_list(sos).
  all x (p(x) -> q(x))
  exists y r(y).
  all x y (p(x) | r(y))
  end_of_list.

  Una vez que hayas creado tu archivo con las formulas a refutar, guardalo con su nombre, y por ejemplo la extensión .in

  Ahora estamos en disposición de invocar al programa desde la linea de comandos. Este debe recibir tus formulas de entrada, por lo que escribiremos lo siguiente en la consola:

  otter > entrada.in

  Si queremos redireccionar la salida a un archivo escribimos:

  otter > entrada.in < salida.out

  También existe una versión de Otter con interfaz gráfica (ventanas, botones). Se llama XOtter, pero creo que no esta demasiado actualizada.

  Espero haberte servido de ayuda, un saludo desde España

Trackback this post  |  Subscribe to the comments via RSS Feed