Inferenz mit Umgebungen

Motivation: Inferenzsystem für (aussagenlogische) Formeln mit Variablenbindung

• Grundbereich: Aussagen der Form $\mathsf {wert}$ (E, F, B)

  (in Umgebung E hat Formel F den Wert B)

• Regeln für Operatoren $${\frac{{\operatorname{\mathsf{wert}}(E,X,1),\operatorname{\mathsf{wert}}(E,Y,1)}}{{\operatorname{\mathsf{wert}}(E,X\wedge Y,1)}}}$$,…
• Regeln für Umgebungen $${\frac{{}}{{\operatorname{\mathsf{wert}}(E[v:=b],v,b)}}}$$,    $${\frac{{\operatorname{\mathsf{wert}}(E,v',b')}}{{\operatorname{\mathsf{wert}}(E[v:=b],v',b')}}}$$ für v≠v'
• Regeln für Bindung: $${\frac{{\operatorname{\mathsf{wert}}(E,X,b), \operatorname{\maths... ...,Y,c)}}{{\operatorname{\mathsf{wert}}(E,\mathtt{let~} v=X \mathtt{~in~} Y,c)}}}$$