Formel
Die Klassen für Formeln bilden die folgende Hierarchie:
- Formula
- Clause
- GeneralHornClause
- Literal (Copyable)
- NegativeLiteral
- Atom
- OrdinaryAtom (Unifiable)
- ApplicativeAtom
- EvalAtom
- AssignmentAtom
- ConjunctionOrDisjunction
- Conjunction
- NormalProgram
- LiteralConjunction (Copyable)
- Disjunction
- OrdinaryAtomDisjunction
Das wird durch diese Anweisungen erreicht.
(defclass formula ())
(defclass clause (formula))
(defclass general-horn-clause (clause))
(defclass literal (formula copyable))
(defclass negative-literal (literal))
(defclass atom (literal))
(defclass ordinary-atom (atom unifiable))
(defclass applicative-atom (atom))
(defclass test-atom (applicative-atom))
(defclass assignment-atom (applicative-atom))
(defclass conjunction-or-disjunction (formula))
(defclass conjunction (conjunction-or-disjunction))
(defclass normal-program (conjunction))
(defclass literal-conjunction (conjunction copyable))
(defclass disjunction (conjunction-or-disjunction))
(defclass ordinary-atom-disjunction (disjunction))
Eine Konjunktion oder Disjunktion enthält eine Liste von Formeln.
(defmethod initialize ((this conjunction-or-disjunction) formulas)
(every-is-a? formula formulas)
(progn
(.= this formulas formulas)
this))
Eine Klausel besteht aus einer Disjunktion von gewöhnlichen Atomen und einer Konjunktion von Literalen.
(defmethod initialize ((this clause) (antecedents ordinary-atom-disjunction) (consequents literal-conjunction))
t
(progn
(.= this antecedents antecedents)
(.= this consequents consequents)
(freeze this)))
Eine Hornklausel ist eine Klausel, die nur ein gewöhnliches Atom in ihrer Disjunktion enthält.
(defmethod initialize ((this general-horn-clause) (antecedent ordinary-atom) (consequents literal-conjunction))
t
(initialize
this
(new ordinary-atom-disjunction (list antecedent))
consequents))
Ein negatives Literal enthält ein Atom.
(defmethod initialize ((this negative-literal) (an-atom atom))
t
(progn
(.= this atom an-atom)
this))
Ein Atom enthält eine Struktur (siehe Term).
(defmethod initialize ((this ordinary-atom) (a-structure structure))
t
(progn
(.= this structure a-structure)
this))
Ein Test-Atom enthält eine Liste von Variablen und eine Funktion.
(defmethod initialize ((this test-atom) variables function)
(every-is-a? constant-or-variable variables)
(progn
(.= this variables variables)
(.= this function function)
(freeze this)))
Ein Assignment-Atom enthält eine Konstante oder eine Variable, eine Liste von Variablen und eine Funktion.
(defmethod initialize ((this assignment-atom) (left-hand-side constant-or-variable) variables function)
(every-is-a? constant-or-variable variables)
(progn
(.= this left-hand-side left-hand-side)
(.= this variables variables)
(.= this function function)
(freeze this)))
Die Accessor-Methoden greifen auf diverse Bestandteile der Instanzen der oben definierten Klassen zu.
(defmethod get-formulas ((this conjunction-or-disjunction))
t
(. this formulas))
(defmethod get-consequents ((this clause))
t
(get-formulas (. this consequents)))
(defmethod get-antecedents ((this clause))
t
(get-formulas (. this antecedents)))
(defmethod get-antecedent ((this general-horn-clause))
t
(first (get-antecedents this)))
Die folgenden Funktionen wandeln die Listendarstellung von Formeln in die Instanzdarstellung um.
(defproc to-program (source)
(new normal-program
(map-with to-clause source)))
(defproc to-clause (source)
(if
(and
(= (length source) 3)
(= (first source) (quote implied)))
(new general-horn-clause
(to-ordinary-atom (second source))
(to-literal-conjunction (third source)))
(throw (quote error) "clause must start with implied and have two more elements")))
(defproc to-ordinary-atom (source)
(new ordinary-atom (to-structure source)))
(defproc to-literal-conjunction (source)
(new literal-conjunction
(cond
((= source t) nil)
((= (first source) (quote and)) (map-with to-literal (rest source)))
(t (list (to-literal source))))))
(defproc to-literal (source)
(if
(= (first source) (quote not))
(to-negative-literal source)
(to-atom source))))
(defproc to-negative-literal (source)
(new negative-literal
(to-atom (second source))))
(defproc to-atom (source)
(let
((discriminator (first source)))
(cond
((= discriminator (quote true?)) (to-test-atom source))
((= discriminator (quote is)) (to-assignment-atom source))
(t (to-ordinary-atom source)))))
(defproc to-test-atom (source)
(let
((body (second source)))
(let
((names (find-variable-names body nil)))
(new test-atom
(map-with (lambda (name) (new variable name nil)) names)
(make-lambda names body)))))
(defproc find-variable-names (expr names)
(cond
((null? expr) names)
((list? expr) (find-variable-names (rest expr) (find-variable-names (first expr) names)))
((is-variable-name? expr) (cons expr names))
(t names)))
(defproc make-lambda (names body)
((mlambda args (list lambda names body))))
(defproc to-assignment-atom (source)
(let
((left-hand-side (second source))
(right-hand-side (third source)))
(let
((names (find-variable-names right-hand-side nil)))
(new assignment-atom
(to-constant-or-variable left-hand-side)
(map-with (lambda (name) (new variable name nil)) names)
(make-lambda names right-hand-side)))))
Die Methoden to-list wandeln die Instanzdarstellung von ausgewählten Formeln in die Listendarstellung um.
(defmethod to-list ((this literal-conjunction))
t
(with-slots-read-only (formulas) this
(cond
((null? formulas) t)
((single? formulas) (to-list (first formulas)))
(t (cons (quote and) (map-with to-list formulas))))))
(defmethod to-list ((this ordinary-atom))
t
(to-list (. this structure)))
- Formula
- Clause
- GeneralHornClause
- Literal (Copyable)
- NegativeLiteral
- Atom
- OrdinaryAtom (Unifiable)
- ApplicativeAtom
- EvalAtom
- AssignmentAtom
- ConjunctionOrDisjunction
- Conjunction
- NormalProgram
- LiteralConjunction (Copyable)
- Disjunction
- OrdinaryAtomDisjunction
Das wird durch diese Anweisungen erreicht.
(defclass formula ())
(defclass clause (formula))
(defclass general-horn-clause (clause))
(defclass literal (formula copyable))
(defclass negative-literal (literal))
(defclass atom (literal))
(defclass ordinary-atom (atom unifiable))
(defclass applicative-atom (atom))
(defclass test-atom (applicative-atom))
(defclass assignment-atom (applicative-atom))
(defclass conjunction-or-disjunction (formula))
(defclass conjunction (conjunction-or-disjunction))
(defclass normal-program (conjunction))
(defclass literal-conjunction (conjunction copyable))
(defclass disjunction (conjunction-or-disjunction))
(defclass ordinary-atom-disjunction (disjunction))
Eine Konjunktion oder Disjunktion enthält eine Liste von Formeln.
(defmethod initialize ((this conjunction-or-disjunction) formulas)
(every-is-a? formula formulas)
(progn
(.= this formulas formulas)
this))
Eine Klausel besteht aus einer Disjunktion von gewöhnlichen Atomen und einer Konjunktion von Literalen.
(defmethod initialize ((this clause) (antecedents ordinary-atom-disjunction) (consequents literal-conjunction))
t
(progn
(.= this antecedents antecedents)
(.= this consequents consequents)
(freeze this)))
Eine Hornklausel ist eine Klausel, die nur ein gewöhnliches Atom in ihrer Disjunktion enthält.
(defmethod initialize ((this general-horn-clause) (antecedent ordinary-atom) (consequents literal-conjunction))
t
(initialize
this
(new ordinary-atom-disjunction (list antecedent))
consequents))
Ein negatives Literal enthält ein Atom.
(defmethod initialize ((this negative-literal) (an-atom atom))
t
(progn
(.= this atom an-atom)
this))
Ein Atom enthält eine Struktur (siehe Term).
(defmethod initialize ((this ordinary-atom) (a-structure structure))
t
(progn
(.= this structure a-structure)
this))
Ein Test-Atom enthält eine Liste von Variablen und eine Funktion.
(defmethod initialize ((this test-atom) variables function)
(every-is-a? constant-or-variable variables)
(progn
(.= this variables variables)
(.= this function function)
(freeze this)))
Ein Assignment-Atom enthält eine Konstante oder eine Variable, eine Liste von Variablen und eine Funktion.
(defmethod initialize ((this assignment-atom) (left-hand-side constant-or-variable) variables function)
(every-is-a? constant-or-variable variables)
(progn
(.= this left-hand-side left-hand-side)
(.= this variables variables)
(.= this function function)
(freeze this)))
Die Accessor-Methoden greifen auf diverse Bestandteile der Instanzen der oben definierten Klassen zu.
(defmethod get-formulas ((this conjunction-or-disjunction))
t
(. this formulas))
(defmethod get-consequents ((this clause))
t
(get-formulas (. this consequents)))
(defmethod get-antecedents ((this clause))
t
(get-formulas (. this antecedents)))
(defmethod get-antecedent ((this general-horn-clause))
t
(first (get-antecedents this)))
Die folgenden Funktionen wandeln die Listendarstellung von Formeln in die Instanzdarstellung um.
(defproc to-program (source)
(new normal-program
(map-with to-clause source)))
(defproc to-clause (source)
(if
(and
(= (length source) 3)
(= (first source) (quote implied)))
(new general-horn-clause
(to-ordinary-atom (second source))
(to-literal-conjunction (third source)))
(throw (quote error) "clause must start with implied and have two more elements")))
(defproc to-ordinary-atom (source)
(new ordinary-atom (to-structure source)))
(defproc to-literal-conjunction (source)
(new literal-conjunction
(cond
((= source t) nil)
((= (first source) (quote and)) (map-with to-literal (rest source)))
(t (list (to-literal source))))))
(defproc to-literal (source)
(if
(= (first source) (quote not))
(to-negative-literal source)
(to-atom source))))
(defproc to-negative-literal (source)
(new negative-literal
(to-atom (second source))))
(defproc to-atom (source)
(let
((discriminator (first source)))
(cond
((= discriminator (quote true?)) (to-test-atom source))
((= discriminator (quote is)) (to-assignment-atom source))
(t (to-ordinary-atom source)))))
(defproc to-test-atom (source)
(let
((body (second source)))
(let
((names (find-variable-names body nil)))
(new test-atom
(map-with (lambda (name) (new variable name nil)) names)
(make-lambda names body)))))
(defproc find-variable-names (expr names)
(cond
((null? expr) names)
((list? expr) (find-variable-names (rest expr) (find-variable-names (first expr) names)))
((is-variable-name? expr) (cons expr names))
(t names)))
(defproc make-lambda (names body)
((mlambda args (list lambda names body))))
(defproc to-assignment-atom (source)
(let
((left-hand-side (second source))
(right-hand-side (third source)))
(let
((names (find-variable-names right-hand-side nil)))
(new assignment-atom
(to-constant-or-variable left-hand-side)
(map-with (lambda (name) (new variable name nil)) names)
(make-lambda names right-hand-side)))))
Die Methoden to-list wandeln die Instanzdarstellung von ausgewählten Formeln in die Listendarstellung um.
(defmethod to-list ((this literal-conjunction))
t
(with-slots-read-only (formulas) this
(cond
((null? formulas) t)
((single? formulas) (to-list (first formulas)))
(t (cons (quote and) (map-with to-list formulas))))))
(defmethod to-list ((this ordinary-atom))
t
(to-list (. this structure)))