Resolution
Die Resolution ist der wichtigste Schritt bei der Ausführung von Logikprogrammen (siehe Hornklausel).
Die Funktion compile übersetzt ein Logikprogramm von der Listendarstellung in die Instanzdarstellung und indexiert gewöhnliche Atome mit passenden Hornklauseln.
(defproc compile (source)
(let
((program (to-program source)))
(progn
(freeze program)
(prepare-resolution program program)
program)))
Das Indexieren wird von den Methoden prepare-resolution erledigt.
(defmethod prepare-resolution ((this formula) (program normal-program))
t
nil)
(defmethod prepare-resolution ((this negative-literal) (program normal-program))
t
(progn
(prepare-resolution (. this atom) program)
(.= this program program)
(freeze this)))
(defmethod prepare-resolution ((this ordinary-atom) (program normal-program))
t
(progn
(.= this matching-clauses
(select-if
(lambda (clause)
(aand
(unify-copies this (get-antecedent clause) (make-context) (make-lock) (gensym) (gensym))
(progn (undo it) t)))
(get-formulas program)))
(.= this matching-clause-count (length (. this matching-clauses)))
(freeze this)))
(defmethod prepare-resolution ((this conjunction) (program normal-program))
t
(map-with
(curry (prepare-resolution _ program))
(get-formulas this)))
(defmethod prepare-resolution ((this general-horn-clause) (program normal-program))
t
(map-with
(curry (prepare-resolution _ program))
(get-consequents this)))
Die Methode solve übersetzt ein Ziel von der Listendarstellung in die Instanzdarstellung, indexiert die gewöhnlichen Atome und startet dann den Beweisprozess.
(defmethod solve (source (program normal-program))
(list? source)
(let
((this (to-literal-conjunction source)))
(progn
(prepare-resolution this program)
(solve this program))))
Der Beweisprozess hält alle gleichzeitig verfolgten Zweige in einer Prioritätswarteschlange.
(defmethod solve ((this literal-conjunction) (program normal-program))
t
(let
((agenda (new pairing-heap
(lambda (pair-1 pair-2)
(<
(length (get-formulas (first pair-1)))
(length (get-formulas (first pair-2)))))
(list (list this this)))))
(aand
(search-shortest-first agenda)
(to-list it))))
Die Zweige mit den wenigsten verbleibenden Literalen befinden sich am Anfang der Schlange, denn sie sind die vielversprechendsten. Diese Zweige werden zuerst weiterverfolgt.
(defmethod search-shortest-first ((agenda pairing-heap))
t
(let
((pair nil))
(loop
(when (is-empty? agenda)
(return nil))
(setq pair (head agenda))
(when (is-solved? pair)
(return (second pair)))
(setq agenda (tail agenda))
(dolist (successor (get-successors pair))
(setq agenda (insert-into agenda successor))))))
Ein Zweig ist gelöst, wenn kein Literal verblieben ist.
(defproc is-solved? (pair)
(null? (get-formulas (first pair))))
Die Funktion get-successors selektiert ein Literal und wendet darauf die Resolution an. Nicht immer sind alle Literale selektierbar. Wenn mehrere auswählbar sind, dann wird eine Heuristik angewendet. Literale, in denen alle Variablen einen Wert haben, werden bevorzugt, ebenso gewöhnliche Atome, die auf möglichst wenige Hornklauseln passen.
(defproc get-successors (pair)
(let
((todos (first pair))
(goal (second pair)))
(aand
(select-literal todos)
(resolve it (without-literal todos it) goal))))
(defmethod select-literal ((todos literal-conjunction))
t
(let
((literals (select-if is-selectable? (get-formulas todos))))
(let
((ground-literals (select-if is-ground? literals)))
(if
(null? ground-literals)
(and literals (first literals))
(first
(sort
ground-literals
(lambda (literal-1 literal-2)
(less?
(get-branch-count literal-1)
(get-branch-count literal-2)))))))))
Gewöhnliche Literale können immer selektiert werden.
(defmethod is-selectable? ((this ordinary-atom))
t
t)
Andere Literale können nur selektiert werden, wenn sie keine Variablen ohne Wert enthalten.
(defmethod is-selectable? ((this applicative-atom))
t
(is-ground? this))
(defmethod is-selectable? ((this negative-literal))
t
(is-ground? this))
(defmethod is-ground? ((this ordinary-atom))
t
(is-ground? (. this structure)))
(defmethod is-ground? ((this applicative-atom))
t
(every? is-ground? (. this variables)))
(defmethod is-ground? ((this negative-literal))
t
(is-ground? (. this atom)))
(defmethod is-ground? ((this constant))
t
t)
(defmethod is-ground? ((this variable))
t
(aand
(. this value)
(is-ground? it)))
(defmethod is-ground? ((this structure))
t
(with-slots-read-only (head tail) this
(and
(is-ground? head)
(is-ground? tail))))
(defmethod is-ground? ((this term-list))
t
(every? is-ground? (. this elements)))
Die Methode get-branch-count wird für die Auswahlheuristik benötigt.
(defmethod get-branch-count ((this ordinary-atom))
t
(. this matching-clause-count))
(defmethod get-branch-count ((this applicative-atom))
t
0)
(defmethod get-branch-count ((this negative-literal))
t
(get-branch-count (. this atom)))
Die Methode without-literal entfernt ein Literal aus einer Konjunktion.
(defmethod without-literal ((todos literal-conjunction) (a-literal literal))
t
(new literal-conjunction
(remove a-literal (get-formulas todos))))
Für gewöhnliche Atome liefert der Resolutionsschritt einen Beweiszweig für jede passende Hornklausel.
(defmethod resolve ((this ordinary-atom) (todos literal-conjunction) (goal literal-conjunction))
t
(remove nil
(map-with
(lambda (clause)
(let
((context (make-context))
(context-lock (make-lock))
(namespace-1 (gensym))
(namespace-2 (gensym)))
(if
(unify-copies this (get-antecedent clause) context context-lock namespace-1 namespace-2)
(list
(new literal-conjunction
(append
(copy (get-formulas todos) context context-lock namespace-1)
(copy (get-consequents clause) context context-lock namespace-2)))
(copy goal context context-lock namespace-1))
nil)))
(. this matching-clauses))))
Ein Test-Atom liefert den aktuellen Zweig zurück, wenn der Test erfolgreich ist. Ansonsten wird der Zweig nicht weiterverfolgt.
(defmethod resolve ((this test-atom) (todos literal-conjunction) (goal literal-conjunction))
t
(with-slots-read-only (variables function) this
(if
(apply function (map-with value-of variables))
(list (list todos goal))
nil)))
Ein Assignment-Atom versucht, den berechneten Wert zuzuweisen. Nur wenn das erfolgreich ist, wird der aktuelle Zweig weiterverfolgt.
(defmethod resolve ((this assignment-atom) (todos literal-conjunction) (goal literal-conjunction))
t
(with-slots-read-only (left-hand-side variables function) this
(let
((right-hand-value (new constant (apply function (map-with value-of variables))))
(context (make-context))
(context-lock (make-lock))
(namespace (gensym)))
(if
(unify-copies left-hand-side right-hand-value context context-lock namespace nil)
(list
(list
(copy todos context context-lock namespace)
(copy goal context context-lock namespace)))
nil))))
Für ein negatives Literal wird durch einen rekursiven Aufruf von solve versucht, das enthaltene Atom zu beweisen. Nur wenn das fehlschlägt, wird der aktuelle Zweig weiterverfolgt.
(defmethod resolve ((this negative-literal) (todos literal-conjunction) (goal literal-conjunction))
t
(with-slots-read-only (atom program) this
(if
(solve (new literal-conjunction (list atom)) program)
nil
(list (list todos goal)))))
Die Funktion compile übersetzt ein Logikprogramm von der Listendarstellung in die Instanzdarstellung und indexiert gewöhnliche Atome mit passenden Hornklauseln.
(defproc compile (source)
(let
((program (to-program source)))
(progn
(freeze program)
(prepare-resolution program program)
program)))
Das Indexieren wird von den Methoden prepare-resolution erledigt.
(defmethod prepare-resolution ((this formula) (program normal-program))
t
nil)
(defmethod prepare-resolution ((this negative-literal) (program normal-program))
t
(progn
(prepare-resolution (. this atom) program)
(.= this program program)
(freeze this)))
(defmethod prepare-resolution ((this ordinary-atom) (program normal-program))
t
(progn
(.= this matching-clauses
(select-if
(lambda (clause)
(aand
(unify-copies this (get-antecedent clause) (make-context) (make-lock) (gensym) (gensym))
(progn (undo it) t)))
(get-formulas program)))
(.= this matching-clause-count (length (. this matching-clauses)))
(freeze this)))
(defmethod prepare-resolution ((this conjunction) (program normal-program))
t
(map-with
(curry (prepare-resolution _ program))
(get-formulas this)))
(defmethod prepare-resolution ((this general-horn-clause) (program normal-program))
t
(map-with
(curry (prepare-resolution _ program))
(get-consequents this)))
Die Methode solve übersetzt ein Ziel von der Listendarstellung in die Instanzdarstellung, indexiert die gewöhnlichen Atome und startet dann den Beweisprozess.
(defmethod solve (source (program normal-program))
(list? source)
(let
((this (to-literal-conjunction source)))
(progn
(prepare-resolution this program)
(solve this program))))
Der Beweisprozess hält alle gleichzeitig verfolgten Zweige in einer Prioritätswarteschlange.
(defmethod solve ((this literal-conjunction) (program normal-program))
t
(let
((agenda (new pairing-heap
(lambda (pair-1 pair-2)
(<
(length (get-formulas (first pair-1)))
(length (get-formulas (first pair-2)))))
(list (list this this)))))
(aand
(search-shortest-first agenda)
(to-list it))))
Die Zweige mit den wenigsten verbleibenden Literalen befinden sich am Anfang der Schlange, denn sie sind die vielversprechendsten. Diese Zweige werden zuerst weiterverfolgt.
(defmethod search-shortest-first ((agenda pairing-heap))
t
(let
((pair nil))
(loop
(when (is-empty? agenda)
(return nil))
(setq pair (head agenda))
(when (is-solved? pair)
(return (second pair)))
(setq agenda (tail agenda))
(dolist (successor (get-successors pair))
(setq agenda (insert-into agenda successor))))))
Ein Zweig ist gelöst, wenn kein Literal verblieben ist.
(defproc is-solved? (pair)
(null? (get-formulas (first pair))))
Die Funktion get-successors selektiert ein Literal und wendet darauf die Resolution an. Nicht immer sind alle Literale selektierbar. Wenn mehrere auswählbar sind, dann wird eine Heuristik angewendet. Literale, in denen alle Variablen einen Wert haben, werden bevorzugt, ebenso gewöhnliche Atome, die auf möglichst wenige Hornklauseln passen.
(defproc get-successors (pair)
(let
((todos (first pair))
(goal (second pair)))
(aand
(select-literal todos)
(resolve it (without-literal todos it) goal))))
(defmethod select-literal ((todos literal-conjunction))
t
(let
((literals (select-if is-selectable? (get-formulas todos))))
(let
((ground-literals (select-if is-ground? literals)))
(if
(null? ground-literals)
(and literals (first literals))
(first
(sort
ground-literals
(lambda (literal-1 literal-2)
(less?
(get-branch-count literal-1)
(get-branch-count literal-2)))))))))
Gewöhnliche Literale können immer selektiert werden.
(defmethod is-selectable? ((this ordinary-atom))
t
t)
Andere Literale können nur selektiert werden, wenn sie keine Variablen ohne Wert enthalten.
(defmethod is-selectable? ((this applicative-atom))
t
(is-ground? this))
(defmethod is-selectable? ((this negative-literal))
t
(is-ground? this))
(defmethod is-ground? ((this ordinary-atom))
t
(is-ground? (. this structure)))
(defmethod is-ground? ((this applicative-atom))
t
(every? is-ground? (. this variables)))
(defmethod is-ground? ((this negative-literal))
t
(is-ground? (. this atom)))
(defmethod is-ground? ((this constant))
t
t)
(defmethod is-ground? ((this variable))
t
(aand
(. this value)
(is-ground? it)))
(defmethod is-ground? ((this structure))
t
(with-slots-read-only (head tail) this
(and
(is-ground? head)
(is-ground? tail))))
(defmethod is-ground? ((this term-list))
t
(every? is-ground? (. this elements)))
Die Methode get-branch-count wird für die Auswahlheuristik benötigt.
(defmethod get-branch-count ((this ordinary-atom))
t
(. this matching-clause-count))
(defmethod get-branch-count ((this applicative-atom))
t
0)
(defmethod get-branch-count ((this negative-literal))
t
(get-branch-count (. this atom)))
Die Methode without-literal entfernt ein Literal aus einer Konjunktion.
(defmethod without-literal ((todos literal-conjunction) (a-literal literal))
t
(new literal-conjunction
(remove a-literal (get-formulas todos))))
Für gewöhnliche Atome liefert der Resolutionsschritt einen Beweiszweig für jede passende Hornklausel.
(defmethod resolve ((this ordinary-atom) (todos literal-conjunction) (goal literal-conjunction))
t
(remove nil
(map-with
(lambda (clause)
(let
((context (make-context))
(context-lock (make-lock))
(namespace-1 (gensym))
(namespace-2 (gensym)))
(if
(unify-copies this (get-antecedent clause) context context-lock namespace-1 namespace-2)
(list
(new literal-conjunction
(append
(copy (get-formulas todos) context context-lock namespace-1)
(copy (get-consequents clause) context context-lock namespace-2)))
(copy goal context context-lock namespace-1))
nil)))
(. this matching-clauses))))
Ein Test-Atom liefert den aktuellen Zweig zurück, wenn der Test erfolgreich ist. Ansonsten wird der Zweig nicht weiterverfolgt.
(defmethod resolve ((this test-atom) (todos literal-conjunction) (goal literal-conjunction))
t
(with-slots-read-only (variables function) this
(if
(apply function (map-with value-of variables))
(list (list todos goal))
nil)))
Ein Assignment-Atom versucht, den berechneten Wert zuzuweisen. Nur wenn das erfolgreich ist, wird der aktuelle Zweig weiterverfolgt.
(defmethod resolve ((this assignment-atom) (todos literal-conjunction) (goal literal-conjunction))
t
(with-slots-read-only (left-hand-side variables function) this
(let
((right-hand-value (new constant (apply function (map-with value-of variables))))
(context (make-context))
(context-lock (make-lock))
(namespace (gensym)))
(if
(unify-copies left-hand-side right-hand-value context context-lock namespace nil)
(list
(list
(copy todos context context-lock namespace)
(copy goal context context-lock namespace)))
nil))))
Für ein negatives Literal wird durch einen rekursiven Aufruf von solve versucht, das enthaltene Atom zu beweisen. Nur wenn das fehlschlägt, wird der aktuelle Zweig weiterverfolgt.
(defmethod resolve ((this negative-literal) (todos literal-conjunction) (goal literal-conjunction))
t
(with-slots-read-only (atom program) this
(if
(solve (new literal-conjunction (list atom)) program)
nil
(list (list todos goal)))))