Posts by Neverlasting

    Das ist richtig, aber man muss nicht eine riesengroße Menge an Möglichkeiten durchprobieren. Zuerst überlegt man sich ohne Tableau-Algorithmus, warum

    aus der KB folgt. Dann weiß man, welche Expansionen man beim Tableau-Algorithmus machen muss.


    Das ist sicher hilfreich, aber nicht notwendig, um die Aufgabe in vertretbarer Zeit zu lösen. Es sollte reichen, solange wie möglich nur deterministische Regeln zu verwenden. (Oder halt z. B. die Oder-Regel nur, wenn von einem Disjunkt eh schon die Negation im Label steht, sodass man den dazugehörigen Zweig nicht mehr anschauen muss, weil er sowieso einen Clash erzeugen würde.)


    Welche Expansionen man machen muss, damit man was hat? Einen Clash? Ein Clash in einer Folge von Expansionen würde ja noch nicht bedeuten, dass alle möglichen Folgen von Expansionen zu einem Clash führen!?


    Wenn du solange es geht nur deterministische Regeln anwendest, und nichtdeterministische nur wenn einer der Zweige sowieso gleich wegen eines Clash wegfällt, dann schon.

    Zuerst muss man

    negieren, in NNF umwandeln, und zu K hinzufügen.


    Richtig. Und zu beachten ist, dass die GCIs umgeschrieben werden müssen zu einer Konzept-Konjunktion von Konzept-Disjunktionen. Die TBox kommt außerdem erst durch die T-Regel zu den Knoten und ist nicht im initial completion graph.


    Das zweite ist falsch, meiner Meinung nach.


    Dem schließe ich mich an. Also zusammenfassend: Aufgabe 5: f, f, t, t.



    Hat eigentlich jemand einen formalen Beweis für 1.2? Also dass eine "aufgeblasene" Interpretation immer noch ein Modell ist? Mir fällt momentan nur was ein, was wohl unerträglich viel Schreibarbeit wäre...

    Im übrigen bin ich der Meinung, dass 1.2 unglücklich ausgedrückt ist: "There is a TBox that has only finite models." Man könnte ja argumentieren: Da es eine TBox gibt, die unerfüllbar ist (Aufgabe 1.1), gilt auch für jedes ihrer Modelle (es gibt ja keine), dass es endlich ist. Aber ich nehme an, das war nicht gemeint...

    Bei mir war das gleiche Problem. Praktischerweise bin ich gleichzeitig an der Uni Wien inskribiert und damit ist's gegangen. Ich tippe also darauf, dass die TU "schuld" ist. Vielleicht ist irgendein Server wieder mal überlastet? Aber weiß auch nicht, wie das genau überprüft wird...

    DEFERRABLE INITIALLY DEFERRED : kontrolliert deferred constraint.
    kann jemand das bestaetigen?


    Es wäre sinnvoll, sich zu überlegen, was es heißt, dass ein constraint deferred ist und wozu man das braucht. Mit Stichwörter auswendig Lernen wird man nicht weit kommen. Aber wer die Aufgabe selbst gelöst hat (sprich: nicht von Kollegen oder von einer alten Musterlösung abgeschrieben), sollte damit kein Problem haben.

    Da der Nenner jedoch 0 sein kann muss dies abgefangen werden.


    Es müsste möglich sein, die Aufgabe so zu lösen, dass das nicht notwendig ist. Du kannst gerne 0 abfangen, solange das Ergebnis stimmt, aber ich könnte mir vorstellen, dass dann die Lösung vielleicht komplizierter wird als nötig. Bei Outer Joins gibt's ja Nullwerte (also nicht die Zahl 0), wenn es für ein Tupel keinen Joinpartner gibt, und in so einem Fall sollte auch eine Division keinen Fehler liefern. Wenn du auf eine sehr komplizierte Lösung der Aufgabe kommst, würde ich empfehlen, vielleicht nochmal drüber nachzudenken, ob man's einfacher machen kann, bevor du dich und den Tutor mit unlesbaren SQL-Ungetümen plagst. :) Prinzipiell sollte die Aufgabe nicht sehr kompliziert sein, auch wenn man vielleicht ein bisschen nachdenken muss.

    Gar nicht. Alles was die Angabe hier verlangt, ist ein Attribut "key" vom Typ "string" als verpflichtend zu definieren, und das war's in diesem Fall. Der Rest ist wohl nur ein Kommentar dazu, was die Bedeutung sein soll, oder wie das Dokument dann letzten Endes aussehen soll. Zum Sicherstellen von Eindeutigkeit und Referenzierung gibt's ja am Schluss der Angabe noch ein paar eigene Aufgaben (key, keyref).

    WTF? Wenn ich sowas wie if(a || !b) c; else d; schreibe, dann meint CBMC, er findet kein Gegenbeispiel. Aber wenn ich stattdessen if(!a && b) d; else c; schreibe kommt endlich mein Gegenbeispiel. Das gleiche ist wenn ich statt "if(a || b) c;" schreibe: "if(a) c; if(b) c;" Ich bin jetzt schon viel zu lange wach und mein Kopf funktioniert nicht mehr so richtig, aber sollte das nicht genau das gleiche machen?

    Naja, da da steht, man soll "alle" finden nehm ich an exakte Methoden sollten schon sein, auch wenn's in dem Beispiel vielleicht wurscht wäre.
    Ich hab Needleman-Wunsch verallgemeinert, Ziemlich grausige Sache, mit dreidimensionalen Matrizen zu rechnen. Hab mir ein Programm dafür geschrieben, bin mir aber nicht ganz sicher ob es stimmt. Ich komm jedenfalls auf nur ein optimales Alignment, das den Wert 3 hat:

    Code
    1. A-TC
    2. CAGC
    3. C-GC

    Wäre schön, wenn es jemand bestätigen / widerlegen könnte.


    Korrektur: Bin auf einen Fehler draufgekommen. Krieg jetzt zwei Alignments mit Wert 3...

    Nicht von der anfangs steifen Atmosphäre einschüchtern lassen, bei uns war sie ganz nett. Ihr bekommt meines Wissens zwei "Aufgaben", die darin bestehen, einen Fehler den ihr gemacht habt auszubessern oder so ähnlich... Aber in den Folien darf nachgeschaut werden. Alles nicht so wild, man sollte halt ungefähr verstanden haben, was man da gemacht hat.

    jo, genau e (wie vorher) ist für alle inputs defined.


    Warum?


    Wenn e keine totale Funktion ist, also undefiniert sein kann, dann haben wir ein Problem, oder? Weil dann können {F & e}p{G} und {F & -e}q{G} t. c. sein, aber daraus folgt nicht, dass in einem Zustand wo F gilt, auch e definiert ist. Somit gilt die Konklusion ja nicht, oder hab ich mich da vertan?


    Also brauchen wir, dass e immer definiert ist. Aber warum soll e für alle Zustände definiert sein?

    Ich hab die y auch alle rausgeworfen (durch zweimalige Durchführung der Vereinfachung mit dem Gleichheitsgraphen). Bin mir nicht hundertprozentig sicher, aber ich glaube schon, dass es trotzdem equisat. ist. Es geht ja nicht um Äquivalenz, sondern Equisatisfiability.


    Wenn das Ergebnis der Vereinfachung equisat. zur urspr. Formel ist, dann ist wohl das Ergebnis der Sparse Method auf die Vereinfachung immer noch equisat. zur urspr. Formel!?


    Ich komme übrigens auf


    (wobei e_{i,j} nur für x-Gleichheiten stehen) und auf


    Kann das jemand bestätigen / widerlegen?

    Wieso gibt es beim 2. Übungsblatt nur 8 Beispiele?


    Psssst! Hast du etwa zuwenig zu tun? ;)


    Hat die Hausübung, die irgendwo in den Folien war auch 2 Punkte gegeben oder gibt es diesmal nur 8 Punkte (oder geben gewisse Beispiele mehr als einen Punkt)?


    Nein, die hat soweit ich weiß keine Punkte gegeben. Ich glaube mich zu erinnern, dass Prof. Egly gemeint hat, es gäbe auch auf dieses Aufgabenblatt 10 Punkte, obwohl halt nur 8 Aufgaben sind.

    Also für die Regel "In jedem Feld darf nur eine Zahl stehen" hätte ich diesen Formelteil hier:



    Geht das irgendwie schöner/kürzer? Ist das überhaupt korrekt? ;)



    Das ist nicht in CNF. Ich hab sowas in der Art wie "für jedes Feld und für jede Kombination von 2 Farben dürfen nicht beide Variablen wahr sein".

    Aber wenn man sich die NNF Form der Formel auf den Folien ansieht, dann sieht man, dass eine Negation 2 x vorkommt
    was dazu führt, dass die ganze Formel pos. Polarität hat.


    Um sicher zu gehen hab ich nun mal das 4'te Bsp auch in NNF umgewandelt.
    Ich sehe 4 x Negation in der NNF. Somit kann ich sagen, dass der root + ist weil 4 == gerade


    Momenterl... Soweit ich weiß, ist die Polarität eines Knotens positiv genau dann, wenn die Anzahl der Negationen von der Wurzel bis zu diesem Knoten gerade ist. Somit bei der Wurzel immer positiv. Oder?

    polarität is zwecks optimierung da.. aber wie wende ich sie an?


    So wie ich das verstanden habe, interessiert dich die Polarität bei Tseitin gar nicht und kommt halt bei Plaisted-Greenbaum zum Einsatz, um wie du sagst die Translation insofern zu optimieren als redundante Klauseln gestrichen werden. Positive Polarität: Nur --> Richtung der Äquivalenz übersetzen. Negative Polarität: Nur <-- Richtung. Glaub ich ;)
    (Ich finde es eigentlich schon ein bisschen ärgerlich, dass das kaum erklärt wurde und wir jetzt eine Aufgabe dazu bekommen. Das was auf den Folien steht, reicht bei weitem nicht fürs Verständnis und soweit ich mich erinnern kann wurde das in der VO auch nicht so toll erklärt. Oder hätte ich einfach mehr schlafen sollen?)

    Von denen gewinnen 2 und 4 verlieren. Insofern ist meine Gewinnwahrscheinlichkeit 1 : 2.


    Du meinst wohl 2/6=1/3?
    Ja ich glaub das müsste eigentlich stimmen, ich hoffe nur diese watscheneinfache Erklärung wird akzeptiert ;)