Deduction using the ProofWeb system

De WikiGLC
Saltar a: navegación, buscar

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.

Obtenido de «https://www.glc.us.es/web/index.php?title=Deduction_using_the_ProofWeb_system&oldid=412»