Diferencia entre revisiones de «Sistemas»
De Razonamiento automático (2018-19)
| Línea 1: | Línea 1: | ||
En esta página se irá escribiendo enlaces a los sistemas utilizados en el curso | En esta página se irá escribiendo enlaces a los sistemas utilizados en el curso | ||
| + | |||
| + | == Asistentes de demostración == | ||
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html Isabelle/HOL]. | # [http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html Isabelle/HOL]. | ||
| + | |||
| + | == Editores de pruebas por deducción natural == | ||
| + | # [http://www.doc.ic.ac.uk/pandora/newpandora Pandora] (y [https://www.cs.us.es/~jalonso/cursos/lmf/sistemas/pandora.jar copia local]) | ||
| + | # [http://web.student.chalmers.se/~jespolss/Conan.html Conan] (y su [https://t.co/8aNC1H9MvD descripción]) | ||
| + | |||
| + | == Editores de pruebas por 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). | ||
Revisión del 20:06 23 ene 2019
En esta página se irá escribiendo enlaces a los sistemas utilizados en el curso
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).