Fachrat Informatik - Forum

doch ist erlaubt

das habe ich mich auch schon gefragt. man kann ja ein modell mit 0en und 1en angeben, das möglichst simpel ist.
ich glaube das ist auch nötig, denn wenn man sich klausuraufgabe 3 anschaut, dann braucht man zu viel zeit für ne kompliziertere lösung.

Laut Herrn Dr. Holz ist das egal. Die Baumstruktur ist sogar aus korrekturtechnischen Gründen bevorzugt.

Quoted

Original von Prof_NARF
Laut Herrn Dr. Holz ist das egal. Die Baumstruktur ist sogar aus korrekturtechnischen Gründen bevorzugt.

genau, sofern alles korrekt gerechnet ist, natürlich

Quoted

Original von NullAhnung
Das ist schonmal gut. Kann ich bei dem Logikprogramm auch Klauseln doppelt benutzen?

Da es sich hierbei um Resolution handelt, gilt das in diesem Thread Gesagte.

Quoted

Wie gebe ich s und t an?

Was sind s und t?

Quoted

Original von NullAhnung
Das eben weiß ich ja nicht so genau. Da steht: Man gebe Terme s und t an, so dass die Formel P(f(s),t) n R(s, f(t)) erfüllt ist

Im Grund geht es ja darum, eine konkrete erfüllbare Formel anzugeben (dazu in diesem Falle das s und t). Eine solche Formel ergibt sich aus den angewendeten Substitutionen im Verlauf der Resolution, in der Vorlesung oder Übung wurde dazu garantiert ein Beispiel gemacht.

Nachdem du gezeigt hast das F aus Gamma beweisbar ist, musst du nur die Veränderung der Variablen durch das sub betrachten. D.h. du wendest das sub auf die Variablen in der Formel F an und siehst daraus, welche Struktur die Terme s und t haben müssen.
Beispiel:
Man soll zeigen, dass F = exists x exists y P(x,y) aus Gamma beweisbar ist. Man wendet das Logikprogramm an und erhält ein sub = sub1 ... subn, n>=1. Man zeigt das über die Resolutionen, dass Gamma |- F sub.
Ferner gebe man Terme s und t an, so dass die Formel P(s,t) aus Gamma beweisbar ist. Man betrachtet nun P(x,y) sub. Angenommen dies sei
P(g(f(c)),g(c)). Nun weiß man, dass s=g(f(c)) und t=g(c). Fertig.
Ich hoffe das Beispiel hat Licht ins Dunkel gebracht.