1 Homework 1

Released: Wednesday, January 11, 2023 at 6:00pm

Due: Wednesday, January 18, 2023 at 6:00pm

What to Download:

https://github.com/logiccomp/s23-hw1/raw/main/hw1.rkt

Please start with this file, filling in where appropriate, and submit your homework to the HW1 assignment on Gradescope. This page has additional information, and allows us to format things nicely.

1.1 Problem 1

We can express propositional logic using boolean functions in ISL-Spec, a language you are familiar with from Fundamentals 1 (as it’s essentially the same as ISL+, which you used). Most are built in, but some we will define. See the following table, which lists the logical operator and the corresponding ISL-Spec function (or definition, if it’s not built in).

For example, P \land Q can be expressed as the following function:

(define (p1 P Q)

(and P Q))

Translate the following expressions in logic into corresponding function definitions, named p2,p3, p4. Note that the number (and names) of arguments may be different for the different expressions, as they do not all use the same variables.

Template code (included in file linked at top of page):

;; (P /\ Q) \/  ~(R /\ S)
(define (p2 ...) ...)

;; P -> ~Q
(define (p3 ...) ...)

;; ~(Q /\ ~Q) = T
(define (p4 ...) ...)

1.2 Problem 2

Just as we can express propositional logical statements as code, we can also express proofs about propositional logic in code. These proofs are often written as truth tables, with the goal to show that a given expression is always true (or maybe is never true) regardless of the assignment of variables. You can do this by enumerating, in a table, all possible assignments of variables.

For example, if we wanted to know that P \land \neg P is false or unsatisfiable (i.e., for all possible assignments of variables, the result in false), we can define the following truth table to prove it:

Here we see, regardless of whether we assign T or F to P, our expression ends up F.

To do this in code, we can express each row of the truth table as a unit test. We can define the above expression as:

(define (p1 P)

(and P (not P)))

And then write the two lines of the truth table:

(check-expect (p1 #t) #f)

(check-expect (p1 #f) #f)

This then corresponds to a proof that is verified by running those tests. If one of our cases were wrong, we would get a test failure.

For this problem, you should prove that the two following equalities (these are De Morgan’s Laws) hold for all possible assignments (i.e., are valid) by first defining them (p5 and p6) and then defining their truth tables using check-expect. Remember to include all possible combinations of inputs!

Template code (included in file linked at top of page):

;; ~(P /\ Q) = ~P \/ ~Q
(define (p5 ...) ...)
(check-expect (p5 ...) ...)
; ...

;; ~(P \/ Q) = ~P /\ ~Q
(define (p6 ...) ...)
(check-expect (p6 ...) ...)
; ...

1.3 Problem 3

We’ve seen that logical implication (\Rightarrow) can be defined in terms of \land and \neg (including in the table in Problem 1).

It turns out, there are many cases when you can define one operator in terms of another.

In this exercise, for each operator, define a version of it in terms of just if. For example, \neg P, would be represented as (define (op_neg P) (if P #f #t)). You are welcome to validate your encodings using truth-table tests, but you are not required.

Note: all of these operators should be binary (take two arguments), even if some of them may have a possibly interpretation with more than two arguments.

Template code (included in file linked at top of page):

;; /\
(define (op_and ...) ...)

;; \/
(define (op_or ...) ...)

;; ->
(define (op_implies ...) ...)

;; =
(define (op_equal ...) ...)

;; ⊕ (exclusive or)
(define (op_xor ...) ...)

1.4 Problem 4

Simplifying propositional formulas is an important topic, as simpler formulas, especially if they have fewer variables, are easier to check for validity (truth), unsatisfiability (falsehood), etc.

For example, if I have the expression P \land (Q \lor \neg Q), we can see that the subexpression Q \lor \neg Q will always be true, no matter the assignment of Q, and thus we could first simplify this to P \land T. But since P \land T is equivalent to just P, we can further simplify.

In code, what this means is that the function:

(define (p7 P Q)

(and P (or Q (not Q))))

Is equivalent to the function:

(define (p7s P Q) P)

And we can check that using a truth table, which has four rows since there are two variables.

(check-expect (p7 #t #t) (p7s #t #t))

(check-expect (p7 #t #f) (p7s #t #f))

(check-expect (p7 #f #t) (p7s #f #t))

(check-expect (p7 #f #f) (p7s #f #f))

Here we left Q as an input to p7s to make it obvious that the truth table test is showing they are equivalent on all inputs. Note that it is of course equivalent to a function that does not have the extra argument, but the truth table may be harder to understand, so for this problem, we will write our simplified versions in this more verbose form, even when we can eliminate variables.

Your task, in this problem, is to perform simplifications of this form for the three problems below, and include truth tables that confirm that your simplifications were correct. We are giving you the expressions written both in logical syntax and in the ISL-Spec code that we expect you to simplify & test with.

Template code (included in file linked at top of page):

;; (P /\ R) \/ (Q /\ ~Q)
(define (p9 P Q R)
  (or (and P R) 
      (and Q (not Q))))
(define (p9s P Q R) 
  ...)

;; (P /\ Q /\ P) \/ (Q /\ R)
(define (p10 P Q R)
    (or (and P Q P) 
        (and Q R)))
(define (p10s P Q R)
    ...)

;; (P /\ Q /\ R) \/ (~Q /\ S /\ Q)
(define (p11 P Q R S)
    (or (and P Q R)
        (and (not Q) S Q)))
(define (p11s P Q R S)
  ...)