CISC 360 Assignment 3
due Monday, 2023–03–20 at 11:59pm, via onQ
Jana Dunfield March 5, 2023
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 file must compile
Your file must load (:load in 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 Ifyouchoosetoworkinagroupof2
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.
a3, Jana Dunfield, CISC 360, W. 2023 1 2023/3/5
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
| Bot
-- truth (always true)
-- falsehood (contradiction)
-- conjunction
-- disjunction
| And Formula Formula
| Or Formula Formula
| Implies Formula Formula -- implication
| Not Formula
| Atom Variable
deriving (Eq, Show)
-- negation
-- atomic proposition ("propositional variable")
a3, Jana Dunfield, CISC 360, W. 2023
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 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).
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 pos- sible valuations 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
a3, Jana Dunfield, CISC 360, W. 2023 3 2023/3/5
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:
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.)
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.
a3, Jana Dunfield, CISC 360, W. 2023 4 2023/3/5
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
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 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 in ctx.)
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"]
a3, Jana Dunfield, CISC 360, W. 2023 5 2023/3/5
(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.)
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.
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 (∈) 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.
a3, Jana Dunfield, CISC 360, W. 2023 6 2023/3/5
phi ∈ ctx
ctx ? phi UseAssumption
ctx ? Top Top-Right phi : ctx?psi
ctx ? Implies phi psi Implies-Right ctx ? phi2
ctx ? Or phi1 phi2 Or-Right-2
ctx?phi1 ctx?phi2 ctx ? And phi1 phi2
And-Right
ctx ? phi1
ctx ? Or phi1 phi2 Or-Right-1
ctx1 ++ [phi1] ++ ctx2 ? phi
ctx1 ++ [Or phi1 phi2] ++ ctx2 ? phi
ctx1 ++ [phi1, phi2] ++ ctx2 ? phi
ctx1 ++ [And phi1 phi2] ++ ctx2 ? phi And-Left
ctx1 ++ [phi2] ++ ctx2 ? phi
Or-Left
ctx1 ++ ctx2 ? phi1 ctx1 ++ [phi2] ++ ctx2 ? psi ctx1 ++ [Implies phi1 phi2] ++ ctx2 ? psi
Implies-Left
ctx1 ++ [Bot] ++ ctx2 ? phi Bot-Left
ctx1 ++ ctx2 ? psi ctx, phi ? Bot
ctx1 ++ [Not psi] ++ ctx2 ? Bot Not-Left ctx ? Not phi Not-Right Figure 1 Rules to implement within prove core and prove left
a3, Jana Dunfield, CISC 360, W. 2023 7 2023/3/5
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.
11. ‘Not-Left’ says that if Not psi is an assumption, and we can prove psi (without the assumption Not psi), then we have proved Bot.
12. ‘Not-Right’ says that if we can prove Bot under the assumption phi, then we have proved Not 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 Figure 1.
Note: As usual, we may test your code using additional test cases that we do not make available to you.
3.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.
a3, Jana Dunfield, CISC 360, W. 2023 8 2023/3/5
3.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.
This is the end of the main assignment. There is a bonus question on the next page.
a3, Jana Dunfield, CISC 360, W. 2023 9 2023/3/5
4 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 Figure 1, write rules for universal quantification over natural numbers ?X φ. 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 , 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? (For example, can it do proofs by induction?)
a3, Jana Dunfield, CISC 360, W. 2023 10 2023/3/5