Retour à la page du séminaire

Tristan Crolard (Université de Paris 12 Creteil)
Propriété de la forme normale en Logique Soustractive

résumé

La Logique Soustractive est une extension la logique intuitionniste avec un nouveau connecteur (la soustraction) dual de l'implication. Cette extension est conservative dans le cadre propositionnel. Il est par ailleurs possible de définir une restriction de la déduction naturelle classique (ou de LK), stable par réduction, qui capture cette logique. La preuve de la conservativité peut donc s'obtenir de manière habituelle par élimination des coupures. Toutefois, ces formes normales ne permettent pas d'obtenir directement la propriété de la disjonction (en raison des séquents à conclusions multiples). Nous discuterons des règles supplémentaires à considérer pour obtenir de "bonnes" formes normales.