Beispiele für den PL-Beweiser

Verwandte Seiten

Sie finden in der Folge eine Reihe von Übungsbeispielen, großteils aus dem Buch "Elementare Logik" von Benson Mates. Diese Beispiele sind Teil der Testsuite für meinen Theorembeweiser. Wenn Sie selber eines der Beispiele verwenden möchten, tragen Sie es am besten mittels "copy & paste" in den Eingabebereich des Beweisers ein. Beachten Sie, dass einige dieser Beispiele nur vom Verfahren Mates erfolgreich hergeleitet werden können und dass manche von ihnen einen hohen Rechenzeitbedarf aufweisen.

alle(x,alle(y,F(x,y)))<->alle(y,alle(x,F(x,y)))

ein(x,ein(y,F(x,y)))<->ein(y,ein(x,F(x,y)))

ein(x,alle(y,F(x,y)))->alle(y,ein(x,F(x,y)))

alle(x,F(x)&G(x))  <-> \
	(alle(x,F(x)) & alle(x,G(x)))

(alle(x,F(x)) v alle(x,G(x))) -> alle(x,F(x)v G(x))

(alle(x,F(x)) v alle(x,G(x))) -> \
	alle(x,F(x) v G(x))

ein(x,F(x)&G(x)) -> (ein(x,F(x)) & ein(x,G(x)))

ein(x,F(x) v G(x)) <-> (ein(x,F(x)) v ein(x,G(x)))

```
alle(x,P v F(x)) <-> (P v alle(x,F(x)))
```

~(alle(x,P v F(x)) <-> (P v alle(x,F(x))))

```
alle(x,P->F(x)) <-> (P->alle(x,F(x)))
```
```
ein(x,P & F(x)) <-> (P & ein(x,F(x)))
```
```
ein(x,P v F(x)) <-> P v ein(x,F(x))
```
```
ein(x,P->F(x)) <-> P->ein(x,F(x))
```
```
alle(x,F(x)->P) <-> ein(x,F(x))->P
```
```
alle(x,F(x)->P) <-> ein(x,F(x))->P
```
```
alle(x,P & F(x)) <-> (P & alle(x,F(x)))
```
```
ein(x,F(x)->P) <-> (alle(x,F(x)) -> P)
```

alle(x,ein(y,F(x) & G(y)))
(alle(x,F(x)) & ein(y,G(y)))

alle(x,ein(y,F(x)&G(y)))
ein(y,alle(x,F(x)&G(y)))

alle(x,F(x)) v ein(y,G(y)) <->\
alle(x,ein(y,F(x) v G(y)))

alle(x,ein(y,F(x)v G(y)))
ein(y,alle(x,F(x)v G(y)))

alle(x,ein(y,F(x)->G(y)))
ein(y,alle(x,F(x)->G(y)))

alle(x,ein(y,alle(z,ein(w,~F(x,y)v F(w,z)))))

ein(x,ein(y, ~I(x,y) & alle(z,I(z,x) v I(z,y)) ))
ein(x,ein(y,~I(x,y))) & alle(x,alle(y,alle(z,(I(x,y) v I(x,z)) v I(y,z))))

```
~(alle(x1,ein(x2,ein(x3,alle(x4,ein(x5,F(x2,x1,x5)  &
~F(x4,x3,x5)))))))
```
Beachten Sie, dass dieser Ausdruck kein Theorem ist, sondern einen Fehler in den Tableaumethoden des Beweisbauers demonstriert, der irgendwann - wenn es die Zeit erlaubt - behoben werden soll. Vielen Dank an Timm Lampert für den Hinweis auf diesen Fehler.

2012-03-31 01:19:53
christian.gottschall@posteo.de