In this exercise, you will write a Prolog program to determine the validity of inferences in the Aristotelian syllogistic. Of course, one could simply apply depth-first or breadth-first search on a complete system of proof rules for this language as explained in the lectures. However, by analysing the logic, we can write a much more efficient program.
Recall that, in the syllogistic, we suppose an indefinitely large set of atoms p, q, p1, . . . . A literal is either an atom p or an expression p ̄ (read: “not-p”), where p is an atom. A formula in the syllogistic is an expression of either of the types ∀(p, l) and ∃(p, l), where p is an atom, and l a literal.
The semantics of these formulas was explained in the lectures. As usual we say that a set of premises Θ entails a conclusion θ just in case all interpretations making all the formulas in Θ true also make θ true. We write this condition in symbols as Θ |= θ. If there is no interpretation making all the formulas in Θ true, we say that Θ is unsatisfiable. Our task is the following: given a set of premises Θ and a conclusion θ, determine whether Θ entails θ.
We need the following preliminaries. If l is a literal, we denote its opposite by ̄
̄
l; note that p ̄ = p. We call ∀(p, l) a universal formula, and ∃(p, l) an existential
formula. Suppose Φ is a set of universal formulas, and l, m are literals. We say that there is a Barbara-step in Φ from l to m if either of the following
̄
conditions hold: (i) l = p and ∀(p,m) ∈ Φ; (ii) m = p ̄ and ∀(p,l) ∈ Φ. Say
that a Barbara-path in Φ from l to m is a sequence of literals l0,…,lk (k ≥ 0)
suchthatl0 =l,lk =mandthereisaBarbarastepfromli toli+1 foralli
(0 ≤ i < k). It should be obvious that, if there is a Barbara-path in Φ from p
to l, then Φ |= ∀(p, l); likewise, if there is a Barbara-path in Φ from l to p ̄, then ̄
Φ |= ∀(p, l).
We are now in a position to describe our algorithm for deciding whether
Θ |= θ. The first step is to split the premises Θ into a set of universal formulas Φ,
and a set of existential formulas Ψ. Let θ be any formula and suppose Φ∪Ψ |= θ.
It can be shown that (i) if θ is universal and Φ ∪ Ψ is satisfiable, then Φ |= θ;
(ii) if θ is existential, then there exists ψ ∈ Ψ such that Φ ∪ {ψ} |= θ; and ̄
(iii) If Φ ∪ Ψ is unsatisfiable, then there exists ∃(p, l) ∈ Ψ such that Φ |= ∀(p, l). Thus, to test whether an argument is valid, we can just consider these conditions separately. In fact, it can be shown that, for a set Φ of universal formulas: (i) Φ |= ∀(p, l) holds if and only if there is a Barbara-path in Φ from p to l; and (ii)
2
Φ ∪ {∃(p, l)} |= ∃(q, m) if and only if there is a Barbara-path in Φ from either p or l to q, and also a Barbara-path in Φ from either p or l to m.
This gives us all we need to test validity in the syllogistic. Your task is now to implement this procedure in Prolog. Of course, we must encode the four syllogistic formulas as Prolog terms. Do this as follows:
∀(p, q) ∀(p, q ̄) ∃(p, q) ∃(p, q ̄)
all(+p,+q) all(+p,-q) some(+p,+q) some(+p,q).
1. Write a predicate which returns the opposite of a literal.
?- opposite(+a,L).
L = -a.
?- opposite(-a,L).
L = +a.
2. Write a predicate separate/3, which takes a list of formulas in the syl- logistic, and separates it into two lists: one containing the existential formulas, and the other containing the universal formulas. E.g.
?- separate([some(+a,+b),all(+d,-d),all(+a,+b),all(+b,+c),
some(+e,+b)],Ex,Univ).
Ex = [some(+a, +b), some(+e, +b)],
Univ = [all(+d, -d), all(+a, +b), all(+b, +c)].
(4 marks)
3. Write a predicate bPath(L,M,UFlas) to determine whether there is a Barbara-path in the set of universal formulas UFlas from literal L to literal M, thus:
?- bPath(+a,-c,[all(+a,+b),all(+b,-c)]).
true .
?- bPath(+c,-a,[all(+a,+b),all(+b,-c)]).
true .
?- bPath(+a,-c,[all(+a,+b),all(-a,+c)]).
false.
Don’t get stuck in an infinite loop!
(2 marks)
(6 marks)
3 4. Usingthealgorithmoutlinedabove,writeapredicateinfCheck(Flas,Fla)
to determine whether a set of premises Flas entails a conclusion Fla.
?- infCheck([all(+a,+b),all(+b,+c),some(+d,-c)],some(+d,-a)).
true .
?- infCheck([all(+a,+b),all(+b,+c),some(+d,-c)],some(+a,-d)).
false.
Watch the corner cases!
(8 marks)