19.10. - Diskussion über eine Modifikation des CND-Kalküls
CND ist ein Kalkül für natürliches Schließen in klassischer Logik, der auch als Typisierungsystem für Terme des \lambda\mu-Kalküls dient. Eine konstruktive Einschränkung dieses Kalküls erlaubt nun die Typisierung lediglich für sogenannte "sichere" \lambda\mu-Terme, die auf geschlossene reine \lambda-Terme reduziert werden können...
| Was |
|
|---|---|
| Wann |
19.10.2010 von 14:15 bis 15:45 |
| Wo | 3.04.1.02 |
| Termin übernehmen |
vCal
iCal
|
CND ist ein Kalkül für natürliches Schließen in klassischer Logik.
Crolard präsentiert in [1] eine Einschränkung dieses Kalküls auf
konstruktive Beweise als Kalkül \overline{CND}^r. Dabei behält er die
Mehrfach-Konklusionen von CND bei, definiert jedoch Abhängigkeiten
zwischen Hypothesen und Konklusionen. Die Einschränkung des Kalküls
ergibt sich nun auf Basis dieser Abhängigkeiten durch eine Modifikation
der Implikations-Introduktions-Regel.
Allerdings leidet diese Variante des Kalküls unter einem
Degenerierungseffekt, so dass sich scheinbar konstruktive Sequenzen wie
A\/B |- A, B nicht ableiten lassen.
Gegenstand der Diskussion soll nun sein, wie die Restriktion des Kalküls
gelockert werden könnte, um diesen Effekt zu vermeiden. Als
Anhaltspunkt dient der Sequenzenkalkül \lambda\mu_rPRL. Dieser nimmt
zwar in ähnlicher Art eine konstruktive Einschränkung klassischer Logik
vor, leidet jedoch nicht unter besagtem Effekt.
Literatur:
[1] Tristan Crolard, “A Constructive Restriction of the λμ-calculus.” Technical Report 02 (2002).
