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

Database System Concepts

7th Edition

ISBN:9780078022159

Author:Abraham Silberschatz Professor, Henry F. Korth, S. Sudarshan

Publisher:Abraham Silberschatz Professor, Henry F. Korth, S. Sudarshan

Chapter1: Introduction

Section: Chapter Questions

Problem 1PE

See similar textbooks

Related questions

Question

100%

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

Expert Solution

Trending now

This is a popular solution!

Step by step

Solved in 4 steps

SEE SOLUTION Check out a sample Q&A here

Knowledge Booster

Learn more about

Need a deep-dive on the concept behind this application? Look no further. Learn more about this topic, computer-science and related others by exploring similar questions and additional content below.