CSE 360: Lecture 7

Natural Deduction for Propositional Logic

kind bool           type.
type p, q, r, s     bool.
type and, or, imp   bool -> bool -> bool.
type pv             bool -> o.

pv B :- pv A, pv (imp A B).
pv (imp A B) :- pv A => pv B.
pv A :- pv (and A B).
pv B :- pv (and A B).
pv (and A B) :- pv A, pv B.
pv C :- pv (or A B), (pv A => pv C),
                     (pv B => pv C).
pv (or A B) :- pv A.
pv (or A B) :- pv B.

Two notions of negations

Intuitionistic and classical logic have the ex nihilo quod principle: from a contradiction (inconsistency) you can prove anything.

This principle seems too ``global'' often. For example, if a database of student enrollment becomes inconsistent, it doesn't seem sensible for facts like 

(append nil (2::nil) nil)
to be provable. It seems that inconsistences should sometimes be more ``local''. Minimal logic is a weakened form of intuitionistic logic in which ex nihilo quod has been removed.

We can view minimal logic as having no special symbol for negation; that is, lambda Prolog does not have any special symbol for false, so it implements minimal logic. Notice that fail is different from false.

Consider the following queries: 

(p => q) => ((q => incon) => (p => incon))
p => ((p => incon) => incon)
p; (p => incon)
((p; (p => incon)) => incon) => incon.

Modules and Program Equivalence

Let mod1 and mod2 denote the conjunction of the program clauses in two modules. Also assume that these modules do not contain any occurrences of existential quantifiers or disjunctions. Thus, this code can be both a program and a query.

Assume that mod1 |- mod2 (that is, the first module logically implies the second module). Also assume that mod2 |- G . We therefore know that mod1 |- G .

Thus, if mod1 and mod2 are logically equivalent, then they are observationally equivalent; that is, they prove all the same goal formulas. In such a situation, one module can be replaced with another module and from a declarative point-of-view, there will not be any difference. From an operational point-of-view, there can be a difference.

Other notions of equivalence are also possible and natural.

Notions of Program Equivalence

Are the following two modules equivalent? 
module mod1.
type p, q   int -> o.

p 1.
p 2.
q X :- p X.

module mod2.
type p, q   int -> o.

p 1.
p 2.
q 1.
q 2.
yes: In the sense that they prove the same atomic facts.

no: In the sense that there are hypothetical goals that the first proves and the second does not prove.

p 3 => q 3.
pi y\(p y => q y).
Notice that the code in module mod1 implies the code in mod2.

Programs involving locally defined predicates

Consider the following module in for determining evenness of integers. 
module even1.

kind nat     type.
type z       nat.
type s       nat -> nat.
type even    nat -> o.

even z.
even (s (s N)) :- even N.
The following module computes the same predicate but with an auxiliary predicate that is declared locally. 
module even2.

kind nat     type.
type z       nat.
type s       nat -> nat.
type even    nat -> o.
local odd    nat -> o.

even z.
even (s N) :- odd N.
odd  (s z).
odd  (s N) :- even N.
It is possible to prove that these two modules are logically equivalent. In proving that even2 follows from even1, substitute for the predicate odd the predicate n\(even (s n)).
Lecture Directory / Module Directory / CSE360 Syllabus