计算机代写｜CISC 360 Assignment 3

1 Add your student ID

The file a3.hs will not compile until you add your student ID number by writing it after the =:

— Your student ID:

student_id :: Integer

student_id =

You do not need to write your name. When we download your submission, onQ includes your

name in the filename.

If you are working in a group of 2, put the second student ID in a comment, like this:

— Your student ID:

student_id :: Integer

student_id = 11112222 — 33334444

2 Q2: Truth tables

2.1 Formulas

In this assignment, we represent a logical formula as the data type Formula. Every Formula has one of the following forms:

type Variable = String

data Formula = Top — truth (always true)

| Bot — falsehood (contradiction)

| And Formula Formula — conjunction

| Or Formula Formula — disjunction

| Implies Formula Formula — implication

| Not Formula — negation

| Atom Variable — atomic proposition (“propositional variable”)

deriving (Eq, Show)

For example, if vA, vB and formula2 are defined as follows:

vA = Atom “A”

vB = Atom “B”

formula2 = Implies Bot (And vA vB)

then formula2 represents “if false then (A and B)”, and can be drawn as the tree

2.2 Valuations and truth tables

A Valuation maps each atomic proposition variable to a Boolean:

type Valuation = [(Variable, Bool)]

For example, the valuation [(“A”, False), (“B”, True)] indicates that Atom “A” is considered false, and Atom “B” is considered true. Under this valuation, the formula And vA vB would be false (because vA is False in the valuation), but the formula Implies vA vB would be true (because vB is true in the valuation).

2.3 Q2a: getVariables

Complete the function getVariables, which gathers all the variables (like “A”, “B”, etc.) that appear in a formula. getVariables should never return any duplicates: given the formula And vA vA, that is, And (Atom “A”) (Atom “A”), your implementation of getVariables should return

[“A”], not [“A”, “A”].

(Hint: Read the comment in a3.hs about the Haskell library function nub.)

getVariables :: Formula -> [Variable]

2.4 Q2b: getValuations

Complete the function getValuations, which—given a list of variables (strings)—returns all possible valuations of True and False.

For example, getValuations [“A”, “B”] should return a list containing the four possible valuations:

The order of the valuations in the output doesn’t matter.

getValuations :: [Variable] -> [Valuation]

Hint: Think carefully about the base case when the argument (list of variables) is empty. If there are no variables, there is one possible valuation, which is the empty valuation (empty list).

That is not the same as saying there are no valuations; if there are no valuations, you should return the empty list, but if there is one possible valuation you should return a list whose only element is that one valuation.

2.5 Q2c: evalF

Complete the function evalF which, given a valuation valu and a formula phi, evaluates the formula phi as follows:

(This is the same idea as the CISC 204 “material implication” equivalence φ → ψ ≡ ¬φ∨ψ.)

(This part is already written for you.)

2.6 Testing Q2

Once you have completed all three functions above, you can use our function buildTable to test them by printing a truth table with all possible valuations. For example, calling buildTable on And vA vB should produce a table with four rows, with all possible valuations of A and B, such that the right-hand “result” is True only when both A and B are true.

3 Q3: Tiny Theorem Prover

This question uses some of the same types as Q2, but in a rather different way.

You will implement a function prove that takes a context containing formulas that are assumed  to be true. If the formula can be proved according to the rules given below then prove should return True. Otherwise, it should return False.

We are not interested only in whether a thing is true or false, but why, so the Tiny Theorem Prover also generates derivations that represent (part of) the proof that was found. The function prove all returns a list of all the proofs found.

Both prove and prove all call other functions to do the central work.

If phi is a formula, and ctx is a context (list of assumptions), then we write

ctx ⊢ phi

to mean that phi is provable (“true”) under the assumptions in ctx

Warning: the notation in this question varies substantially from that in CISC 204. The notation used in this problem is similar to that used in the second half of Gerhard Gentzen’s dissertation— which is not the half that CISC 204’s “natural deduction” comes from. The second half of Gentzen’s dissertation describes sequent calculus. Like 204, sequent calculus includes sequents; a sequent is a list of premises (written before the “turnstile” symbol ⊢) along with a conclusion (written after the⊢). Unlike 204 (at least when I taught it), the rules of sequent calculus operate by manipulating the sequent, rather than by constructing a line-numbered proof.

First, let’s look at some examples. (These are just examples. To correctly implement this question, you need to understand and follow the inference rules in Figure 1.)

Therefore, B is true, and A is true, so B ∧ A is true.

(a) To see if [] ⊢ Implies (Atom “A”) (Atom “A”) is true, we suppose (assume) the antecedent of the implication, which is Atom “A”, and then prove the consequent, Atom “A”. We do this by “reducing” the problem to

[Atom “A”] ⊢ [Atom “A”]

(A difference between sequent calculus and 204’s natural deduction is that, while premises and assumptions are pretty similar in natural deduction, they aren’t considered the same.

For example, you might lose marks in 204 if you claimed you were using a premise when you were actually using an assumption introduced by the rule →i. Sequent calculus does not distinguish these: an assumption added using “Implies-Right”, which is the sequent calculus equivalent to

→i, is added to the list of premises in the sequent.)