Tema 9: Editores lógicos

1 Deducción natural con Pandora

• Pandora se encuentra aquí (o en su copia local)

• 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

• APLI2 (APLIcación de Ayuda Para Lógica Informática).