Rechnergestütztes Beweisen (Hofmann, WS 2005/06)

2005-12-01 VL 14

Tatsache: Es gibt eine endliche Menge M von Gleichungen, so dass die
erzeugte Theorie <M> unentscheidbar ist.

Z.B.: Nicht-freie Monoide

Kanonisierung durch semantische Interpretation:

Sei T eine Gl.th. und II eine Interpretation von T.  Sei

  q_tau : [|tau|]_II -> Terme(tau)  
  u_tau : Variablen(tau) -> [|tau|]_II

so dass

  (N1) q_tau(u_tau(x)) = x in T

  (N2) Für jedes Funktionssymbol f : [tau1..taun -> tau] gilt

      q_tau([|f|](v1..vn)) = f(q_tau1(v1)..q_taun(vn)) in T

Dann ist sigma(t) := q_tau([|t|](x1->u_tau1(x1)..xn->u_taun(xn)))
(wobei x1:tau1..xn:taun > t : tau) ein Kanonisierer (erfüllt C1,C2).

NB: Terme(tau) = { t | K > t : tau für ein K }.

Bew: (C2) t1=t2 ==> sigma(t1)=sigma(t2) folgt aus der Tatsache, dass
sigma(t) nur von [|t|] abhängt.
(C1) sigma(t)=t durch Induktion über den Aufbau von t.


Entscheidung der Theorie der Monoide
====================================

Beispiel: T sei die Theorie der Monoide.  Es gibt nur einen Typ D.

Erste Möglichkeit:

  II(D)        = Var*    (endliche Wörter über den Variablen)
  [|*|](w1,w2) = w1 w2   (Juxtaposition/Konkatenation)
  [|e|]        = epsilon (leeres Wort)

  q(x1,...,xn) = x1 * (x2 * ... (xn * e) ...)
  u(x)         = x       (einbuchstabiges Wort)

Bedingungen sind erfüllt:

  (N1) q(u(x)) = x * e = x (in T)

  (N2) q(x1..xn y1..ym) = x1 * (... * (xn * (y1 * (... * (ym * e))...))...)
         --v1-- --v2--
       q(v1) * q(v2)    = (x1 * ... * (xn * e)) * (y1 * ... * (ym * e))
 
       Diese beiden Terme sind gleich in der Theorie der Monoide.

Zweite Möglichkeit:

  II(D) = { f : Terme -> Terme | es gibt einen Term t mit f(t') = t*t' in T }

  [|*|](f,g) = f o g  (Funktionskomposition)

  Wenn f in II(D) vermöge t1 und g in II(D) vermöge t2, dann
  f o g in II(D) vermöge t1*t2, denn

   f(g(t')) = t1 * g(t') = t1 * (t2 * t') = (t1 * t2) * t' in T

  [|e|](t)=t  (Identität) ist in II(D) vermöge des Terms e.

II(D) erfüllt alle Gesetze in T (Ass, L-, R-Neutr).

  q(f) = f(e)

  u(x)(t) = x * t

  q(u(x))  = u(x)(e) = x * e = x in T
  q(f o g) = f(g(e))     = t1 * (t2 * e)       =  (in T)
  q(f)*q(g)= f(e) * g(e) = (t1 * e) * (t2 * e)


Entscheidung der Theorie der Paare und Projektionen
===================================================

Typen: tau1, tau2 ::= beta | tau1 * tau2

Funktionssymbole:

        pr1_tau1,tau2 : [tau1*tau2 -> tau1]
        pr2_tau1,tau2 : [tau1*tau2 -> tau2]
       pair_tau1,tau2 : [tau1,tau2 -> tau1*tau2]

Schreibweise

  t.1     für   pr1_tau1,tau2(t)
  t.2     für   pr2_tau1,tau2(t)
  <t1,t2> für  pair_tau1,tau2(t1,t2)

Gleichungen

    <x,y>.1 = x
    <x,y>.2 = y
  <x.1,x.2> = x

Versuch einer semantischen Kanonisierung:

  II(beta) = Terme vom Typ beta

  II(tau1*tau2) = II(tau1) x II(tau2)  (kartesisches Produkt)

  [|pair|](u,v) = (u,v)
   [|pr1|](u,v) = u
   [|pr2|](u,v) = v

  q_beta(t) = t
  q_tau1*tau2((u,v)) = <q_tau1(u),q_tau2(v)>

Neutrale Terme seien Variablen gefolgt von Projektionen.

  u_tau : Neutrale Terme(tau) -> [|tau|]

  u_beta(n)      = n
  u_tau1,tau2(n) = (u_tau1(n.1),u_tau2(n.2))

Rest: Übungsaufgabe.


Kanonisierung durch Termersetzung
=================================

Sei T Gleichungstheorie und --> eine binäre Relation auf den Termen so
dass

  (1) (<-- UNION -->)* = "="         (Korrektheit,Vollständigkeit)

  (2) Für alle t gibt es ein t', so dass t -->* t' -/->.
      Solch ein t' heisst Normalform.    (Schwache Normalisierung)

  (3) Wenn  t -->* t1  und   t -->* t2, dann gibt es ein t'
      mit  t1 -->* t'  und  t2 -->* t'.                (Konfluenz)

Dann gibt für jeden Term t eine eindeutige Normalform t'.  Also ist
sigma(t)=t' berechenbar und ein Kanonisierer.


Quantorenfreie Formeln über einer Gleichungstheorie T
=====================================================

Gegeben: Boolsche Kombination phi von Gleichungen.
Frage  : Gilt phi in allen Modellen von T?

Bringe phi in KNF (i.a. mit exponentiellem Aufwand).
Prüfe jede Klausel separat.
Jede Klausel lässt sich in der Form

  s1=t1 AND ... AND sn=tn IMPLIES u1=v1 OR ... OR um=vm
  -------- Gamma --------

schreiben.  Wegen Konvexität reicht es, zu prüfen, ob

  Gamma ==> ui = vi

für ein i. [Nimm die Variablen in Gamma als neue Konstanten und füge
die Gleichungen in Gamma zur Theorie T hinzu.  Wende Konvexität dieser
neuen Gleichungstheorie an.]  Im Folgenden beschränken wir uns daher
auf Gleichungssequenzen der Form

  Gamma ==> gamma

wobei Gamma eine Menge von Gleichungen und gamma eine Gleichung ist.
Vorsicht!  Die freien Variablen in Gamma und gamma sind rigide,
d.h. dürfen nicht instantiiert werden!

Beispiel: T = "lineare Arithmetik"
      Gamma = {x+y=1, x-y=1}
      gamma = x=1
Gamma==>gamma ist dann wahr.

Beispiel: Sei T die Theorie der Monoide.
Gamma sei 

  ac=ca, ad=da, bc=cb, bd=db, fca=cf, fdb=df, 
  cdca = cdcaf, caaa=aaa, daaa=aaa

Es ist unentscheidbar, ob Gamma ==> t=aaa für gegebenen Term t.