计算机代写｜CISC 360 Assignment 3

这是一篇来自加拿大的关于CISC 360的计算机代写，以下是具体作业内容详情：

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:

Top, which is always true (sometimes written ⊤)
Bot, which is always false (sometimes written ⊥)
Not phi, representing negation (¬φ)
And phi1 phi2, representing conjunction (φ1 ∧ φ2)
Or phi1 phi2, representing disjunction (φ1 ∨ φ2)
Implies phi psi, representing implication (φ → ψ or φ ⊃ ψ: “if φ (phi) then ψ (psi)”)
Atom v, representing a propositional variable (“atomic formula”, or “propositional constant”) named v.

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

Implies

/ \

Bot And

/ \

vA vB

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:

one valuation in which both “A” and “B” are True
one valuation in which both “A” and “B” are False
one valuation in which “A” is True and “B” is False
one valuation in which “A” is False and “B” is True

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:

If phi is Top, then evalF returns True. (Already written for you.)
If phi is Bot, then evalF returns False. (Already written for you.)
If phi is Not psi, then evalF returns the negation of evalF psi. (Already written for you.)
If phi is Atom v, then evalF should look up v in the valuation valu, and return the associated boolean. For example, evalF [(“B”, False)] (Atom “B”) should return False.

If phi is And phi1 phi2, then evalF should return True if and only if evalF returns True for both phi1 and phi2 (under the same valuation valu).

If phi is Or phi1 phi2, then evalF should return True if and only if evalF returns True for either phi1 or phi2 (under the same valuation valu).

If phi is Implies phi1 phi2, then evalF should return True if and only if either

evalF returns False on phi1, or
evalF returns True on phi2.

(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.)

[] ⊢ Top is provable, because Top is always true. (In fact, ctx ⊢ Top is provable regardless of what assumptions are in ctx.)

[Atom “A”] ⊢ Atom “A” is provable, because we are assuming the propositional variable A is true.

[Atom “A”] ⊢ Atom “B” is not provable, because knowing that the variable A is true tells us nothing about whether B is true.

[Atom “A”, Atom “B”] ⊢ And (Atom “B”) (Atom “A”) is provable, because we are assuming A, and assuming B.

[And (Atom “A”) (Atom “B”)] ⊢ And (Atom “B”) (Atom “A”) is provable, because we are assuming A ∧ B, and the only way that A ∧ B could be true is if both A and B are true.

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

[] ⊢ Implies (Atom “A”) (Atom “A”) is provable:

(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.)

程序辅导定制C/C++/JAVA/安卓/PYTHON/留学生/PHP/APP开发/MATLAB