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