Reminder: All work submitted must be your own, or, if you are working with one other student, your teammate’s.

Late policy: Assignments submitted up to 24 hours late (that is, by 11:59 pm the following day) will be accepted without penalty.  Assignments submitted more than 24 hours late will not be accepted, except through an accommodation or a consideration.

0    IMPORTANT: Your ile must compile

Your file must load (:loadin GHCi) successfully, or we will subtract 30% from your mark.

If you are halfway through a problem and run out of time, comment out the code that is

causing :load to fail by surrounding it with {- . . .  -}, and write a comment describing what you were trying to do. We can often give (partial) marks for evidence of progress towards a solution, but we need the file to load and compile.

0    If you choose to work in a group of 2

You must use version control (such as GitHub, GitLab, Bitbucket, etc.).  This is primarily to help you maintain an equitable distribution of work, because commit logs provide information about the members’ level of contribution.

Your repository must be private—otherwise, anyone who has your GitHub (etc.) username can copy your code, which would violate academic integrity.  However, upon request from the course staff, you must give us access to your repository.  (You do not need to give us access unless we ask.)

We only need one submission of the assignment (“Assignment 3”).  However, each of you must submit a brief statement.

1.  Give your names and student ID numbers.

2. Estimate the number of hours you spent on the assignment.

3. Briefly describe your contribution, and your teammate’s contribution.   (Coding,  trying to understand the assignment, testing, etc.)

This is meant to ensure that both group members reflect on their relative contributions.

If you do not submit a statement, you will not receive an assignment mark.  This is meant to ensure that each group member is at least involved enough to submit a statement. Each member must submit a statement.

0    Be careful with library functions

Haskell has a rather large built-in library. This assignment is not about how to find library functions, but about how to use some of the core features of Haskell. You will not receive many marks if you just call a library function that solves the whole problem. The point is to solve the problem yourself.

If you are not sure whether you are calling a library function that solves the whole problem, contact the instructor. Note that if we suggest a library function, you may certainly use it.

(The only way I know to avoid this issue is to craft problems that are complicated and arbitrary, such that no library function can possibly solve them. I don’t like solving complicated and arbitrary problems, and you probably don’teither.)

0    Add your student ID

Begin by renaming the file to a3-studentid.hs.  For example, if your student ID number were 87654321, you should rename the file to a3-87654321.hs.

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

--  Rename  this  file  to  include  your  student  ID:  a3-studentid.hs

--  Also,  add  your  student  ID  number  after  the  "=":

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, uncomment the “second student id” line and add the second student’s ID number there.

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

|   Bot

|  And  Formula  Formula

|   Or  Formula  Formula

|   Implies  Formula  Formula |  Not  Formula

|  Atom  Variable

deriving  (Eq,  Show)

--  truth  (always  true)

--  falsehood  (contradiction)

--  conjunction

--  disjunction

--  implication

--  negation

--  atomic  proposition  ("propositional  variable")

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    Q1:  Horn clauses

2.1   Q1a:  classify

The function classify should take a Formula and return a result distinguishing whether the For- mula is a “fact” (an Atom), a “rule” (an implication whose left-hand side is a conjunction, and whose right-hand side is an Atom), or neither.

(When we get to Prolog—very soon—Prolog “clauses” are either facts or rules; this question is intended to help you understand what Prolog clauses are.)

For details and examples, see a3.hs.

2.2   Q1b: Testing classify

Input coverage means that for each “shape” of input to classify, there is at least one test case pro- viding that input. What counts as a “shape” is not clearly defined; testing every possible constructor of ’Formula’ may be sufficient.

Output coverage means that for each “shape” of output from classify, there is at least one test case checking that classify returns that output. Defining “shape” is easier here, because the output of classify has type FormulaKind.  Therefore you need at least one test case in which classify should return Fact, one test case in which classify should return Rule, and one test case in which classify should return NotClause.

Code coverage means that every part of your code gets tested.  For example, if your code for classify has a clause whose body is NotClause, you need at least one test case that makes that clause run (steps into that body).

A single test case may satisfy a combination of input, output, and code coverage.

We have provided one test case, test classify1 .   Name your test cases test classify2 , test classify3, etc., and add them to the list in test classify .

You don’t have to explain why you chose your test cases, but an explanation may increase your marks if we think your tests are incomplete.

3    Q2:  Truth tables

3.1   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 consid- ered 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).

3.2   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]

3.3   Q2b: getValuations

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

For example, getValuations  ["A",  "B"] should return a list containing the four possible val- uations:

1.  one valuation in which both "A" and "B" are True

2.  one valuation in which both "A" and "B" are False

3.  one valuation in which "A" is True and "B" is False

4.  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.

3.4   Q2c: evalF

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

1.  If phi is Top, then evalF returns True. (Already written for you.)

2.  If phi is Bot, then evalF returns False. (Already written for you.)

3.  If phi is Not  psi, then evalF returns the negation of evalF  psi. (Already written for you.)

4.  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.

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

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

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

3.5   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.

4    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 inctx

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 ques- tion, you need to understand and follow the inference rules in Figure 1.)

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

2.  [Atom  "A"]「 Atom  "A" is provable, because we are assuming the propositional variable A is true.

3.  [Atom  "A"]「 Atom  "B" is not provable, because knowing that the variable A is true tells us nothing about whether B is true.

4.  [Atom  "A", Atom  "B"]「 And   (Atom  "B")   (Atom  "A") is provable, because we are assuming A, and assuming B.

5.  [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.

6.  []「 Implies  (Atom  "A")  (Atom  "A") is provable:

(a) To see if []「 Implies  (Atom  "A")  (Atom  "A") is true, we suppose  (assume) the an- tecedent 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, theyaren’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.) 

7.  [Implies  (Atom  "A")   (Atom  "B"), Atom  "A"] 「  Atom  "B"  is  provable:   we have two as- sumptions, one that A implies B, and a second assumption that A is true.  By these assump- tions, B is true. To show this, we reduce the problem to

[Atom  "B", Atom  "A"]「 Atom  "B"

Why can we do that?  We are assuming that A implies B, but we know A  (because we are assuming it).  So we produce some new knowledge—that B is true—and add it to the as- sumptions.

In this specific setting, it is legitimate to replace the assumption Implies  (Atom  "A")   (Atom "B") with Atom  "B", which is the consequent of the implication.

Expressed as inference rules, the rules we want to implement are shown in Figure 1.

phi 2 ctx

ctx「 phi

ctx「 phi1       ctx「 phi2

ctx「 And phi1 phi2

ctx「(ct)O(x)r「phi1(phi)p(1)hi2 Or-Right-1

 Top-Right

ctx「 Top

ctx 「(ct)O(x)r「phi1(phi)2phi2 Or-Right-2

ctx1 ++ [phi1] ++ ctx2「 phi       ctx1 ++ [phi2] ++ ctx2「 phi ctx1 ++ [Or phi1 phi2] ++ ctx2「 phi

Or-Left

And-Left

ctx1 ++ ctx2「 phi1       ctx1 ++ [phi2] ++ ctx2「 psi ctx1 ++ [Implies phi1 phi2] ++ ctx2「 psi

Implies-Left

ctx1 ++ [Bot] ++ ctx2「 phi Bot-Left

Figure 1  Rules to implement within prove core and prove left

We attempt to explain these rules in English. In each rule, the conclusion of the rule is below the line, and the premises (if any) are above the line.

1.  ‘UseAssumption’ says that if we are trying to prove a formula, and the formula appears in (2) our list of assumptions, then it is provable: we have assumed exactly that formula.

2.  ‘Top-Right’ says that the true formula is always provable.

3. ‘And-Right’ says that a conjunction is provable if both subformulas phi1 and phi2 are provable

(And-Right has one premise for phi1, and one premise for phi2).

This corresponds to the ^i rule in CISC 204.

4.  ‘Implies-Right’ says that an implication is provable if, assuming the antecedent, we can prove the consequent.   The premise is written using Haskell’s “cons” notation:  we  add the  an-

tecedent phi to the list of assumptions ctx and try to prove the consequent psi. This corresponds to the !i rule in CISC 204.

5.  ‘Or-Left’ says that if we’re assuming a disjunction Or  phi1  phi2 is true, we can “case-split”

on it: prove the goal under assumption phi1, and also under assumption phi2. This corresponds to the__e rule in CISC 204.

6.  ‘Or-Right-1’ says that a disjunction is provable if its first subformula, psi1, is provable. This corresponds to the__i1 rule in CISC 204.

7.  ‘Or-Right-2’ says that a disjunction is provable if its second subformula, psi2, is provable. This corresponds to the__i2 rule in CISC 204.

8. ‘And-Left’ says that if we are assuming a conjunction, we should “decompose” the conjunction to bring out each of the subformulas phi1 and phi2 as a separate assumption.

This corresponds roughly to the ^e1 and ^e2 rules being used simultaneously in CISC 204 (if that were allowed).

9.  ‘Implies-Left’ says that if we are assuming that phi1 implies phi2, and (first premise) the antecedent phi1 is provable, and (second premise) we can prove psi assuming phi2, then psi is provable under our original assumptions ctx1 ++ [Implies phi1 phi2] ++ ctx2.

This corresponds roughly to the !e rule in CISC 204.

10.  ‘Bot-Left’ says that if Bot is an assumption, then we can prove any phi.

A general explanation of how to turn inference rules into code is beyond the scope of this assignment, and this particular set of rules is subtle, so we have given you a framework to build upon.

This framework uses continuations to handle the “search” aspect of the problem: we are search- ing for a proof using the rules in Figure1.

Note: As usual, we may test your code using additional test cases that we do not make available to you.

4.1   What you need to do

Fill in the undefined parts in prove core and prove left .  Some of the rules are already imple- mented for you; you should examine the existing code to figure out what to do.

When you call kSucceed, you need to pass two arguments:

•  a Derivation;

•  a “more function” that can be called to get additional proofs (additional derivations).

A Derivation represents the structure of the proof found. For example, if the code is trying to prove vC given the context  [vB,  vC], then the proof that uses the rule UseAssumption is repre- sented by

UseAssumption  vC

If we are trying to prove Or  vC  vC using the context  [vB,  vC], there is more than one pos- sible proof (and prove all should return all of them); one of the possible proofs uses the rule UseAssumption, followed by the rule OrRight-1, which is represented by the derivation

OrRight  1  (UseAssumption  vC)

When you call prove core or prove left, you need to pass two continuations: a success con - tinuation and a failure continuation. Often, the failure continuation needs to be a “more function”. For example, in the code for Implies-Left, which is already given to you, we pass more1 as the failure continuation in the second call to prove   core.

4.2   More CISC 204 notes

The function prove core implements backward reasoning: it looks at the shape of the conclusion (the formula after the turnstile symbol “「”), and tries to do the last step of the proof, which tells it what the next-to-last step in the conclusion should be.

The function prove left implements forward reasoning on premises (assumptions) .

The job of alternating between backward and forward reasoning is implemented in the structure of the two functions prove core and prove right .

5    Q4: Theorem  Prover Bonus

You can get full marks on the assignment without doing this bonus part; you might get a total assignment grade over 100% by doing this bonus question; but this bonus question is worth no more than 5% of the marks for the assignment.

This question is not expected to have an easy answer, so don’t attempt it unless you really want to.

If you attempt this question, submit your answers in a separate file named a3bonus.hs.  (This is to make sure you don’t create bugs that would cause you to lose marks on the main assignment.)

Q4a: In the style of Figure1, write rules for existential quantification over natural numbers 9X '. You will probably want to adapt material from CISC 204 or other work on logic; if you do, give the source of the rules.

Q4b:  Extend the Formula type with appropriate constructors to represent 9, predicates, and quantified variables X. You may need to declare some other types.

Q4c: Write some test cases.

Q4d:  Implement your rule(s) within prove core and prove left, adding helper functions if required.  (Hint:  substitution '[t/X], which replaces occurrences of the variable X with a term t throughout the formula ', was an important operation in CISC 204-style natural deduction.)

Q4e:  Discuss your rules and implementation.  Do you think your implementation can prove every true sequent involving existentials?