2 Q2: Implication Form
2.1 Formulas
Copyright By PowCoder代写 加微信 powcoder
In this assignment, we represent a logical formula using Prolog atoms. Every formula is one of the
following:
• top, representing truth (written⊤ in 204)
• bot, representing falsehood (written⊥ in 204)
• and(P1,P2), representing conjunction P1 ∧ P2
• or(P1,P2), representing disjunction P1 ∨ P2 (only used in the bonusquestion)
• implies(P,Q), representing implication P
• not(P), representing negation: ¬P
Q: “if P thenQ”
• v(V), representing an atomic proposition V, where V is an atom like a, b or d
For example,
implies(bot, and(v(a), v(b)))
represents “if false then (a and b)”, and can be drawn as the tree
The questions Q2a, Q2b, and Q2c are explained in comments in a5.pl.
3 Q3: Tiny Theorem Prover
You will finish implementing a predicate prove that takes a context Ctx containing
formulas that are ASSUMED to be true. If the formula P can be proved ACCORDING to the rules given
below then prove should be satisfied, that is, the query prove(Ctx, P, R) should be true and Deriv
should contain a DERIVATION representing the rules used.
If P is a formula, and Ctx is a context (list of assumptions), then we write
to mean that P is provable (“true”) under the assumptions in Ctx. For example:
1. [] top is provable, because top is ALWAYS true. (So in fact, Ctx top isprovable regardless
of what assumptions are in Ctx.)
2. [] ⊢ bot is not provable, because bot is false and we have no assumptions.
3. [v(a)] ⊢ v(a) is provable, because we are assuming the propositional variable a is true.
4. [v(a)] v(b) is not provable, because knowing that a is true tells us nothing about whether
b is true.
5. [v(a),v(b)] ⊢and(v(b), v(a)) is provable, becausewe are assuminga, and assumingb.
6. [and(v(a), v(b))] and(v(b), v(a)) is provable, becausewe are assumingA∧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.
7. []⊢ implies(v(a), v(a)) is provable:
(a) To see if [] implies(v(a), v(a) is true, we suppose (assume) the antecedent of
the implication, which is v(a), and then prove the consequent, v(a). We do this by
“reducing” the problem to
[v(a)] ⊢ [v(a)]
8. [implies(v(a), v(b)), v(a)] v(b) is provable: we have two assumptions, one that A
implies B, and a second assumption that A is true. By these assumptions, B is true. To show
this, we reduce the problem to
[v(b), v(a)] ⊢ v(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(v(a),
v(b) with v(b), which is the consequent of the implication. (This does not
hold for many specific logics, but I am confident it holds for this one. If I am wrong,
you will still get full marks for implementing this.)
Expressed as inference rules, the rules to implement are:
UseAssumption
Ctx ⊢ Q1 Ctx ⊢Q2
[P | Ctx]⊢Q
Implies-Right
Ctx⊢top Ctx⊢and(Q1,Q2) Ctx ⊢ implies(P, Q)
Ctx1++ [P1,P2]++Ctx2⊢Q
Ctx1 ++ [and(P1, P2)] ++Ctx2 ⊢ Q
Ctx1++Ctx2⊢P1 Ctx1 ++ [P2] ++Ctx2 ⊢ Q
Implies-Left
Ctx1 ++ [implies(P1, P2)] ++Ctx2 ⊢ Q
Weattempt 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 Q1 and Q2 are provable
(And-Right has one premise for Q1, and one premise for Q2).
4. ‘Implies-Right’ says that an implication is provable if, assuming the antecedent, we can prove
the consequent. The premise is written using Prolog’s “cons” notation: we add the antecedent
P to the list of assumptions Ctx and try to prove the consequent Q.
5. ‘And-Left’ says that if we are ASSUMING a conjunction, we should “decompose” the conjunction
to bring out each of the subformulas P1 and P2 as a separate assumption.
6. ‘Implies-Left’ says that if we are ASSUMING that P1 implies P2, AND (first premise) the an-
tecedent P1 is provable, AND (second premise) we can prove Q assuming P2, then Q is prov-
able under our original assumptions Ctx1 ++ [implies(P1,P2)] ++Ctx2.
Unlike the Haskell version of this question, EACH rule CAN be written AS A
SINGLE Prolog CLAUSE. There is no need to separate the rules into “left” rules
(implemented in prove_left) and “right” rules (implemented in prove’).
Moreover, since Prolog does backtracking search, we don’t need to use continuations.
Q3a.Write Prolog clauses that correspond to the rules And-Right and Implies-Right.
Q3b. Implement Implies-Left.
Hint: Compare our Prolog clause for ‘And-Left’ to the rule ‘And-Left’.
4 Bonus (up to 5%)
Implement the Or-Left, Or-Right-1, Or-Right-2 rules from Assignment 3.
2Q2: Implication Form
3 Q3: Tiny Theorem Prover
4Bonus (up to 5%)
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com