- Natural Deduction for Propositional Logic
- Two notions of negation
- Modules and Program Equivalence
- Notions of Program Equivalence
- Programs involving locally defined predicates

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.

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

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.

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.

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.

**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

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

Lecture Directory / Module Directory / CSE360 Syllabus