Projektarbeit im Fach ”Logisches Programmieren“ Konjunktive Normalform und Resolution in der

Aussagen- und Prädikatenlogik

Matthias Köppe^{∗}

11. Mai 1997

Zusammenfassung

In der Programmiersprache Scheme wurde ein Programm entwickelt, das Formeln der Aussagen- und Prädikatenlogik in die Konjunktive Normalform überführen kann. Für die Aussagenlogik wurde ein Entscheidungsverfahren implementiert, welches mittels Resolution bestimmt, ob eine Formel ein Satz eines Axiomensystems ist. Für die Prädikatenlogik wurde ein Semi-Entschei-dungsverfahren mit Breitensuche implementiert, welches mittels Unifikation und Resolution Sätze eines Axiomensystems beweisen kann; ein einfaches Antwortsystem kann Fragen semi-beantworten. Ein Modul zur leichteren Eingabe von Formeln erlaubt eine relaxierte Verwendung von Klammern und identifiziert Variablensymbole über eine Namenskonvention. Es stehen Funktionen bereit, die Formeln in eine leicht lesbare Textform bzw. in Code für das Satzsystem TEX überführen.

1 Scheme-Modul für Aussagenlogik

Das folgende Scheme-Modul (logic.scm) beinhaltet die Definition aussagenlogischer Ausdrücke als abstrakte Datentypen, die Bereitstellung der externen Repräsentationen, die Überführung eines Ausdrucks in die Konjunktive Normalform und die aussagenlogische Resolution.

Hilfsmittel

(define (lambda-and . x)

Ein ‘and’, das keine ‘special form’ ist.

(or (null? x)
 (and (car x) (apply lambda-and (cdr x)))))
(define (lambda-or . x)

Ein ‘or’, das keine ‘special form’ ist.

(and (not (null? x))
  (or (car x) (apply lambda-or (cdr x)))))
(define (remove-if predicate? x)

∗mkoeppe@csmd.cs.uni-magdeburg.de

Entfernt alle Elemente der Liste, für die das Prädikat erfüllt ist.

(cond ((null? x) x)
((predicate? (car x)) (remove-if predicate? (cdr x)))
(else (cons (car x) (remove-if predicate? (cdr x))))))
(define (first-that pred? l)

Ermittelt eine Teilliste, deren erstes Element das Prädikat erfüllt.

(cond ((null? l) l)
((pred? (car l)) l)
(else (first-that pred? (cdr l)))))
(define (make-set elem-list)

Läßt jedes Element nur einmal auftreten.

(cond ((null? elem-list) elem-list)
(else
 (cons (car elem-list)
       (make-set
        (remove-if (lambda (x)
                     (equal? x (car elem-list)))
                   (cdr elem-list)))))))
(define (set-cons elem set)

Fügt das Element nur hinzu, wenn es nicht schon da ist.

(if (member elem set)
set
(cons elem set)))
(define (set-append . set-list)

Fügt Elemente nur hinzu, wenn sie nicht schon da sind.

(set-append-aux set-list '()))
(define (set-append-aux set-list result)
(cond ((null? set-list) result)
((null? (car set-list))
 (set-append-aux (cdr set-list) result))
((member (caar set-list) result)
 (set-append-aux (cons (cdar set-list) (cdr set-list))
                 result))
(else (set-append-aux (cons (cdar set-list) (cdr set-list))
                      (cons (caar set-list) result)))))
(define (set-minus set1 set2)

Entfernt alle Elemente der zweiten Menge aus der ersten Menge und gibt das Ergebnis zurück.

(remove-if (lambda (x) (member x set2)) set1))
(define (atom->string atom)
(cond ((number? atom) (number->string atom))
((symbol? atom) (symbol->string atom))
((string? atom) atom)
((char? atom) (string atom))))

Interne Repräsentation aussagenlogischer Formeln

Konstruktoren

Es werden keine Vereinfachungen gemacht, damit auch beliebig unvereinfachte Ausdrücke repräsentiert werden können.

(define (make-negation expr) (list 'not expr))
(define (make-conjunction . exprs) (cons 'and exprs))
(define (make-disjunction . exprs) (cons 'or exprs))
(define (make-implication expra exprb) (list 'imply expra exprb))
(define (make-equivalence expra exprb) (list 'equiv expra exprb))
(define (make-xor expra exprb) (list 'xor expra exprb))

Prädikate

(define (negation? expr) (and (pair? expr)
                              (eq? 'not (car expr))))
(define (conjunction? expr) (and (pair? expr)
                                 (eq? 'and (car expr))))
(define (disjunction? expr) (and (pair? expr)
                                 (eq? 'or (car expr))))
(define (implication? expr) (and (pair? expr)
                                 (eq? 'imply (car expr))))
(define (equivalence? expr) (and (pair? expr)
                                 (eq? 'equiv (car expr))))
(define (xor? expr) (and (pair? expr)
                         (eq? 'xor (car expr))))

Diese Definition versagt, sobald wir prädikatenlogische Ausdrücke als aussagenlogische Atome verwenden wollen.

;(define logical-atom? atom?)

Wir verwenden deshalb diese Definition:

(define (logical-atom? expr)
  (not (or (negation? expr)
           (conjunction? expr)
           (disjunction? expr)
           (implication? expr)
           (equivalence? expr)
           (xor? expr))))

Selektoren für die Teilausdrücke von ‘implication’, ‘equivalence’, ‘xor’

(define left-subexpr cadr)
(define right-subexpr caddr)

Selektor für die Liste der in ‘conjunction’ oder ‘disjunction’ gebundenen Ausdrücke

(define subexpr-list cdr)

Selektor für den Teilausdruck einer ‘negation’

(define subexpr cadr)

Hilfsmittel für externe Repräsentationen

Entartete (null- oder einstellige) Konjunktionen und Disjunktionen müssen anders geklammert werden als gewöhnliche. Dazu verwenden wir diese Prädikate:

(define (multiop? expr)
  (or (conjunction? expr)
      (disjunction? expr)))
(define (void-multiop? expr)
  (and (multiop? expr)
       (null? (subexpr-list expr))))
(define (unary-multiop? expr)
  (and (multiop? expr)
       (pair? (subexpr-list expr))
       (null? (cdr (subexpr-list expr)))))
(define (operator-priority-logic expr)

Liefert die Priorität (Stärke der Bindung) des Verknüpfungssymboles in dem Ausdruck.

  (cond ((negation? expr) 10)
        ((void-multiop? expr) 11)
        ((unary-multiop? expr) 10)

(9 ist reserviert für Quantoren)

        ((conjunction? expr) 8)
        ((disjunction? expr) 6)
        ((implication? expr) 4)
        ((equivalence? expr) 4)
        ((xor? expr) 4)
        (else 12)))
(define operator-priority operator-priority-logic)

Externe Repräsentation: TEXForm

(define (texform expr)

Liefert die TEX-Form eines Ausdrucks. Klammerung erfolgt, wenn die Priorität dies erfordert.

  (let ((expr-priority (operator-priority expr)))
    (cond ((negation? expr)
           (string-append "\\neg "
                          (texform-aux-open (subexpr expr)
                                            expr-priority)))
          ((conjunction? expr)
           (texform-multiop "1" "\\wedge " expr expr-priority))
          ((disjunction? expr)
           (texform-multiop "0" "\\vee " expr expr-priority))
          ((implication? expr)
           (texform-binop "\\Rightarrow " expr expr-priority))

          ((equivalence? expr)
           (texform-binop "\\iff " expr expr-priority))
          ((xor? expr)
           (texform-binop "\\oplus " expr expr-priority))
          (else (texform-atom expr)))))
(define (texform-aux expr priority)
  (if (>= priority (operator-priority expr))
      (string-append "(" (texform expr) ")")
      (texform expr)))
(define (texform-aux-open expr priority)
  (if (> priority (operator-priority expr))
      (string-append "(" (texform expr) ")")
      (texform expr)))
(define (texform-atom expr)
  (string-append "\\mathit{"
                 (atom->string expr)
                 "}"))
(define (texform-binop opname expr priority)
  (string-append (texform-aux (left-subexpr expr) priority)
                 opname
                 (texform-aux (right-subexpr expr) priority)))
(define (texform-multiop neutralname opname expr priority)
  (cond ((void-multiop? expr) neutralname)
        ((unary-multiop? expr)
         (texform-aux-open (car (subexpr-list expr))
                           priority))
        (else (string-append
               (texform-aux (car (subexpr-list expr))
                            priority)
               (texform-list opname
                             (cdr (subexpr-list expr))
                             priority)))))
(define (texform-list opname oplist priority)
  (if (null? oplist)
      ""
      (string-append opname
                     (texform-aux (car oplist) priority)
                     (texform-list opname (cdr oplist) priority))))

Externe Repräsentation: TextForm

(define (textform expr)

Liefert die Text-Form eines Ausdrucks. Klammerung erfolgt, wenn die Priorität dies erfordert.

  (let ((expr-priority (operator-priority expr)))
    (cond ((negation? expr)
           (string-append "!"
                          (textform-aux-open (subexpr expr)

                                             expr-priority)))
          ((conjunction? expr)
           (textform-multiop "1" " && " expr expr-priority))
          ((disjunction? expr)
           (textform-multiop "0" " || " expr expr-priority))
          ((implication? expr)
           (textform-binop " => " expr expr-priority))
          ((equivalence? expr)
           (textform-binop " <=> " expr expr-priority))
          ((xor? expr)
           (textform-binop " ^^" expr expr-priority))
          (else (textform-atom expr)))))
(define (textform-aux expr priority)
  (if (>= priority (operator-priority expr))
      (string-append "(" (textform expr) ")")
      (textform expr)))
(define (textform-aux-open expr priority)
  (if (> priority (operator-priority expr))
      (string-append "(" (textform expr) ")")
      (textform expr)))
(define (textform-atom expr)
  (atom->string expr))
(define (textform-binop opname expr priority)
  (string-append (textform-aux (left-subexpr expr) priority)
                 opname
                 (textform-aux (right-subexpr expr) priority)))
(define (textform-multiop neutralname opname expr priority)
  (cond ((void-multiop? expr) neutralname)
        ((unary-multiop? expr)
         (textform-aux-open (car (subexpr-list expr))
                            priority))
        (else (string-append
               (textform-aux (car (subexpr-list expr))
                             priority)
               (textform-list opname
                              (cdr (subexpr-list expr))
                              priority)))))
(define (textform-list opname oplist priority)
  (if (null? oplist)
      ""
      (string-append opname
                     (textform-aux (car oplist) priority)
                     (textform-list opname (cdr oplist) priority))))

Konjunktive Normalform

(define positive-literal? logical-atom?)
(define (negative-literal? expr)
  (and (negation? expr)
       (logical-atom? (subexpr expr))))

(define (contrary? literal1 literal2)
(or (and (positive-literal? literal1)
     (negative-literal? literal2))
(and (positive-literal? literal2)
     (negative-literal? literal1))))
(define (literal? expr)
(or (positive-literal? expr)
(negative-literal? expr)))
(define (clause? expr)

Ermittelt, ob eine Klausel vorliegt. Auch ein einzelnes Literal wird als Klausel angesehen.

(or (literal? expr)
(and (disjunction? expr)
     (apply lambda-and (map literal? (subexpr-list expr))))))
(define (clause->list clause)

Liefert eine Liste aller Literale in der Klausel.

(if (disjunction? clause)
(subexpr-list clause)
(list clause)))
(define (literal-atom literal)

Liefert das Atom des Literals.

(if (negation? literal)
(subexpr literal)
literal))
(define (negate-literal literal)

Negiert das Literal.

(if (negative-literal? literal)
(literal-atom literal)
(make-negation (literal-atom literal))))
(define (canonicalize expr)

Liefert einen äquivalenten Ausdruck, der nur Konjunktionen, Disjunktionen und Negationen verwendet. Die anderen äquivalenten Umformungen behandeln nur diese drei Verknüpfungen.

(cond ((logical-atom? expr)
   (canonicalize-atom expr))
  ((negation? expr)
   (make-negation (canonicalize (subexpr expr))))
  ((conjunction? expr)
   (apply make-conjunction
          (map canonicalize (subexpr-list expr))))
  ((disjunction? expr)

 (apply make-disjunction
        (map canonicalize (subexpr-list expr))))
((implication? expr)
 (make-disjunction
  (make-negation (canonicalize (left-subexpr expr)))
  (canonicalize (right-subexpr expr))))
((equivalence? expr)
 (let ((canonicalized-left
        (canonicalize (left-subexpr expr)))
       (canonicalized-right
        (canonicalize (right-subexpr expr))))
   (make-disjunction
    (make-conjunction canonicalized-left
                      canonicalized-right)
    (make-conjunction
     (make-negation canonicalized-left)
     (make-negation canonicalized-right)))))
((xor? expr)
 (let ((canonicalized-left
        (canonicalize (left-subexpr expr)))
       (canonicalized-right
        (canonicalize (right-subexpr expr))))
   (make-disjunction
    (make-conjunction canonicalized-left
                      (make-negation canonicalized-right))
    (make-conjunction (make-negation canonicalized-left)
                      canonicalized-right))))
(else expr)))
(define (canonicalize-atom expr) expr)
(define (normalize-canonical expr)

Bringt einen kanonischen Ausdruck in Prä-KNF, das heißt, der Ausdruck ist eine Konjunktion von Disjunktionen, aber möglicherweise noch nicht abgeflacht und vereinfacht.

(cond ((logical-atom? expr) expr)
((negation? expr) (normalize-negation expr))
((conjunction? expr) (normalize-conjunction expr))
((disjunction? expr) (normalize-disjunction expr))
(else expr)))
(define (normalize-negation expr)
(cond ((logical-atom? (subexpr expr)) expr)
((negation? (subexpr expr))

Doppelte Verneinung entfernen

 (normalize-canonical (subexpr (subexpr expr))))
((conjunction? (subexpr expr))

de Morgan

 (normalize-canonical
  (apply make-disjunction

(map make-negation
(subexpr-list (subexpr expr))))))
((disjunction? (subexpr expr))

de Morgan

(normalize-canonical
(apply make-conjunction
(map make-negation
(subexpr-list (subexpr expr))))))
(else expr)))
(define (normalize-disjunction expr)

Hier werden Disjunktionen von Konjunktionen mit dem Distributivgesetz ”ausmultipliziert“.

(if (null? (subexpr-list expr))
expr
(let ((normalized-left
(normalize-canonical (car (subexpr-list expr)))))
(cond ((null? (cdr (subexpr-list expr)))
(make-disjunction normalized-left))
((conjunction? normalized-left)
(let ((right (cdr (subexpr-list expr))))
(apply make-conjunction
  (map (lambda (ex)
         (normalize-disjunction
          (apply make-disjunction
                 (cons ex right))))
       (subexpr-list normalized-left)))))
((and (conjunction? (cadr (subexpr-list expr)))
(null? (cddr (subexpr-list expr))))
(apply make-conjunction
(map (lambda (ex)
       (normalize-disjunction
        (make-disjunction normalized-left
                          ex)))
     (subexpr-list
      (cadr (subexpr-list expr))))))
(else (make-disjunction
normalized-left
(normalize-disjunction
(apply make-disjunction
       (cdr (subexpr-list expr))))))))))
(define (normalize-conjunction expr)
(let ((normalized-subexpr-list
(map normalize-canonical (subexpr-list expr))))
(apply make-conjunction normalized-subexpr-list)))
(define (flatten expr)

Flacht Prä-KNF-Ausdrücke ab.

(cond ((conjunction? expr)
 (apply make-conjunction
        (flatten-list conjunction? (subexpr-list expr))))
((disjunction? expr)
 (apply make-disjunction
        (flatten-list disjunction? (subexpr-list expr))))
((negation? expr)
 (make-negation (flatten (subexpr expr))))
(else expr)))
(define (flatten-list predicate? expr-list)
(cond ((null? expr-list) expr-list)
((predicate? (car expr-list))
 (append (flatten-list predicate?
                       (subexpr-list (car expr-list)))
         (flatten-list predicate?
                       (cdr expr-list))))
(else (cons (flatten (car expr-list))
            (flatten-list predicate?
                          (cdr expr-list))))))
(define (remove-duplicates expr)

Entfernt aus allen Klauseln mehrfach auftretende Literale; entfernt überflüssige (immer wahre) Klauseln.

(if (conjunction? expr)
(apply make-conjunction
     (remove-duplicates-clause-list (subexpr-list expr)))
expr))
(define (remove-duplicates-clause-list clause-list)
(cond ((null? clause-list) clause-list)
((obsolete-literal-list? (clause->list (car clause-list)))
 (remove-duplicates-clause-list (cdr clause-list)))
(else (cons (apply make-disjunction
                   (remove-duplicates-list
                    (clause->list
                     (car clause-list))))
            (remove-duplicates-clause-list
             (cdr clause-list))))))
(define (obsolete-literal-list? literal-list)

Ermittelt, ob die Liste komplementäre Literale enthält. (Eine Disjunktion der Literale der Liste ist dann immer wahr.)

(and (pair? literal-list)
(or (member (negate-literal (car literal-list))
         (cdr literal-list))
   (obsolete-literal-list? (cdr literal-list)))))
(define (remove-duplicates-list literal-list)

Entfernt wiederholte Vorkommen von Literalen in der Liste.

(cond ((null? literal-list) literal-list)
   ((member (car literal-list) (cdr literal-list))
    (remove-duplicates-list (cdr literal-list)))
   (else (cons (car literal-list)
               (remove-duplicates-list (cdr literal-list))))))
(define (normalize expr)

Bringt einen Ausdruck in die KNF.

(remove-duplicates
(flatten (normalize-canonical (canonicalize expr)))))

Resolution

(define (theorem? axioms hypothesis)

Ermittelt, ob die Hypothese ein Satz des Axiomensystems ist.

(not
(not
(contradiction?
(normalize
 (make-conjunction axioms (make-negation hypothesis)))))))
(define (contradiction? expr)

Führt auf dem KNF-Ausdruck Resolution durch, bis ein Widerspruch abgeleitet wurde oder sicher ist, daß kein Widerspruch abgeleitet werden kann.

(resolvent-diagonal? (subexpr-list expr) '()))
(define (resolvent-diagonal? clauses-to-come clauses-done)

Geht iterativ alle Elemente der ersten Klauselmenge durch und resolviert sie mit allen Elementen der zweiten Klauselmenge; die Resolventen werden der ersten Klauselmenge hinzugefügt, und das verwendete Element der ersten Klauselmenge wird in die zweite Menge verschoben. Diese Diagonalisierung entspricht einer Breitensuche, da die gefundenen Resolventen an die erste Klauselmenge angehängt wird.

(and (not (null? clauses-to-come))
  (let* ((res-list (resolvent-list (car clauses-to-come)
                                   clauses-done
                                   '()))
         (new-clauses-done (set-cons (car clauses-to-come)
                                     clauses-done))
         (new-clauses-to-come
          (set-minus (set-append clauses-to-come
                                 res-list)
                     new-clauses-done)))

Ist die leere Disjunktion abgeleitet? Sonst muß weiter iteriert werden.

    (or (found-answer? res-list)
        (resolvent-diagonal? new-clauses-to-come
                             new-clauses-done)))))

(define (found-answer? res-list)

Ermittelt, ob die leere Disjunktion abgeleitet wurde.

(member (make-disjunction) res-list))
(define (resolvent-list clause clause-list res-list)

Resolviert iterativ alle Elemente der Liste mit der Klausel, sofern möglich. Das Ergebnis ist eine Liste aller Resolventen.

(cond ((null? clause-list) res-list)
   (else (resolvent-list
          clause
          (cdr clause-list)
          (set-append (resolve-all clause (car clause-list))
                      res-list)))))
(define (resolve-all clause1 clause2)

Ermittelt eine Liste aller Resolventen, die sich durch Auswahl eines Paars komplementärer Literale der angegebenen Klauseln ergeben.

(map (lambda(l) (apply make-disjunction l))
  (resolve-all-list (clause->list clause1) '()
                    (clause->list clause2) '())))
(define (resolve-all-list list1-to-come list1-done list2 res-list)
(cond ((null? list1-to-come) res-list)
   ((member (negate-literal (car list1-to-come)) list2)
    (resolve-all-list (cdr list1-to-come)
                      (cons (car list1-to-come) list1-done)
                      list2
                      (cons
                       (join-literal-lists
                        (append list1-to-come list1-done)
                        list2
                        (car list1-to-come)
                        (negate-literal (car list1-to-come)))
                       res-list)))
   (else
    (resolve-all-list (cdr list1-to-come)
                      (cons (car list1-to-come) list1-done)
                      list2
                      res-list))))
(define (join-literal-lists list1 list2 literal1 literal2)

Verbindet die Literal-Listen. Zuvor werden die angegebenen Literale jeweils aus den Listen entfernt.

(set-append
(remove-if (lambda (x) (equal? x literal1)) list1)
(remove-if (lambda (x) (equal? x literal2)) list2)))
(define (resolve clause1 clause2)

Ermittelt eine Resolvente der beiden Klauseln. Wird nicht verwendet.

  (car (resolve-all clause1 clause2)))
(define (resolvable? clause1 clause2)

Ermittelt, ob die Klauseln resolvierbar sind. Wird nicht verwendet.

  (not (null? (resolve-all clause1 clause2))))

2 Scheme-Modul für Prädikatenlogik

Das folgende Scheme-Modul (plogic.scm) verallgemeinert die Funktionen aus dem Aussagenlogik-Modul für die Verwendung mit prädikatenlogischen Ausdrücken. Es werden Quantifizierungen, Prädikat-Anwendungen und Terme als abstrakte Datentypen definiert. Ein einfaches Antwortsystem wird bereitgestellt. Hilfsmittel

Wir verwenden das Aussagenlogik-Modul und überschreiben einige seiner Funktionen.

(load "logic.scm")

Interne Repräsentation von Prädikatenlogik

Konstruktoren

(define (make-function-symbol name)
  (cons 'function name))
(define (make-predicate-symbol name)
  (cons 'predicate name))
(define (make-variable name)
  (cons 'variable name))
;(define (make-variable name) name)
(define (make-function-application name term-list)
  (cons (make-function-symbol name) term-list))
(define (make-constant name)
  (make-function-application name '()))
(define (make-predicate-application name term-list)
  (cons (make-predicate-symbol name) term-list))
(define (make-forall-quantification variable formula)
  (list 'forall variable formula))
(define (make-exists-quantification variable formula)
  (list 'exists variable formula))

Prädikate

(define (function-symbol? x)
  (and (pair? x)
       (equal? (car x) 'function)))

(define (predicate-symbol? x)
  (and (pair? x)
       (equal? (car x) 'predicate)))
(define (variable? x)
  (and (pair? x)
       (equal? (car x) 'variable)))
;(define variable? symbol?)
(define (forall-quantification? formula)
  (and (pair? formula)
       (equal? (car formula) 'forall)))
(define (exists-quantification? formula)
  (and (pair? formula)
       (equal? (car formula) 'exists)))
(define (function-application? formula)
  (and (pair? formula)
       (function-symbol? (car formula))))
(define (predicate-application? formula)
  (and (pair? formula)
       (predicate-symbol? (car formula))))

Selektor für den Namen eines Funktionssymbols oder Prädikatssymbols

(define name cdr)

Selektor für den Namen einer Variablen

(define (variable-name term) (cdr term))
;(define (variable-name term) term)

Selektoren für Funktions- oder Prädikats-Anwendungen

(define applied-symbol car)
(define (applied-symbol-name application)
  (name (applied-symbol application)))
(define term-list cdr)
(define (arity application)

Ermittelt die Stelligkeit einer Prädikats- oder Funktions-Anwendung.

  (length (term-list application)))

Selektoren für quantifizierte Ausdrücke

(define quantified-variable cadr)
(define subject-to-quantification caddr)

(define (string-upcase string)
  (list->string (map char-upcase (string->list string))))
(define (string-capitalize string)
  (let ((char-list (string->list string)))
    (if (null? char-list)
        ""
        (list->string
         (cons (char-upcase (car char-list))
               (map char-downcase (cdr char-list)))))))
(define (string-downcase string)
  (list->string (map char-downcase (string->list string))))

Überschreiben der Operatorprioritätsermittlung

(define (operator-priority-plogic expr)
  (cond ((forall-quantification? expr) 9)
        ((exists-quantification? expr) 9)
        (else (operator-priority-logic expr))))
(define operator-priority operator-priority-plogic)

Externe Repräsentation: TEXForm

Überschreiben der Repräsentation von Aussagenlogik-Atomen

(define (texform-atom expr)
  (cond ((forall-quantification? expr)
         (texform-quantification
          "\\forall "
          (quantified-variable expr)
          (texform-aux-open (subject-to-quantification expr) 9)))
        ((exists-quantification? expr)
         (texform-quantification
          "\\exists "
          (quantified-variable expr)
          (texform-aux-open (subject-to-quantification expr) 9)))
        ((predicate-application? expr)
         (texform-application
          (texform-predicate-name (applied-symbol-name expr))
          (term-list expr)))
        (else (atom->string expr))))
(define (texform-term expr)
  (cond ((variable? expr)
         (texform-variable (variable-name expr)))
        ((function-application? expr)
         (if (null? (term-list expr))
             (texform-constant (applied-symbol-name expr))
             (texform-application
              (texform-function-name (applied-symbol-name expr))
              (term-list expr))))
        (else (atom->string expr))))

(define (texform-predicate-name name)
  (string-append "\\mathit{"
                 (string-capitalize (atom->string name)) "}"))
(define (texform-function-name name)
  (string-append "\\mathit{"
                 (string-downcase (atom->string name)) "}"))
(define (texform-variable name)
  (string-append "\\mathit{"
                 (string-downcase (atom->string name)) "}"))
(define (texform-constant name)
  (string-append "\\mathit{"
                 (string-capitalize (atom->string name)) "}"))
(define (texform-application name-string term-list)
  (cond ((null? term-list) name-string)
        (else (string-append name-string
                             "("
                             (texform-term (car term-list))
                             (texform-term-list "," (cdr term-list))
                             ")"))))
(define (texform-term-list opname oplist)
  (if (null? oplist)
      ""
      (string-append opname
                     (texform-term (car oplist))
                     (texform-term-list opname (cdr oplist)))))
(define (texform-quantification quantname quantvar quantexpr-string)
  (string-append quantname
                 (texform-variable quantvar)
                 "\\, "
                 quantexpr-string))

Externe Repräsentation: TextForm

Überschreiben der Repräsentation von Aussagenlogik-Atomen

(define (textform-atom expr)
  (cond ((forall-quantification? expr)
         (textform-quantification
          "forall "
          (quantified-variable expr)
          (textform-aux-open (subject-to-quantification expr) 9)))
        ((exists-quantification? expr)
         (textform-quantification
          "exists "
          (quantified-variable expr)
          (textform-aux-open (subject-to-quantification expr) 9)))
        ((predicate-application? expr)
         (textform-application
          (textform-predicate-name (applied-symbol-name expr))
          (term-list expr)))
        (else (atom->string expr))))

(define (textform-term expr)
  (cond ((variable? expr)
         (textform-variable (variable-name expr)))
        ((function-application? expr)
         (if (null? (term-list expr))
             (textform-constant (applied-symbol-name expr))
             (textform-application
              (textform-function-name (applied-symbol-name expr))
              (term-list expr))))
        (else (atom->string expr))))
(define (textform-predicate-name name)
  (string-capitalize (atom->string name)))
(define (textform-function-name name)
  (string-downcase (atom->string name)))
(define (textform-variable name)
  (string-downcase (atom->string name)))
(define (textform-constant name)
  (string-capitalize (atom->string name)))
(define (textform-application name-string term-list)
  (cond ((null? term-list) name-string)
        (else (string-append
               name-string "("
               (textform-term (car term-list))
               (textform-term-list "," (cdr term-list))
               ")"))))
(define (textform-term-list opname oplist)
  (if (null? oplist)
      ""
      (string-append opname
                     (textform-term (car oplist))
                     (textform-term-list opname (cdr oplist)))))
(define (textform-quantification quantname
                                 quantvar quantexpr-string)
  (string-append quantname
                 (textform-variable quantvar)
                 " "
                 quantexpr-string))

Substitutionen

(define make-atomic-substitution cons)
(define atomic-substitution-variable car)
(define atomic-substitution-term cdr)

Eine Substitution ist eine Liste atomarer Substitutionen.

(define (make-substitution var term)
  (list (make-atomic-substitution var term)))

(define (find-substitution var subst)

Findet die Teilsubstitution, deren erste atomare Substitution die angegebene Variable ersetzt.

(assoc var subst))
(define (compose-substitutions . subst-list)

Erzeugt die Komposition einer Liste von Substitutionen. Die am weitesten links stehende Substitution wird zuletzt auf eine Formel angewandt, wie man es bei der Komposition von Abbildungen gewöhnt ist. Auf die rechten Ersatz-Ausdrücke werden also weiter links stehende Substitutionen angewandt.

(if (null? subst-list)
 '()
 (append
  (car subst-list)
  (apply
   compose-substitutions
   (map (lambda(subst)
          (map (lambda(atomic-subst)
                 (make-atomic-substitution
                  (atomic-substitution-variable atomic-subst)
                  (apply-substitution-term
                   (atomic-substitution-term atomic-subst)
                   (car subst-list))))
               subst))
        (cdr subst-list))))))
(define (apply-substitution formula subst)

Wendet eine Substitution auf eine Formel an. Vorausgesetzt wird eine bereinigte Form, so daß wir uns nicht um gebundene Variablen kümmern müssen.

(cond ((forall-quantification? formula)
    (make-forall-quantification
     (quantified-variable formula)
     (apply-substitution (subject-to-quantification formula)
                         subst)))
   ((exists-quantification? formula)
    (make-exists-quantification
     (quantified-variable formula)
     (apply-substitution (subject-to-quantification formula)
                         subst)))
   ((conjunction? formula)
    (apply make-conjunction
           (map (lambda(f) (apply-substitution f subst))
                (subexpr-list formula))))
   ((disjunction? formula)
    (apply make-disjunction
           (map (lambda(f) (apply-substitution f subst))
                (subexpr-list formula))))
   ((negation? formula)

         (make-negation (apply-substitution (subexpr formula)
                                            subst)))
        ((predicate-application? formula)
         (make-predicate-application
          (applied-symbol-name formula)
          (map (lambda(t) (apply-substitution-term t subst))
               (term-list formula))))
        (else formula)))
(define (apply-substitution-term term subst)

Wendet eine Substitution auf einen Term an.

  (cond ((function-application? term)
         (make-function-application
          (applied-symbol-name term)
          (map (lambda (t) (apply-substitution-term t subst))
               (term-list term))))
        ((variable? term)
         (let ((s (find-substitution (variable-name term) subst)))
           (if (pair? s)
               (atomic-substitution-term s)
               term)))
        (else term)))

Erzeugen von Namen

(define temp-counter 0)
(define (temporary-symbol prefix)
  (set! temp-counter (+ temp-counter 1))
  (string->symbol
   (string-append prefix (number->string temp-counter))))
(define (temporary-predicate)
  (temporary-symbol "p_"))
(define (temporary-variable)
  (temporary-symbol "v_"))
(define (temporary-function)
  (temporary-symbol "f_"))

Konjunktive Normalform

(define (canonicalize-atom expr)

Überschreibt canonicalize-atom aus logic.scm. Verallgemeinert so die Funktion canonicalize, indem aussagenlogische Atome, die prädikatenlogische Formeln sind, weiter zerlegt werden.

  (cond ((forall-quantification? expr)
         (make-forall-quantification
          (quantified-variable expr)
          (canonicalize (subject-to-quantification expr))))
        ((exists-quantification? expr)

 (make-exists-quantification
  (quantified-variable expr)
  (canonicalize (subject-to-quantification expr))))
(else expr)))
(define (rename-bound-variables formula)

Überführt eine kanonische Formel in eine bereinigte Form durch systematisches Umbenennen gebundener Variablen.

(rename-bound-variables-aux formula '()))
(define (rename-bound-variables-aux formula subst)
(cond ((negation? formula)
 (make-negation
  (rename-bound-variables-aux (subexpr formula) subst)))
((conjunction? formula)
 (apply make-conjunction
        (map (lambda(f)
               (rename-bound-variables-aux f subst))
             (subexpr-list formula))))
((disjunction? formula)
 (apply make-disjunction
        (map (lambda(f)
               (rename-bound-variables-aux f subst))
             (subexpr-list formula))))
((forall-quantification? formula)
 (mangle-quantification make-forall-quantification
                        formula subst))
((exists-quantification? formula)
 (mangle-quantification make-exists-quantification
                        formula subst))
((predicate-application? formula)
 (make-predicate-application
  (applied-symbol-name formula)
  (map (lambda(term) (apply-substitution-term term subst))
       (term-list formula))))
(else formula)))
(define (mangle-quantification make-quantification formula subst)
(let ((mangled-quantified-variable (temporary-variable)))
(make-quantification
mangled-quantified-variable
(rename-bound-variables-aux
(subject-to-quantification formula)
(compose-substitutions
(make-substitution
(quantified-variable formula)
(make-variable mangled-quantified-variable))
subst)))))
(define (quantify-free-variables formula)

Bindet freie Variablen in der kanonischen Formel mit Existenzquantoren.

(let ((var-list (free-variables formula)))
(quantify-list formula var-list)))
(define (quantify-list formula var-list)
(if (null? var-list)
formula
(quantify-list
(make-exists-quantification (car var-list) formula)
(cdr var-list))))
(define (free-variables formula)

Ermittelt eine Liste der freien Variablen in der kanonischen Formel.

(cond ((negation? formula) (free-variables (subexpr formula)))
((or (conjunction? formula)
     (disjunction? formula))
 (apply set-append
        (map free-variables (subexpr-list formula))))
((predicate-application? formula)
 (apply set-append
        (map free-variables-term (term-list formula))))
((or (exists-quantification? formula)
     (forall-quantification? formula))
 (remove-if (lambda(x)
              (equal? x (quantified-variable formula)))
            (free-variables
             (subject-to-quantification formula))))
(else '())))
(define (free-variables-term term)
(cond ((function-application? term)
 (apply set-append
        (map free-variables-term (term-list term))))
((variable? term)
 (list (variable-name term)))
(else '())))
(define (replace-predicate formula predicate replacement)

Ersetzt in der Formel die Prädikat-Anwendung durch die Ersatzformel; kennt nur Quantifizierungen und Negation.

(cond ((forall-quantification? formula)
 (make-forall-quantification
  (quantified-variable formula)
  (replace-predicate (subject-to-quantification formula)
                     predicate replacement)))
((exists-quantification? formula)
 (make-exists-quantification
  (quantified-variable formula)
  (replace-predicate (subject-to-quantification formula)
                     predicate replacement)))
((negation? formula)
 (make-negation (replace-predicate (subexpr formula)

                                   predicate replacement)))
((predicate-application? formula)
 (if (equal? (applied-symbol-name formula) predicate)
     replacement
     formula))
(else formula)))
(define (prenexify formula)

Überführt eine kanonische, bereinigte, vollständig gebundene Formel in die Pränexform.

(let* ((temp-predicate (temporary-predicate))
 (collected
  (collect-quantifications
   formula
   (make-predicate-application temp-predicate '()))))
(replace-predicate (cdr collected)
               temp-predicate
               (car collected))))
(define (collect-quantifications formula temp-predicate)

Liefert ein Paar: Dequantifizierte Formel und Quantoren-Vorlage (das angegebene Prädikat, quantifiziert mit allen Quantoren).

(cond ((negation? formula)
 (let ((collected (collect-quantifications (subexpr formula)
                                           temp-predicate)))
   (cons (make-negation (car collected))
         (morganize-negation (cdr collected)))))
((disjunction? formula)
 (collect-quantifications-multiop
  make-disjunction (subexpr-list formula) temp-predicate))
((conjunction? formula)
 (collect-quantifications-multiop
  make-conjunction (subexpr-list formula) temp-predicate))
((forall-quantification? formula)
 (swap-quantification formula
                      make-forall-quantification
                      temp-predicate))
((exists-quantification? formula)
 (swap-quantification formula
                      make-exists-quantification
                      temp-predicate))
(else (cons formula temp-predicate))))
(define (collect-quantifications-multiop make-multiop
                                 expr-list temp-predicate)
(collect-quantifications-list make-multiop expr-list '()
                        temp-predicate temp-predicate))
(define (collect-quantifications-list make-multiop
                              expr-list changed-list
                              quant temp-predicate)

(if (null? expr-list)
 (cons (apply make-multiop changed-list)
       quant)
 (let ((collected-car
        (collect-quantifications (car expr-list)
                                 temp-predicate)))
   (collect-quantifications-list
    make-multiop
    (cdr expr-list)
    (cons (car collected-car) changed-list)
    (replace-predicate quant
                       (applied-symbol-name temp-predicate)
                       (cdr collected-car))
    temp-predicate))))
(define (swap-quantification formula
                        make-quantification temp-predicate)

Wälzt einen Quantor der Formel auf die Quantoren-Vorlage der gebundenen Formel um.

(let ((collected (collect-quantifications
               (subject-to-quantification formula)
               temp-predicate)))
(cons (car collected)
     (make-quantification (quantified-variable formula)
                          (cdr collected)))))
(define (morganize-negation formula)

Morganisiert alle führenden Quantoren.

(cond ((forall-quantification? formula)
    (make-exists-quantification
     (quantified-variable formula)
     (morganize-negation (subject-to-quantification formula))))
   ((exists-quantification? formula)
    (make-forall-quantification
     (quantified-variable formula)
     (morganize-negation (subject-to-quantification formula))))
   (else formula)))
(define (skolemify formula)

Überführt eine Formel in Pränexform in die Skolemform

(skolemify-aux formula '() '()))
(define (skolemify-aux formula variable-list subst)

Sammelt die all-quantifizierten Variablen in einer Variablenliste und ersetzt alle Vorkommen von Existenz-quantifizierten Variablen durch eine Anwendung eines neu erfundenen Funktionssymbols auf die gesammelten Variablen.

(cond ((forall-quantification? formula)
       (make-forall-quantification
        (quantified-variable formula)
        (skolemify-aux
         (subject-to-quantification formula)
         (cons (make-variable
                (quantified-variable formula))
               variable-list)
         subst)))
      ((exists-quantification? formula)
       (skolemify-aux
        (subject-to-quantification formula)
        variable-list
        (compose-substitutions
         (make-substitution
          (quantified-variable formula)
          (make-function-application (temporary-function)
                                     variable-list)))))
      (else (apply-substitution formula subst))))
(define (normalize formula)

Bringt eine Formel in die KNF. Überschreibt die gleichnamige Funktion aus

   logic.scm.
(remove-duplicates
 (flatten
  (normalize-canonical
   (dequantify
    (pre-normalize formula))))))
(define (pre-normalize formula)
(skolemify
 (prenexify
  (quantify-free-variables
   (rename-bound-variables
    (canonicalize formula))))))
(define (dequantify formula)

Entfernt führende Quantoren.

(cond ((or (forall-quantification? formula)
           (exists-quantification? formula))
       (dequantify (subject-to-quantification formula)))
      (else formula)))

Unifikation von Termen und Prädikat-Anwendungen

(define (occurrence? variable term)

Implementation des ‘occur check’.

(cond ((function-application? term)
       (apply lambda-or (map (lambda(t) (occurrence? variable t))
                             (term-list term))))
      ((variable? term)
       (equal? (variable-name term) variable))))

(define (difference predicate-app-list)

Ermittelt eine zur Eingabeliste parallele Liste, welche die Differenzterme enthält. Das Ergebnis ist #t, wenn die Prädikat-Anwendungen identisch sind; (), wenn wegen unterschiedlicher Prädikate nichts machbar ist. Ansonsten wird die Liste der Unterscheidungsterme geliefert.

(let ((car-arity (arity (car predicate-app-list)))
   (car-name (applied-symbol-name (car predicate-app-list))))
(if (apply
    lambda-and
    (map (lambda (pred-app)
           (and
            (equal? (applied-symbol-name pred-app) car-name)
            (= (arity pred-app) car-arity)))
         (cdr predicate-app-list)))
   (difference-list (map term-list predicate-app-list))
   '())))
(define (difference-list term-list-list)

Liefert die Liste der Unterscheidungsterme. Vorausgesetzt wird, daß eine Liste gleichlanger Listen vorliegt.

(if (null? (car term-list-list))
 #t
 (let ((mapcar-difference
        (difference-term (map car term-list-list))))
   (if (eq? mapcar-difference #t)
       (difference-list (map cdr term-list-list))
       mapcar-difference))))
(define (difference-term t-list)

Liefert die Liste der Unterscheidungsterme oder #t, wenn die Terme identisch sind.

(cond ((function-application? (car t-list))

Überprüfe, ob alle Elemente Funktionsanwendungen sind, deren Funktionssymbole zudem übereinstimmen; wenn ja, gehe deren Argumente von links nach rechts durch. Ansonsten liefere die ganze Liste als Differenzliste.

    (let ((car-arity (arity (car t-list)))
          (car-name (applied-symbol-name (car t-list))))
      (if (apply lambda-and
                 (map (lambda (t)
                        (and (function-application? t)
                             (equal? (applied-symbol-name t)
                                     car-name)
                             (= (arity t) car-arity)))
                      (cdr t-list)))
          (difference-list (map term-list t-list))
          t-list)))
   ((variable? (car t-list))

Überprüfe, ob alle Variablen übereinstimmen; wenn ja, liefere #t. Ansonsten liefere die ganze Liste als Differenzliste.

    (let ((car-name (variable-name (car t-list))))
      (if (apply
           lambda-and
           (map (lambda (t)
                  (and (variable? t)
                       (equal? (variable-name t) car-name)))
                (cdr t-list)))
          #t
          t-list)))
   (else t-list)))
(define (mgu predicate-app-list)

Ermittelt den ‘mgu’ (allgemeinsten Unifikator) der Prädikat-Anwendungen mittels des Verfahrens von Robinson. Das Ergebnis ist #t, wenn die Prädikat-Anwendungen nicht unifizierbar sind; ansonsten die gefundene Substitution.

(mgu-aux predicate-app-list '()))
(define (mgu-aux predicate-app-list subst)
(let ((diff-list (difference predicate-app-list)))
(cond
((eq? diff-list #t) subst)
((null? diff-list) #t)
(else
 (let ((list-var (first-that variable? diff-list)))
   (cond
    ((null? list-var) #t)

Mehrfaches Auftreten der Variable für sich ist zulässig; jedoch nicht Auftreten der Variable innerhalb der Terme (‘occur check’).

    ((apply lambda-or
            (map (lambda (t)
                   (occurrence?
                    (variable-name (car list-var))
                    t))
                 (remove-if variable? diff-list)))
     #t)
    (else

Wähle einen Term, der nicht die Variable selbst ist, erstelle eine Substitution und wende sie an.

     (let* ((list-notvar
             (first-that
              (lambda (t)
                (or (not (variable? t))
                    (not
                     (eq? (variable-name t)
                          (variable-name (car list-var))))))
              diff-list))

            (new-subst
             (make-substitution
              (variable-name (car list-var))
              (car list-notvar))))
       (mgu-aux
        (make-set
         (map (lambda (f)
                (apply-substitution f new-subst))
              predicate-app-list))
        (compose-substitutions new-subst subst))))))))))
(define (mgu-term term-list)

Das ist die in der Ausgabenstellung beschriebene mgu-Funktion, welche auf einer Liste von Termen operiert. Sie wird sonst nicht gebraucht.

(let ((temp-pred (temporary-predicate)))
(mgu (map (lambda (t)
           (make-predicate-application temp-pred (list t)))
         term-list))))

Prädikatenlogische Resolution

Wir verwenden die gleiche Resolutionsstrategie wie bei der Aussagenlogik: Es wird eine Breitensuche durchgeführt. Man beachte, daß die Funktion resolvent-diagonal? in der Prädikatenlogik nur ein Semi-Entscheidungs-verfahren ist. – Wir müssen nur eine einzige Funktion überschreiben:

(define (resolve-all-list list1-to-come list1-done list2 res-list)

Überschreibt die Funktion aus logic.scm.

(cond ((null? list1-to-come) res-list)
   (else (resolve-all-list
          (cdr list1-to-come)
          (cons (car list1-to-come) list1-done)
          list2
          (resolve-all-list-aux
           (car list1-to-come)
           (append (cdr list1-to-come) list1-done)
           list2
           '()
           res-list)))))
(define (resolve-all-list-aux list1-cur list1-rest
                         list2-to-come list2-done res-list)
(cond ((null? list2-to-come) res-list)
   ((contrary? list1-cur (car list2-to-come))
    (let ((car-mgu
           (mgu (list (literal-atom list1-cur)
                      (literal-atom (car list2-to-come))))))

Wenn nicht unifizierbar, in der zweiten Liste weitersuchen. Ansonsten Resolvente speichern und weitersuchen.

(cond ((eq? car-mgu #t)
(resolve-all-list-aux
list1-cur list1-rest
(cdr list2-to-come)
(cons (car list2-to-come) list2-done)
res-list))
(else
(resolve-all-list-aux
list1-cur list1-rest
(cdr list2-to-come)
(cons (car list2-to-come) list2-done)
(cons (map (lambda(literal)
             (apply-substitution literal
                                 car-mgu))
           (join-literal-lists
            (cons list1-cur list1-rest)
            (append list2-to-come list2-done)
            list1-cur
            (car list2-to-come)))
      res-list))))))
(else (resolve-all-list-aux
list1-cur list1-rest
(cdr list2-to-come)
(cons (car list2-to-come) list2-done)
res-list))))

Antwortsystem

(define (make-answer var-name)
(make-predicate-application
'answer
(if (pair? var-name)
(map make-variable var-name)
(list (make-variable var-name)))))
(define (answer? formula)
(and (predicate-application? formula)
(equal? (applied-symbol-name formula) 'answer)))
(define (answer-clause? formula)

Ermittelt, ob die Klausel nur aus Antwortliteralen besteht. Darin enthalten ist der Fall der leeren Klausel.

(apply lambda-and (map answer? (subexpr-list formula))))

Wir redefinieren die Entscheidung, ob eine Antwort gefunden wurde; falls ja, geben wir auch die Antwort zurück.

(define (found-answer? res-list)

Ermittelt, ob eine Antwort-Klausel (eine Klausel, die nur Antwortterme enthält) in der Liste enthalten ist.

(cond ((null? res-list) #f)
((answer-clause? (car res-list)) (car res-list))
(else (found-answer? (cdr res-list)))))

(define (forall-quantify var-name formula)
  (cond ((null? var-name) formula)
        ((pair? var-name)
         (forall-quantify
          (cdr var-name)
          (make-forall-quantification (car var-name) formula)))
        (else (make-forall-quantification var-name formula))))
(define (answer axioms question variable)

Ermittelt eine Antwort auf die Frage. Es kann eine einzelne Variable oder eine Liste von Variablen, die in der Frage frei sind, angegeben werden.

  (contradiction? (normalize
                   (make-conjunction
                    axioms
                    (make-forall-quantification
                     variable
                     (make-disjunction
                      (make-negation question)
                      (make-answer variable)))))))

3 Scheme-Modul für die vereinfachte Eingabe logischer Formeln

Die interne Repräsentation ist für die Eingabe von Formeln wenig geeignet. Man betrachte etwa das folgende Axiomensystem:

Liebt(Eva, Essen) ∧ Liebt(Eva, Wein) ∧ ∀x (Liebt(x, Wein) ⇒ Liebt(Adam, x))

Es hat die folgende interne Repräsentation:

(and ((predicate . liebt) ((function . eva)) ((function . essen)))
     ((predicate . liebt) ((function . eva)) ((function . wein)))
     (forall x
             (imply ((predicate . liebt) (variable . x)
                                         ((function . wein)))
                    ((predicate . liebt) ((function . adam))
                                         (variable . x)))))

Insbesondere die Darstellung von Konstanten als nullstellige Funktions-Anwendun-gen macht die Eingabe sehr aufwendig. Aus diesem Grunde wurde die Funktion parse entwickelt, die die folgende einfache Eingabe gestattet:

(parse '(and (liebt eva essen)
             (liebt eva wein)
             (forall x implies (liebt x wein) (liebt adam x))))

Funktionssymbole und Prädikatssymbole sind bereits durch die syntaktische Struktur eindeutig unterscheidbar. Für die Unterscheidung von Variablen und Konstanten wird eine Namensregel verwendet: Symbole, die mit den Buchstaben X, Y oder Z beginnen, werden als Variablen angesehen, alle anderen als Konstanten. Diese Namensregel läßt sich durch explizite Angabe übergehen, etwa mit '(var a) und

'(const x).

Verzichtet wurde hingegen auf die Möglichkeit einer Infix-Notation bei der Eingabe. Da Formeln häufig aus vielstelligen Konjunktionen und Disjunktionen bestehen, ist die Präfix-Notation wesentlich kürzer.

Das folgende Scheme-Modul (input.scm) enthält dies alles.

Einfache Eingabe logischer Formeln

(define (parse formula)

Untersucht die Formel und wandelt sie in die interne Repräsentation um.

(cond ((and (pair? formula)
   (null? (cdr formula)))

Entfernt ein überflüssiges Klammerpaar.

(parse (car formula)))
((and (pair? formula)
   (symbol? (car formula)))

Interpretiert Schlüsselwörter.

(case (car formula)
((all forall)
 (make-forall-quantification (cadr formula)
                             (parse (cddr formula))))
((ex exist exists)
 (make-exists-quantification (cadr formula)
                             (parse (cddr formula))))
((and)
 (apply make-conjunction (map parse (cdr formula))))
((or)
 (apply make-disjunction (map parse (cdr formula))))
((not)
 (make-negation (parse (cdr formula))))
((xor)
 (make-xor (parse (cadr formula))
           (parse (caddr formula))))
((imp imply implies)
 (make-implication (parse (cadr formula))
                   (parse (caddr formula))))
((eq eqv equiv equivalent)
 (make-equivalence (parse (cadr formula))
                   (parse (caddr formula))))
(else (parse-for-predicate formula))))
((pair? formula)

Sieht die Formel als Prädikat-Anwendung an.

(parse-for-predicate formula))
(else formula)))
(define (parse-for-predicate formula)
(make-predicate-application (car formula)
                   (map parse-term (cdr formula))))
(define (parse-term formula)

Untersucht den Term und wandelt ihn in die interne Repräsentation um.

  (cond ((pair? formula)
         (case (car formula)
           ((var vari variable)
            (if (pair? (cdr formula))
                (make-variable (cadr formula))
                (make-variable (cdr formula))))
           ((const constant)
            (if (pair? (cdr formula))
                (make-constant (cadr formula))
                (make-constant (cdr formula))))
           (else (make-function-application
                  (car formula)
                  (map parse-term (cdr formula))))))
        ((symbol? formula)
         (if (means-variable? formula)
             (make-variable formula)
             (make-constant formula)))
        (else (make-constant formula))))
(define (means-variable? symbol)

Per Konvention sind alle Symbole, die mit den Buchstaben X bis Z beginnen, Variablennamen.

  (let ((first-character
         (car (string->list (symbol->string symbol)))))
    (and (char-ci>=? first-character #\X)
         (char-ci<=? first-character #\Z))))

4 Anwendungsbeispiele

4.1 Arithmetik

Das Axiomensystem für die Addition nichtnegativer ganzer Zahlen.

(define ax-add
  (parse '(and (all x add x 0 x)
               (all x all y all z
                    (implies (add x y z)
                             (add x (s y) (s z)))))))
 ⟹ ax-add
(texform ax-add)

⟹ ∀x Add(x, 0 , x) ∧ ∀x ∀y ∀z (Add(x, y, z) ⇒ Add(x, s(y), s(z)))

Beweis eines Satzes dieses Axiomensystems:

(theorem? ax-add (parse '(add (s 0) (s (s 0)) (s (s (s 0))))))
 ⟹ #t

Berechnungen als Antworten auf Fragen:

(textform
 (answer ax-add (parse '(add (s (s 0)) (s (s (s 0))) y)) 'y))

 ⟹ "Answer(s(s(s(s(s(0))))))"
(textform
 (answer ax-add (parse '(add (s 0) x (s (s (s (s (s 0))))))) 'x))
 ⟹ "Answer(s(s(s(s(0)))))"

4.2 Mehrdeutige Antworten

(define ax-liebt
  (parse '(and (liebt eva essen)
               (or (liebt eva wein) (liebt anna wein))
               (forall x implies (liebt x wein) (liebt adam x)))))
 ⟹ ax-liebt
(texform ax-liebt)

⟹ Liebt(Eva, Essen) ∧ (Liebt(Eva, Wein) ∨ Liebt(Anna, Wein)) ∧ ∀x (Liebt(x, Wein) ⇒ Liebt(Adam, x))

(theorem? ax-liebt (parse '(ex y (liebt adam y))))
 ⟹ #t
(texform (answer ax-liebt (parse '(liebt adam y)) 'y))

⟹ Answer(Anna) ∨ Answer(Eva)

5 Grenzen

Das Axiomensystem für die Addition nichtnegativer ganzer Zahlen.

(define ax-add
  (parse '(and (all x add x 0 x)
               (all x all y all z
                    (implies (add x y z)
                             (add x (s y) (s z)))))))

Die Erweiterung für Multiplikation.

(define ax-arith
  (make-conjunction
   ax-add
   (parse '(and (all x mult x 0 0)
                (all x all y all z all w
                     (imply (and (mult x y z) (add z x (var w)))
                            (mult x (s y) (var w))))))))

Dieser Satz konnte bislang nicht bewiesen werden:

;(theorem? ax-arith (parse '(mult (s 0) (s 0) (s 0))))

Es ist noch nicht bekannt, ob ein Programmfehler dafür verantwortlich ist oder ob nur die Implementierung nicht effizient genug für die Lösung in angemessenem Zeit- und Speicherrahmen ist.