Sequentialkalkül

[PreDaTa]

hallo,
hab da noch ein paar fragen bezüglich Sequentialkalkül.

Auf was genau kommts an beim erstellen eines Modells, falls das kalkül nicht mehr ableitbar ist?!? sehe ich das richtig wenn man links von der ableitung z.B true-werte nimmt und rechts false, oder was ist genau die idee dahinter?!

kann man, wenn ein ableitungsbaum gescheitert ist abbrechen,..oder soll man das ganze kalkül weiter ableiten bis zum bitteren ende?

danke im voraus

mfG

R.W

[kill_switch]

Beim Sequentialkalkül zerlegst du ja so lange, bis nur noch Axiome oder Antiaxiome übrig bleiben.

bei Axiomen ist alles bewiesen, findest du aber ein Antiaxiom, stimmt die Formel nicht.

das mit den true und false einsetzen stimmt schon.
aber:
ein Antiaxiom ist z.b.
G |- A,B weil links und rechts keine gemeinsame Variable steht und deshalg z.b. mit I(A)=f, I(B)=f, I(G)=t
wir t |- f,f haben, was nicht sein darf.

deshalb ist

B,G |- A,B ein Axiom da links und rechts B steht. deshalb sind die beiden Seiten nicht mehr unabhängig und du kannst keinen Gegenbeweis finden.
(Beispiel entnommen vom Test SS 2003)


hoff es kann dir helfen

[Calida]

Hm ich hab da auch mal eine Frage dazu. Auf Übungsblatt 5 Bsp 1.
Kann mir wer erklären warum hier nach dem ersten Schritt, auf der linken Seite V-l ausgführt wird? Ich hätte angenommen das hier wieder impl -l angewendet werden muss...

Danke

[lEn00x]

du kannst dir eines von beiden aussuchen. Du wirst so-und-so auf der linken seite nur axiome rausbekommen.

[Calida]

Super, danke für die Rasche Antwort :)

[Anday]

Ich verstehe nicht, wie man bei Beispiel 5.7 auf das dritte Gegenbeispiel kommt und wie man Variablen die im Anti-Axiom nicht vorkommen mit true und false belegt!? (bei Bsp 5.7 wurden sie einfach mit false belegt, aber könnte das nicht ein Zufall sein???)

Bitte Danke

anday

[seimen]

ich versteh das mit dem sequentialkalkül nicht ganz und hab da ein paar grundlegende fragen:

zb das erste bsp im skript (4.31): da hab ich beim ersten schritt von unten nach oben:
|-((A imp B) u A) imp B --> imp-r --> (A imp B) u A|-B
darauf muss ich dann die regel für imp-r :
F|-G, A imp B --> imp-r --> F,A|-G,B anwenden.

jetzt ist mir nicht klar was da bei mir das F, G, A und B sind und wie ich das lesen muss, dh ob "sachen" durch einen beistrich getrennt werden oder zusammengehören.

vielleicht kann mir das wer mit hilfe von ein paar klammern erklären, wie ich die regeln lesen/deuten muss.

danke schon mal, ich hoffe man weiss worauf ich hinaus will...

edit:

ich habs ! :) , ist ja puppeneinfach
also das A und B sind einfach die seiten des terms den ich grad bearbeite, F ist alles links, und G alles rechts davon und wurscht.

juhu