Diferencia entre revisiones de «Tema 9: Editores lógicos»
De Razonamiento automático (2018-19)
(→Deducción natural con Pandora) |
(→Deducción natural con Pandora) |
||
(No se muestran 2 ediciones intermedias del mismo usuario) | |||
Línea 3: | Línea 3: | ||
* Pandora se encuentra [http://www.doc.ic.ac.uk/pandora/newpandora aquí] (o en su [https://www.cs.us.es/~jalonso/cursos/lmf/sistemas/pandora.jar copia local]) | * Pandora se encuentra [http://www.doc.ic.ac.uk/pandora/newpandora aquí] (o en su [https://www.cs.us.es/~jalonso/cursos/lmf/sistemas/pandora.jar copia local]) | ||
− | * Un libro que usa Pandora es [ | + | * Un libro que usa Pandora es [https://www.doc.ic.ac.uk/~susan/firstyearbook.pdf Reasoned programming] por K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers. |
* Ejemplos con Pandora | * Ejemplos con Pandora | ||
− | ** [http://bit.ly/1tqZIOe | + | ** [http://bit.ly/1tqZIOe Ejemplo 1]: |
*** p ∧ q → r ⊢ p → (q → r) | *** p ∧ q → r ⊢ p → (q → r) | ||
*** p ∨ q ⊢ q ∨ p | *** p ∨ q ⊢ q ∨ p | ||
− | ** [http://bit.ly/1nWAVp4 | + | ** [http://bit.ly/1nWAVp4 Ejemplo 2]: |
+ | *** p ∨ q → r ⊢ (p → r) ∧ (¬r → ¬q) | ||
+ | ** [http://bit.ly/18BMtGx Ejemplo 3]: | ||
+ | *** ∃x (P(x) ∨ Q(x)) ⊢ ∃xP(x) ∨ ∃xQ(x) | ||
== Deducción natural con Conan == | == Deducción natural con Conan == |
Revisión actual del 08:00 25 ene 2019
Sumario
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
2 Deducción natural con Conan
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í.