Acciones
Tema 9: Editores lógicos
De Razonamiento automático (2018-19)
1 Deducción natural con Pandora
- Un libro que usa Pandora es Reasoned programming por K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers.
- Ejemplos con Pandora
- Ejemplo 1:
- p ∧ q → r ⊢ p → (q → r)
- p ∨ q ⊢ q ∨ p
- Ejemplo 2:
- p ∨ q → r ⊢ (p → r) ∧ (¬r → ¬q)
- Ejemplo 3:
- ∃x (P(x) ∨ Q(x)) ⊢ ∃xP(x) ∨ ∃xQ(x)
2 Deducción natural con Conan
- Conan se encuentra aquí.
- La descripción de Conan se encuentra aquí.
3 Cálculo de secuentes con Logitext
- Logitext se encuentra aquí aquí.
4 Cálculo de secuentes con Sequent Calculus Trainer
- Sequent Calculus Trainer se encuentra aquí.
5 Formalización
