Logique pour programmeurs : Une introduction en douceur au calcul des séquents

Ce billet, le premier d'une série sur la logique, introduit le calcul des séquents comme un système puissant pour le raisonnement. En utilisant la notation de Gentzen, l'auteur explique comment représenter symboliquement les inférences logiques, en couvrant les règles d'inférence, les arbres de dérivation et les métavariables. L'article compare le calcul des séquents, la déduction naturelle des séquents et la déduction naturelle, et aborde le calcul des séquents unilatéral et la logique intuitionniste. Enfin, il présente brièvement les termes de preuve en logique intuitionniste et leur connexion avec le lambda-calcul simplement typé.