; #lang racket ;; Teil 1: Mengenlehre ;; Mengenerweiterung: ;; Eingabe: ;; sets: Eine Liste von Listen (interpretiert als ;; Menge von Mengen) ;; element: Ein einzelnes (neues) Element ;; Ausgabe: ;; Liste von Listen, wobei jede der Originalliste ;; um das einzelne Element erweitert wird (define (add-to-sets sets element) (if (null? sets) sets (cons (cons element (car sets)) (add-to-sets (cdr sets) element)))) ;; Potenzmenge (define (powerset l) (cond ((null? l) (list l)) (else (let* ((sub-ps (powerset (cdr l))) (new (car l)) (sub-new (add-to-sets sub-ps new)) (result (append sub-ps sub-new))) result)))) ;; Element-Funktion (define (is-element? x set) (if (null? set) #f (if (equal? x (car set)) #t (is-element? x (cdr set))))) ;; Einfuegen in eine Menge (define (set-insert x set) (if (is-element? x set) set (cons x set))) ;; Vereinigungsmenge (define (set-union set1 set2) (if (null? set1) set2 (set-insert (car set1) (set-union (cdr set1) set2)))) ;; Filtern einer Liste nach einem Praedikat. Rueckgabewert: Liste der ;; Werte in lst, fuer die fun ungleich #f ist (define (filter fun lst) (if (null? lst) lst (let ((rest (filter fun (cdr lst))) (current (car lst))) (if (fun current) (cons current rest) rest)))) ;; Teil 2: Logik-Hilfsfunktionen ;; Menge der Aussagevariablen in einer Formel (define (get-form-propvars form) (if (symbol? form) (list form) (let ((op (car form)) (argvars (map get-form-propvars (cdr form)))) (cond ((equal? op 'not) (car argvars)) (else (set-union (car argvars) (cadr argvars))))))) ;; Menge der Aussagevariablen in einer Liste/Menge von Formeln (define (get-formset-propvars forms) (if (null? forms) '() (set-union (get-form-propvars (car forms)) (get-formset-propvars (cdr forms))))) ;; Ausgabe einer (funktionalen) Interpretation als Liste der mit #t ;; belegten (wahren) Variablen. vars ist Liste aller Variablen der ;; Domaene. (define (display-interpretation-atoms interpretation vars) (display (filter interpretation vars))) ;; Auswertung einer Formel unter einer Interpretation. (define (prop-eval form var-interpretation) (if (symbol? form) (var-interpretation form) (let ((op (car form)) (args (map (lambda (x) (prop-eval x var-interpretation)) (cdr form)))) (cond ((equal? op 'not) (not (car args))) ((equal? op 'or) (or (car args) (cadr args))) ((equal? op 'and) (and (car args) (cadr args))) ((equal? op 'implies) (or (not (car args)) (cadr args))) ((equal? op 'equiv) (equal? (car args) (cadr args))) (else (display "Error in formula") (newline)))))) ;; Wandele eine Liste von Variablen in eine (funktionale) ;; Interpretation um, die genau diese Variablen mit #t belegt, alle ;; anderen mit #f (define (make-var-interpretation true-vars) (lambda (x) (if (member x true-vars) #t #f))) ;; Wandele eine funktionale Interpretation auf Variablen in eine ;; funktionale Interpretation auf Formeln um (define (make-eval-fun interpretation) (lambda (x) (prop-eval x interpretation))) ;; Evaluiere eine Menge von Formeln. Ergebnis ist #t genau dann, wenn ;; alle Formeln unter der Interpretationen zu #t ausgewertet werden. (define (prop-eval-set set interpretation) (cond ((null? set) (newline) #t) (else (let ((res (interpretation (car set)))) (display "Formel: ") (display (car set)) (display " => ") (display (if res 1 0)) (if (prop-eval-set (cdr set) interpretation) res #f))))) ;; Ueberpruefe eine Menge von Klauseln unter einer Menge von ;; Interpretationen. Ergebnis ist #t genau dann, wenn alle Formeln ;; unter allen Interpretationen zu #t ausgewertet werden. (define (prop-validate-set set interpretations) (cond ((null? interpretations)) (else (let ((interpretation (car interpretations))) (display "Testing interpretation: ") (display-interpretation-atoms interpretation (get-formset-propvars set)) (newline) (let ((res (prop-eval-set set interpretation))) (display "Result: ") (display res) (newline) (if (prop-validate-set set (cdr interpretations)) res #f)))))) ;; Testformeln (Craig 1) (define f1 '(implies (and a (not b)) c)) (define f2 '(implies c (or a b))) (define f3 '(implies a (not c))) (define f4 '(or a (or b c))) ;; Testformeln (Craig 2) (define g1 '(or a (or b c))) (define g2 '(implies a (or (and b (not c)) (and (not b) c)))) (define g3 '(implies (not b) (not c))) (define g4 '(not (and b (and c (not a))))) (define g5 '(implies (not c) (not b))) ;; Beispielaufrufe (display "Beispiele") (newline) (define I1 (make-var-interpretation '(a b))) (display (prop-eval g2 I1)) (newline) (define I2 (make-var-interpretation '(a b c))) (display (prop-eval g2 I2)) (newline) ;; Berechne Craig 1 (define forms (list f1 f2 f3 f4)) ; (define forms (list g1 g2 g3 g4 g5)) (display (prop-validate-set forms (map make-eval-fun (map make-var-interpretation (powerset '(a b c)))))) (newline)