Deduction using the ProofWeb system

De WikiGLC
Revisión del 11:08 13 nov 2008 de Jalonso (discusión | contribuciones) (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. --...)
(dif) ← Revisión anterior | Revisión actual (dif) | Revisión siguiente → (dif)
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 interesante en el proyecto ...

José A. Alonso 10:08, 13 November 2008 (CET).

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