Diferencia entre revisiones de «Deduction using the ProofWeb system»
(New page: C. Kaliszyk, F. van Raamsdonk, F. Wiedijk, H. Wupper, M. Hendriks y R. de Vrijer ''[http://proofweb.cs.ru.nl/man.pdf Deduction using the ProofWeb system]''. ICIS Technical Report, 2008. --...) |
|||
| (No se muestra una edición intermedia del mismo usuario) | |||
| Línea 3: | Línea 3: | ||
ProofWeb es un editor de demostraciones verificadas en la Web. Su finalidad es pedagógica. El cálculo es de deducción natural (parecido al del libro de Huth y Ryan). Permite distintas presentaciones de las pruebas: cálculo de secuentes, cajas de Fitch. La presentación básica es mediante tácticas en Coq, pero permite introducir las reglas mediantes menús como en Jape. A diferencia de Jape, permite razonar con funciones y con igualdad. Además de Coq, permite la interacción con otros sistemas somo Isabelle. | ProofWeb es un editor de demostraciones verificadas en la Web. Su finalidad es pedagógica. El cálculo es de deducción natural (parecido al del libro de Huth y Ryan). Permite distintas presentaciones de las pruebas: cálculo de secuentes, cajas de Fitch. La presentación básica es mediante tácticas en Coq, pero permite introducir las reglas mediantes menús como en Jape. A diferencia de Jape, permite razonar con funciones y con igualdad. Además de Coq, permite la interacción con otros sistemas somo Isabelle. | ||
| − | Este sistema es | + | Este sistema es puede integrarse en el proyecto [[APLI2S (APLIcaciones de Ayuda Para Lógica Informática)]]. |
| − | [[User:Jalonso|José A. Alonso]] | + | [[User:Jalonso|José A. Alonso]] 8:30, 13 Noviembre 2008 |
[[Category:Lecturas]]. | [[Category:Lecturas]]. | ||
Revisión actual del 11:12 13 nov 2008
C. Kaliszyk, F. van Raamsdonk, F. Wiedijk, H. Wupper, M. Hendriks y R. de Vrijer Deduction using the ProofWeb system. ICIS Technical Report, 2008.
ProofWeb es un editor de demostraciones verificadas en la Web. Su finalidad es pedagógica. El cálculo es de deducción natural (parecido al del libro de Huth y Ryan). Permite distintas presentaciones de las pruebas: cálculo de secuentes, cajas de Fitch. La presentación básica es mediante tácticas en Coq, pero permite introducir las reglas mediantes menús como en Jape. A diferencia de Jape, permite razonar con funciones y con igualdad. Además de Coq, permite la interacción con otros sistemas somo Isabelle.
Este sistema es puede integrarse en el proyecto APLI2S (APLIcaciones de Ayuda Para Lógica Informática).
José A. Alonso 8:30, 13 Noviembre 2008.
