Prädikatenlogik (Stufe 1)

ich kann leider immer noch nicht ganz folgen.
Kannst du oder jmd anders das mal Schritt für Schritt mit mir durchgehen?

Also so wie ich die PL verstanden habe muss ich erst einmal alles was ich weiß aufschreiben (in Normalform bringen ) und vor allem eine Art Behauptung aufstellen.
Diese Behauptung wird dann negiert und mit dem Rest und-Verknüpft.

Liege ich soweit erstmal richtig?

Also ich denke meine 2 Aussagen von oben dürften erstmal stimmen, auch wenn diese noch nicht in Normalform sind.

Mein großes Problem ist eigentlich ganz anderer Natur:
Was ist meine Behauptung oder was will ich zeigen????

[ Will ich zeigen dass es einen Ort gibt an dem Lnechen ist?
[ Oder will ich zeigen dass Lenchen in der Schule ist?
[ ...

Ich weiß nicht so recht wie ich "Wo ist Lenchen?" übersetzen soll.

Axiome:

1. befindet_sich(Schule, C)
2. für alle x: (befindet_sich(x, C) -> befindet_sich(x, L))

Folgerungen:

da "A -> B" dasselbe ist wie "nicht(A) oder B", ist folgendes true:

2'. für alle x: (nicht(befindet_sich(x, C)) oder (befindet_sich(x, L)))

wegen 1. ist

nicht(befindet_sich(Schule, C)) == false

also muß -- mit x:=Schule eingesetzt in 2' -- gelten:

befindet_sich(Schule, L) == true

Bashar

Man müsste schon wissen, welches Ableitungs/Beweisverfahren hier gefragt ist. Resolution? Dazu müssten man in konjunktive, nicht disjunktive Normalform umwandeln. Sequenzenkalkül? Irgendein formaler Beweis wird schon gefragt sein, ansonsten könnte man auch mit Recht schreiben "wie man leicht sieht...".

Interessant übrigens, dass man "Lenchen befindet sich im Schwimmbad" mit dieser Theorie nicht widerlegen kann.

also bei uns heißt das automatisches Beweisen

Aus einer Menge M von Voraussetzungen folgt eine Aussage A.

Dann muss ich zeigen dass M ∧ ¬A = F gilt.

In meinem Fall weiß ich jedoch nicht was A überhaupt ist.

(¬B ∨ A)∧ (¬A)∧ (C ∨ B)∧ (¬C) ....
so sieht bei uns ein Beispiel aus, am Schluss eine Konjunktion von Disjunktionen

hier ein vollst. Beispiel

E XAMPLE 125. automatischer Widerspruchsbeweis PL1
Man hat folgende Fakten:
(1)
(2)
(3)
(4)
(5)
(6)
(7)
Marcus war aus Pompeii
Pompeiier sind Römer
Caesar war ein Staatschef
Alle Römer sind loyal zu Caesar oder sie hassen ihn
Jeder ist loyal zu irgendjemanden
Wer einen Staatschef umbringt ist nicht loyal zu ihm
Marcus versucht Caesar umzubringen
P OM P EI(M arkus)
(∀x)P OM P EI(x) ⇒ ROM AN (x)
LEADER(Caesar)
(∀x)ROM AN (x) ⇒ LOY AL(x, Caesar) ∨ HAT E(x, Caesar)
(∀x)(∃y)LOY AL(x, y)
(∀x)(∀y)LEADER(y) ∧ KILL(x, y) ⇒ ¬LOY AL(x, y)
KILL(M arcus, Caesar)
Dies werden die folgenden PL1 Formeln
(1)
(2)
(3)
(4)
(5)
(6)
(7)
Es soll bewiesen werden, dass Marcus Caesar hasst. Dazu wird diese Aus-
sage verneint und den 7 PL1 Formeln hinzugefügt:
(8) ¬HAT E(M arcus, Caesar)
Erster Schritt ist das Erreichen der Klauselform
(1)
(2)
(3)
(4)
(5)
POMPEI(M arkus)
¬P OM P EI(x1) ∨ ROM AN (x1)
LEADER(Caesar)
¬ROM AN (x2) ∨ LOY AL(x2, Caesar) ∨ HAT E(x2, Caesar)
LOY AL(x3, f 1(x3))

steht doch im Anfangsposting schon da: disjunktive Normalform.

also "A -> B" == "nicht(A) v B", da ist gar keine Zusatzinformation nötig, und daß man eine "für alle x: ... == true" Aussage durch beliebiges Einsetzen (hier x := Schule) nicht falsifiziert, dürfte klar sein.

man darf nur nicht:

"->" (also "nicht(A) v B")

mit

"=>" (Implikation auf der Meta-Ebene, d.h. logische Ableitung unter Ausnutzung
der Gesetze der prädi-Logik)

verwechseln!

ich verstehe die logik ja auch eigentlich aber ... des wirkt sehr abstrakt
Ich weiß einfach nicht wie man Fragen übersetzt.
Also Aussagen ist kein Problem

Aber wie zB würde ich ein Problem

Wie heißt er?

logisch ausdrücken?

Ich mach mir mehr Probleme als nötig glaub ich mittlerweile=)

Aber danke für deine beständigen Hilfestellungen

Bashar

Man könnte die Frage als Existenzaussage formulieren: Es gibt einen Ort, an dem Lenchen sich befindet.

Formeln:
ort(S,C)
forall x: ort(x,C) -> ort(x,L)
negierte Behauptung: ~exist x: ort(x,L)

in DNF, Pränexform (sorry, war vorhin verwirrt, DNF ist natürlich richtig):
ort(S,C)
forall x: ~ort(x,C) v ort(x,L)
forall y: ~ort(y, L)

Skolemform: einfach die Allquantoren wegwerfen, da keine Existenzquantoren da sind

Klauselmenge:
{{ ort(S,C) }, { ~ort(x,C), ort(x,L) }, { ~ort(y,L) }}

Resolution:
{ort(S,C)}
{~ort(x,C), ort(x,L)}
---------------------
{ort(S,L)} (allgemeinster Unifikator: [x/S])

{ort(S,L)}
{~ort(y,L)}
-----------
{} (allgemeinster Unifikator: [y/S])

Wir haben den elementaren Widerspruch abgeleitet und damit die Behauptung bewiesen. Die existenzquantifizierte Variable y in der Behauptung "es gibt einen Ort y, an dem Lenchen sich befindet" wurde durch den Unifikator durch S ersetzt, d.h. Lenchen befindet sich in der Schule.

Ich bin mir nicht 100% sicher, ob das so abläuft, aber ich finde es algorithmisch plausibel.

die Aufgabe ist an Trivialität ja wirklich schwer zu überbieten.

Wie geschrieben, "->" durch disj. NF ersetzen und beachten, daß eine Tautologie mit "für alle x ..." eine solche bleibt, wenn man auf "x := Schule" spezialisiert, und fertig.

shisha schrieb:

Hallo ich hab hier folgende Aufgabe

1. Christian ist in der Schule
2. Lenchen ist immer dort wo Christian ist

Wo ist Lenchen?

1. würde ich sagen:

BEFINDET_SICH(Schule, Christian)

2. würde ich folgendes behaupten:

für alle x BEFINDET_SICH(x, Christian) -> BEFINDET_SICH(x, Lenchen)

Ist das soweit richtig?
Und was will ich eigentlich zeigen?
Dass es einen Ort gibt an dem Lenchen ist?

Das ganze soll dann in dijunktive Normalform gebracht werden und somit letztendlich die Frage beantwortet werden, nur weiß ich noch nicht ganz wie das funktionieren soll

^^ das was marmorkuchen geschrieben hat stimmt schon, a->b ist dasselbe wie 'not a or b', aus was wahrem kann man nichts falsches folgern, aus falschem aber beides (wahrheitstabelle aufmalen, dass siehste's).
btw, du hast in der zweiten aussage noch den zeitlichen quantor 'immer' drin. vielleicht sollste den auch berücksichtigen?

o nein fricky hat meinen thread entweiht....

ne des problem lag ganz wo anders, des -> zu ersetzen ist mir schon vorher klar gewesen, nur nicht was ich genau machen soll

die aufgabe ist ... zu einfach oder ich zu blöd

Bashar

Oder zu blind.