Lógica computacional y teoría de modelos (2019-20) Lógica computacional y teoría de modelos (2019-20)

Sistemas utilizados en Lógica computacional y teoría de modelos (2018-19)

En esta página se irá escribiendo enlaces a los sistemas utilizados en el curso

• gringo, clasp y clingo
  • Instalación de los sistemas:
    • En Ubuntu 16.04 se instala con: sudo apt-get install gringo
    • Instala gringo (4.5.4-1) y clasp (3.1.4-1).
    • Se puede comprobar la versión con: gringo --version (clasp -- version)
    • La ayuda se obtiene con: gringo --help
    • Formas de ejecutarlo:

   gringo [ opciones | ficheros ] | clasp [ opciones | número ]
   clingo [ opciones | ficheros | número ]

• • • • gringo transforma un programa lógico en un programa equivalente sin variables.
      • clasp obtiene los modelos a partir de la salida de gringo.
      • clingo es una combinación de gringo y clasp.

1. Isabelle/HOL.
2. APLI2 (APLIcación de Ayuda Para Lógica Informática).
3. Conan (un editor de demostraciones por deducción natural).
4. ELFE prover (Interactive theorem proving for students).
5. Logitext (un demostrador interactivo basado en el cálculo de secuentes).