#lang racket
;; Starter code for A4Q2
;; May contain Unicode characters - download, don't cut/paste from browser

;; Repeated from A4Q1-starter.rkt:

;; Here is the grammar for formulas or expressions in propositional logic,
;; represented as fully-parenthesized S-expressions.

;; expr = X [not ⊥]
;;      | (T -> T)
;;      | (T ∧ T)
;;      | (T ∨ T)
;;      | (¬ T)

;; A Kripke model (km) is an S-expression that satisfies the following grammar:
;; km = (symbol [var ...] km ...)
;; The symbol is the root label,
;; the list of variables are the ones forced at this node,
;; and the rest of the list is the children of the root.

;; The valid? function checks the monotonicity condition (every variable in the root list of a Kripke model
;; must appear in the root lists of its descendants) and that ⊥ is not used as a variable.

;; valid? : km -> boolean

;; We want to know whether or not a given formula is forced at the root of a Kripke model.

;; forced-at? : expr km -> boolean

;; Replace each quoted question mark below with a km representing a Kripke model.
;; The required conditions are that
;; (valid? answer) is #t and (forced-at? formula answer) is #f.

;; LACI suggests that you write out a justification of your model on paper
;; before confirming it with your answer to A4Q1.
;; You don't have to submit the handwritten justification, but I recommend this approach.


;; answer1 for the DNE formula: '((¬ (¬ A)) -> A)

(define answer1 '?)

;; answer2 for the Peirce formula: '(((A -> B) -> A) -> A)

(define answer2 '?)

;; answer3 for the deMorgan formula: '((¬ (A ∧ B)) -> ((¬ A) ∨ (¬ B)))

(define answer3 '?)

;; answer4 for the 'some implication' formula: '((A -> B) ∨ (B -> A))

(define answer4 '?)