Ciudades

Una red de vuelos entre ciudades. $\mathrm{conn}(A, B)$ es un vuelo directo de $A$ a $B$; $\mathrm{walk}(A, B)$ significa que $B$ es alcanzable desde $A$ encadenando vuelos. El objetivo es demostrar que existe una ruta.

Reglas

• Los axiomas son los vuelos directos, nombrados por las iniciales de las ciudades (por ejemplo $\mathrm{NR}$ para $\mathrm{conn}(NuevaYork, Roma)$).
• $\mathrm{DIR}$: un vuelo directo es una ruta — de $\mathrm{conn}(A, B)$ se obtiene $\mathrm{walk}(A, B)$.
• $\mathrm{COMP}$: las rutas se componen — de $\mathrm{walk}(A, B)$ y $\mathrm{walk}(B, C)$ se obtiene $\mathrm{walk}(A, C)$.

Convenciones

• Las ciudades (NuevaYork, Roma, Sydney, Tokyo, Odense) son constantes.
• Las mayúsculas sueltas ($A$, $B$, $C$) son metavariables que se unifican al aplicar una regla. Una metavariable que una regla introduce pero la meta no determina — como la escala intermedia de $\mathrm{COMP}$ — queda en rojo hasta que otra rama de la demostración la fije, y ese valor se propaga a las metas hermanas.

---

Adaptado de Fabrizio Montesi, «Introduction to Choreographies», Capítulo 1.

Modo libre

Un editor de árboles de deducción sin validación lógica: cualquier texto es una proposición válida y toda regla puede aplicarse sobre cualquier meta. Sirve para bosquejar libremente la forma de una demostración.

Convenciones

• Las proposiciones y los nombres de regla se escriben en LaTeX y se muestran como fórmulas (por ejemplo $A \wedge B$ o $\to\! I$).
• Los tokens de la forma $?a$, $?b$, … son metavariables sin asignar y se muestran en rojo. Tocá un nodo para editar su proposición, o el nombre de una regla para renombrarla.
• Las reglas se nombran por su cantidad de premisas: $\mathrm{Ax}$ (0 premisas), $R_1$ … $R_4$.

Lógica proposicional

Deducción natural para la lógica proposicional con contextos. Una meta tiene la forma $\Gamma \vdash \tau$: «a partir de las hipótesis del contexto $\Gamma$ se deduce la fórmula $\tau$».

Reglas

• $\mathrm{ax}$: si la fórmula ya está en el contexto ($\tau \in \Gamma$), la meta se cierra.
• $\bot_e$: de $\Gamma \vdash \bot$ (una contradicción) se deduce cualquier fórmula.
• $\wedge_i$, $\wedge_{e_1}$, $\wedge_{e_2}$: introducción y eliminación de la conjunción.
• $\vee_{i_1}$, $\vee_{i_2}$, $\vee_e$: introducción y eliminación de la disyunción (la eliminación analiza cada caso extendiendo el contexto con su hipótesis).

Convenciones

• Las metavariables son letras griegas minúsculas — $\tau$, $\sigma$, $\rho$ para fórmulas — y $\Gamma$ para el contexto.
• Los símbolos proposicionales son letras latinas ($A$–$Z$, $a$–$z$); $\bot$ es la contradicción (falso).
• El contexto $\Gamma$ es un conjunto de fórmulas. La pertenencia $\tau \in \Gamma$ sólo se decide cuando el contexto es concreto; si todavía tiene incógnitas, el axioma aún no puede cerrar la meta.