Verwirrenderweise ist das Beispiel für
display-l1 überhaupt keine Formel aus L1 -
Negationen sind ja nur bei Literalen erlaubt. Es ist erlaubt
und erwünscht, daß make-negation überprüft, daß
sein Argument eine Variable oder die Negation einer Variable
ist. Ersatzhalber - noch besser und bonuswürdig - würde
make-negation die deMorganschen Regeln anwendet,
um sicherzustellen, daß das Resultat in L1 ist. In beiden
Fällen allerdings trifft das Beispiel so allerdings nicht mehr
zu.
Ein besseres Beispiel wäre somit:
> (display-l1
(make-conjunction (make-negation (make-variable 1))
(make-disjunction (make-constant #t)
(make-constant #f)))))
(!P1 & (T | B))