Herramientas
Dos herramientas para explorar el cálculo lambda y la deducción natural.
AST Playground
Construí y explorá árboles de sintaxis de expresiones del cálculo lambda: arrastrá nodos, editá fórmulas, cargá expresiones desde la barra y compartí por URL.
Empezá con una gramática:
Proof Playground
Construí árboles de deducción natural arrastrando reglas de inferencia sobre metas abiertas. Las aplicaciones se verifican por unificación y las metavariables se propagan por toda la demostración.
Empezá con un sistema de reglas: