Implement a function called tautology? that takes as input a fully parenthesized formula and returns true if it is a tautology and false otherwise. As was the case in the previous lab, the formula will contain at least one set of parentheses for each operator, but may contain more. The best strategy for doing is to use an insight called Quine's method. It is based on the observation that if a formula, such as (p or (not p)), is a tautology, the result of substituting p with true is a tautology and the result of substituting p with false is also a tautology. This implies a computational strategy: to evaluate whether a formula F is a tautology 1. Collect all of the propositional variables. 2. Substitute every occurrence of the first variable with #t and every occurrence of the same variable with #f 3. Make two recursive calls to Tautology? “And” the results. 4. When all possible substitutions have been made, i.e., the formula contains only truth values, evaluate the formula and return the results. Racket code only please. No loops or hash, thank you Following those steps above, I have this code, but I am getting a lot of errors and am unsure how to fix it so the tests come out like they are supposed to. (define (atom? x) (and (not (null? x)) (not (pair? x)))) (define (tautology? formula) (let ((variables (find-variables formula))) (check-tautology? formula variables))) (define (find-variables formula) (cond ((null? formula) '()) ((atom? formula) (list formula)) ((eq? (car formula) 'not) (find-variables (cadr formula))) (else (append (find-variables (car formula)) (find-variables (cadr formula)))))) (define (check-tautology? formula variables) (if (null? variables) (evaluate-wff formula '()) (let* ((var (car variables)) (true-subst (Substitute var '#t formula)) (false-subst (Substitute var '#f formula))) (and (check-tautology? true-subst (cdr variables)) (check-tautology? false-subst (cdr variables)))))) (define Substitute (lambda (from to L) (cond ((null? L) '()) ((list? (car L)) (cons (Substitute from to (car L)) (Substitute from to (cdr L)))) (else (if (eq? (car L) from) (cons to (Substitute from to (cdr L))) (cons (car L) (Substitute from to (cdr L)))))))) (define evaluate-wff (lambda (L) (cond ( (list? L) (cond ((eq? (length L) 1) (evaluate-wff (car L))) ((eq? (length L) 2) (not (evaluate-wff (cdr L)))) (else (cond ((eq? (cadr L) 'or) (or (evaluate-wff (car L)) (evaluate-wff (caddr L))) ) ((eq? (cadr L) 'and) (and (evaluate-wff (car L)) (evaluate-wff (caddr L))) ) ((eq? (cadr L) 'implies) (or (not (evaluate-wff (car L))) (evaluate-wff (caddr L))) ) (else (eq? (evaluate-wff (car L)) (evaluate-wff (caddr L))))))) ) (else L)))) (define (lookup var env) (cond ((null? env) #f) ((eq? (caar env) var) (cdar env)) (else (lookup var (cdr env))))) (tautology? '(or (and p (not p)) (and (not p) p))) ;should return #t (tautology? '(or p (not p))) ;should return #t
Implement a function called tautology? that takes as input a fully parenthesized formula and returns true if it is a tautology and false otherwise. As was the case in the previous lab, the formula will contain at least one set of parentheses for each operator, but may contain more.
The best strategy for doing is to use an insight called Quine's method. It is based on the observation that if a formula, such as (p or (not p)), is a tautology, the result of substituting p with true is a tautology and the result of substituting p with false is also a tautology. This implies a computational strategy: to evaluate whether a formula F is a tautology
1. Collect all of the propositional variables.
2. Substitute every occurrence of the first variable with #t and every occurrence of
the same variable with #f
3. Make two recursive calls to Tautology? “And” the results.
4. When all possible substitutions have been made, i.e., the formula contains only
truth values, evaluate the formula and return the results.
Racket code only please. No loops or hash, thank you
Following those steps above, I have this code, but I am getting a lot of errors and am unsure how to fix it so the tests come out like they are supposed to.
(define (atom? x)
(and (not (null? x))
(not (pair? x))))
(define (tautology? formula)
(let ((variables (find-variables formula)))
(check-tautology? formula variables)))
(define (find-variables formula)
(cond ((null? formula) '())
((atom? formula) (list formula))
((eq? (car formula) 'not) (find-variables (cadr formula)))
(else (append (find-variables (car formula))
(find-variables (cadr formula))))))
(define (check-tautology? formula variables)
(if (null? variables)
(evaluate-wff formula '())
(let* ((var (car variables))
(true-subst (Substitute var '#t formula))
(false-subst (Substitute var '#f formula)))
(and (check-tautology? true-subst (cdr variables))
(check-tautology? false-subst (cdr variables))))))
(define Substitute
(lambda (from to L)
(cond
((null? L) '())
((list? (car L))
(cons
(Substitute from to (car L))
(Substitute from to (cdr L))))
(else
(if (eq? (car L) from)
(cons to
(Substitute from to (cdr L)))
(cons (car L)
(Substitute from to (cdr L))))))))
(define evaluate-wff
(lambda (L)
(cond ( (list? L)
(cond
((eq? (length L) 1)
(evaluate-wff (car L)))
((eq? (length L) 2)
(not (evaluate-wff (cdr L))))
(else
(cond
((eq? (cadr L) 'or)
(or
(evaluate-wff (car L))
(evaluate-wff (caddr L))) )
((eq? (cadr L) 'and)
(and
(evaluate-wff (car L))
(evaluate-wff (caddr L))) )
((eq?
(cadr L) 'implies)
(or
(not (evaluate-wff (car L)))
(evaluate-wff (caddr L))) )
(else
(eq?
(evaluate-wff (car L))
(evaluate-wff (caddr L))))))) )
(else L))))
(define (lookup var env)
(cond ((null? env) #f)
((eq? (caar env) var) (cdar env))
(else (lookup var (cdr env)))))
(tautology? '(or (and p (not p)) (and (not p) p))) ;should return #t
(tautology? '(or p (not p))) ;should return #t
![18 (define (check-tautology? formula variables)
(if (null? variables)
TT
68
19
20
21
22
23
24
25
26
27 (define Substitute
28
(lambda (from to L)
(cond
29
30
31
32
33
34
35
(evaluate-wff formula '())
let* ((var (car variables))
(true-subst (Substitute var '#t formula))
(false-subst (Substitute var '#f formula)))
(and (check-tautology? true-subst (cdr variables))
(check-tautology? false-subst (cdr variables))))))
((null? L) '(())
((list? (car L))
(cons
(Substitute from to (car L))
(Substitute from to (cdr L))))
(else
Welcome to DrRacket, version 8.7 [cs].
Language: racket, with debugging; memory limit: 128 MB.
evaluate-wff: arity mismatch;
the expected number of arguments does not match the given number
expected: 1
given: 2](/v2/_next/image?url=https%3A%2F%2Fcontent.bartleby.com%2Fqna-images%2Fquestion%2Ff299e2b3-0e23-436d-897a-625b7f1eac0b%2F5a094515-fd06-4dd3-b68b-ae81b38f59c6%2Fcaw9pqn_processed.jpeg&w=3840&q=75)
Trending now
This is a popular solution!
Step by step
Solved in 4 steps
