Resolution < Prädikatenlogik < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
hallo,
ich habe hier mal eine Aufgabe zur Resolutionsmethode angehängt, bei der ich die Lösung nicht so ganz verstehe.
Aufgabe
Eigentlich ist es nur eine Kleinigkeit, es geht um die Erstellung des Baums ganz unten. Dass man die Variablen beliebig benennen darf, solange man innerhalb einer Klausel konsistent bleibt, ist mir schonmal klar.
Aber wieso darf man dann noch mit c und/oder gc ersetzen (was anscheinend Konstanten und eine einstellige Funktion g sein sollen) und was für einen Sinn macht das?
|
|
|
|
Status: |
(Mitteilung) Reaktion unnötig | Datum: | 16:20 Do 04.10.2007 | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|