Vereinigungsbasierte Eliminierungsregel für Gleichheit

Vor ein paar Jahren bin ich auf die folgende linke Regel für Gleichheit in der sequentiellen Berechnung gestoßen:

$$\frac{s \doteq t \leadsto \theta \qquad \theta(\Gamma) \vdash \theta(C)} {\Gamma, s \doteq t \vdash C}$$

Hier berechnet $s \doteq t \leadsto \theta$ den allgemeinsten Unifier $\theta$ für $s$ und $t$ und wendet dann die Substitution auf die Schlussfolgerung $C$ und alle Hypothesen im Kontext $\Gamma$ .

Das Interessante an dieser Vereinigung ist, dass sie einen Ersatz für universelle (dh skolemische) Variablen findet.

Ich kann mich jedoch nicht erinnern, wo ich das gelesen habe, und habe mich gefragt, ob mir jemand helfen könnte, einen Hinweis darauf zu finden.

Ich habe dies oft den Regeln der Definitionsreflexion von Schröder-Heister zugeschrieben, obwohl die Idee darüber hinaus auf Girard und andere zurückgeht; Die Regel, nach der Sie suchen, ist eine Instanz der ersten Anzeige in Abschnitt 4. Sie benötigen jedoch auch eine Regel, die besagt, dass die Annahme der Gleichheit die Kraft eines Widerspruchs hat, wenn die Vereinigungsinstanz nicht zufriedenstellend ist.

Ein allgemeinerer Bericht wurde kürzlich in vielen Arbeiten von Dale Miller, David Baelde und der Firma verwendet (siehe zum Beispiel die kleinsten und größten Fixpunkte in der linearen Logik ). Die allgemeinere Formulierung - die auch nicht von Miller et al. Stammt - ist, dass die Regel lautet

$${\{\theta \in {\sf csu}(t,s) \mid \theta\Gamma \vdash \theta{C} \}}\over{\Gamma, t \doteq s \vdash C}$$

Dabei ist der vollständige Satz von Unifikatoren - der Satz aller einheitlichen Substitutionen von und . Möglicherweise bevorzugen Sie auch die von mir bevorzugte äquivalente Schreibweise dieser Regel (siehe hier zum Beispiel).${\sf csu}(t,s)$$t$$s$

$${\forall \theta. \theta{t} = \theta{s} \longrightarrow \theta\Gamma \vdash \theta{C}}\over{\Gamma, t \doteq s \vdash C}$$

In jedem Fall kann in einer Begriffssprache mit entscheidbarer Vereinigung, in der die Existenz eines Vereinigers die Existenz eines allgemeinsten Vereinigers impliziert, gezeigt werden, dass eine der oben genannten Regeln den beiden folgenden Regeln entspricht:

$${{{\sf no~mgu}(t,s)}\over{\Gamma, t \doteq s \vdash C}} \qquad {{{\sf mgu}(t,s) = \theta \quad \theta\Gamma \vdash \theta{C}}\over{\Gamma, t \doteq s \vdash C}}$$

(PS Frank hat dies in seinem Logikprogrammierkurs in den Vorlesungen 6, 7 und 8 besprochen , an die Sie sich möglicherweise erinnern.)