Gentzen, Gerhard (Allemagne, 1909-Prague, 1945) [Dieudonné et al. 78, Lalement 90]. Gentzen formalise la notion de démonstration en la définissant comme un agencement de règles de déduction au contenu intuitif évident ( calcul des séquents*). Il peut ensuite raisonner sur la structure des démonstrations. L'une des règles de déduction, la règle de coupure, se révèle être redondante ; c'est le Hauptsatz* de Gentzen.
Le calcul des séquents de Gentzen, avec le théorème d'élimination des coupures, peut être vu comme le formalisme commun de la programmation logique et de la programmation fonctionnelle. Brièvement, la programmation fonctionnelle exploite l'élimination des coupures comme un mécanisme d'exécution, alors que la programmation logique exploite les règles de déduction comme règles de calcul de démonstrations sans coupure.
Grammaire logique. n.f. Depuis ses débuts, la programmation logique* est impliquée dans l'analyse syntaxique [Colmerauer 70, Colmerauer 78]. D'abord, on peut la considérer comme un sous-produit du travail de Colmerauer* sur l'analyse automatique de la langue naturelle. Ensuite, très vite, on a découvert qu'un formalisme de règles de grammaire sans contexte augmentées de termes attributs de premier ordre et non-interprétés était puissant et pouvait être traduit de manière directe dans le formalisme des programmes en clauses de Horn ( *). Dans cette optique, un interpréteur de programmes en clauses de Horn sert d'automate de reconnaissance.
Plus généralement, déduction et dérivation syntaxique offrent suffisamment de ressemblance pour que le concept de grammaire logique s'applique à des logiques et des structures linguistiques plus variées que la logique de Horn et les grammaires sans contexte [Abramson et Dahl 89]. Le concept est particulièrement fécond pour le traitement de la langue naturelle. Il suggère aussi l'incorporation à la programmation logique de stratégies d'analyse syntaxique : par exemple, l'analyse de Earley [Earley 70] est incorporée sous la forme de la Earley deduction [Pereira et Warren 83].