Diferencia entre revisiones de «Sistemas»
De Razonamiento automático (2018-19)
(→Editores de pruebas por secuentes) |
|||
| Línea 11: | Línea 11: | ||
* [http://www.uni-kassel.de/eecs/fachgebiete/fmv/projects/sequent-calculus-trainer.html Sequent Calculus Trainer] (un demostrador para el cálculo de secuentes). | * [http://www.uni-kassel.de/eecs/fachgebiete/fmv/projects/sequent-calculus-trainer.html Sequent Calculus Trainer] (un demostrador para el cálculo de secuentes). | ||
* [http://logitext.mit.edu/main Logitext] (un demostrador interactivo basado en el cálculo de secuentes). | * [http://logitext.mit.edu/main Logitext] (un demostrador interactivo basado en el cálculo de secuentes). | ||
| + | |||
| + | == Formalización == | ||
| + | * [http://protosmart.uhu.es/apli2/login APLI2 (APLIcación de Ayuda Para Lógica Informática)]. | ||
Revisión del 10:45 24 ene 2019
En esta página se irá escribiendo enlaces a los sistemas utilizados en el curso
Sumario
1 Asistentes de demostración
2 Editores de pruebas por deducción natural
- Pandora (y copia local)
- Conan (y su descripción)
3 Editores de pruebas por secuentes
- Sequent Calculus Trainer (un demostrador para el cálculo de secuentes).
- Logitext (un demostrador interactivo basado en el cálculo de secuentes).