Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Moin. Ich hab auch noch eine Verstaendnisfrage zum Blatt, speziell Aufgabe 7.4.
Wie darf ich “given by ProLog facts like the following” verstehen? Welche atomaren Funktionen duerfen vorkommen? Nur love/2 und hate/2 oder noch andere?
Ausserdem: Wieviele Models sollen es werden? Und was sollen sie jeweils koennen?
Ich hätte noch eine Frage zu 7.7 [quote]
(Revise the evaluator to a tableau theorem prover/model generation proce- 15pt
dure for closed formulae that only contain the connectives & and ~.)
[/quote]
Wie ist das revise hier gemeint? Soll unser neuer evaluator die Arbeitsweise von tableau kopieren, also die Regeln anwenden, bis alle Zweige atomar sind? Oder soll er funktionieren wie der evaluator aus Aufgabe 7.5 mit dem Unterschied, dass er nur die Junktoren & und ~ verwenden darf?
Da dürfen beliebige auftreten (daher ja das „pred“-Prädikat) - eure methoden sollten also alle noch funktionieren wenn ich jetzt ein neues prädikat einführe. Ihr dürft natürlich auch selber beliebige definieren, wenn ihr Modelle haben wollt in denen es mehr als nur „love“ und „hate“ gibt
Uff, sagen wir 3?
Sie sollten sich voneinander unterscheiden Und sagen wir mal mindestens zwei verschiedene atomare formeln beinhalten, sonst wird’s langweilig
Der evaluator sollte prüfen ob eine formel in einem bestimmten Modell gilt - der nimmt also ein modell und eine formel. Die Revision sollte nur eine Formel nehmen und entweder beweisen dass die formel allgemeingültig ist (true zurückgeben) oder falls sie falsch ist ein gegenmodell konstruieren. In letzterem sollt ihr den Tableau-Kalkül benutzen, in ersterem dürft ihr beliebiges machen.
Danke fuer die schnelle Antwort. Soll unsere Methode also, wenn die Formel nicht allgemeingueltig ist, das Gegenmodell auch zurueckgeben oder reicht es aus, den Tableau-Kalkuel zu verwenden und dann false zurueck zu geben?
Wenn wir das Gegenmodell zurueckgeben sollen, muesste die Methode ja mindestens zwei Parameter (Formel, Gegenmodell) haben, kann also nicht nur eine Formel nehmen…
touché Nee, der sollte schon das Modell generieren und in irgendeiner weise dem nutzer mitteilen - der vorteil von tableau ist ja gerade dass es bei gegenbeweisen eben automatisch modelle generiert; reicht aber natürlich wenn er die nur printed bevor er false zurück gibt
Nee, der sollte schon das Modell generieren und in irgendeiner weise dem nutzer mitteilen - der vorteil von tableau ist ja gerade dass es bei gegenbeweisen eben automatisch modelle generiert; reicht aber natürlich wenn er die nur printed bevor er false zurück gibt