Slide 1: Logic Programming
Automated Reasoning in practice
Slide 2: Motivation: monotonicity
First order logic is monotone:
T’ T |= F1 G
F2 F3
But: people seldom reason monotonically !
Birds fly
+ +
Fred is a bird
Fred flies
Fred is a penguin
2
Slide 3: Default reasoning:
Is a form of reasoning that we’d like to use permanently
otherwise the rules are far too complex!
Is usually supported by hierarchy, inheritance and exceptions in OOP
also an early AI-formalism
CANNOT be expressed in FOL
independent on the knowledge representation !!
CAN be expressed in some FOL extensions
non-monotone logics the simplest one of those is … …
3
Slide 4: Logic Programming
Resolution-based automated reasoning:
restricted to Horn clauses restricted to backwards linear resolution
BUT: with 3 important new extensions:
return Answer Substitutions Least-model semantics instead of standard FOL model semantics Extending Horn clause logic with Negation as Finite Failure
4
Slide 5: Answer substitutions
The link to programming
Slide 6: Answer substitutions
anc(x,y) parent(x,y) anc(x,y) parent(x,z) anc(z,y) parent(A,B) (3) parent(B,C) false anc(u,v) false anc(u,v) Answer: Yes, u v anc(u,v) (1) (2) (4)
(2) {u/x1,v/y1}
false parent(x1,z1) anc(z1,y1) (3) {x1/A,z1/B} false anc(B,y1) (1) {x2/B, y2/y1} That is: u = A and v = C false parent(B,y1) (4) {y1/C} (composition of all mgu’s applied to the goal variables) false
6
Slide 7: And computes ALL answers
anc(x,y) parent(x,y) anc(x,y) parent(x,z) anc(z,y) parent(A,B) (3) parent(B,C) false anc(u,v) (1) {u/x1,v/y1} false parent(x1,y1) false (3) {x1/A,y1/B} (4) {x1/B,y1/C} false Another answer: u = A and v = B The third answer: u = B and v = C
7
(1) (2) (4)
false anc(u,v)
Slide 8: Logic PROGRAMMING
By computing answer substitutions Logic Programming serves as a de basis for a number of “general purpose” programming languages.
Prolog, Mercury, XSB, …
with an efficiency comparable with C !
and even faster for some programs.
8
Slide 9: Example arithmetic:
Practical programming?
Yes: z=7 Yes
double_plus_1(x,y) y is 2*x + 1 false double_plus_1(3,z) false double_plus_1(2,5) Example lists: append([], list, list) append([x|list1], list2, [x|list3]) append(list1, list2, list3) false append([1,2], [3,4,5], z) false append([1,2], y, [1,2,3]) false append(x, y, [1,2]) Yes: z= [1,2,3,4,5] Yes: y= [3] Yes: x = [], y = [1,2] x = [1], y = [2] 9 …
Slide 10: Least model semantics
Specify in a more compact way
Slide 11: Least model semantics
Example: a database:
celebrity(Crabé) celebrity(Jambers) celebrity(Peeters) celebrity(Lisa) celebrity(Tieleman) celebrity(Samson)
Is DeSchreye a celebrity ??
false celebrity(DeSchreye)
We get no proof of inconsistency !
FOL semantics says: celebrity(DeSchreye) is not logically entailed, thus: we do not know if it is true or not! Least model semantics says: ~ celebrity(DeSchreye)
11
Slide 12: Formally: the idea
What are the atomic consequences of theory T? T
p q ~r ~s ~q s model 1 model 3 model 2
In FOL: Consequences are in the intersection: p en ~r. We do not know anything about the truth of q and s. In LP: Consequences are in the intersection: p en ~r. Other predicates are NOT true: ~q and ~s.
12
Slide 13: Relation with FOL
The logic program:
celebrity(Crabé) celebrity(Jambers) celebrity(Peeters) celebrity(Crabé) celebrity(Jambers) celebrity(Peeters) ~celebrity(DeSchreye) ~celebrity(Janssens) … celebrity(Lisa) celebrity(Tieleman) celebrity(Samson) celebrity(Lisa) celebrity(Tieleman) celebrity(Samson) ~celebrity(Cobain) ~celebrity(Dali) …
is equivalent to the infinite FOL theory:
or also to:
∀x celebrity(x) ↔ (x = Crabé) ∨ (x = Jambers) ∨ (x = Peeters) ∨ (x = Lisa) ∨ ( x = Tieleman) ∨ (x = Samson)
13
Slide 14: The “closed” assumption
Logic programming provides a compact way to express ‘complete knowledge’ on some subject. If you do not say that something is true, than it is false.
The Closed World Assumption ! (= everything not entailed by the theory is false)
In other words: Logic Programming supports formulating definitions of the concepts.
Not just state what is true about these concepts (=FOL) !
14
Slide 15: How relevant is the change of semantics?
In FOL: In LP:
{smart(Kelly)} implies neither strong(Kelly) nor ~strong(Kelly)
{smart(Kelly)} implies ~strong(Kelly) In {smart(Kelly), strong(Kelly)} , ~strong(Kelly) is no longer entailed.
In particular: LP is a non-monotone logic !!
Knowledge is differently represented in these 2 formalisms. Also: some concepts can be completely axiomatized in LP but not in FOL.
Ex.: the natural numbers !
15
Slide 16: Negation as finite failure
Slide 17: Negation as finite failure
The basic idea:
extending the representation power of Logic Programming beyond the Horn Clauses logic
How?
equivalent: allow disjunctions in the heads allow negation before the body atoms
– both give complete predicate logic ! – (but: with the least model semantics we will get something different from FOL!)
Here: Introduce negations in bodies !
17
Slide 18: Meaning of negation as finite failure
Not the meaning of standard negation not(B) means: If all attempts to prove B using linear LP-resolution, fail in a finite time, conclude than not(B)
This is meaningful only with the least model semantics (where everything that is not proven to be ‘true’, is considered to be ‘false’)
18
Slide 19: The ancestor example
anc(x,y) parent(x,y) anc(x,y) parent(x,z) anc(z,y) parent(A,B) (3) parent(B,C) false anc(u,v) (1) (2) (4)
Try to prove that “anc(John,B)” holds!
false anc(John,B) (2) {x/John,y/B} (1) {x/John,y/B} false parent(John,B) false parent(John,z) anc(z,B) fails fails
Conclusion: not anc(John,B)
19
Slide 20: Another example
even(0) even(s(s(x))) even(x) odd(y) not even(y) false odd(s(s(s(0)))) false odd(s(s(s(0)))) false not even(s(s(s(0)))) Proof for even(s(s(s(0)))) fails: conclusion not even(s(s(s(0)))) false
20
false even(s(s(s(0)))) {x/s(0)} false even(s(0)) fails
Slide 21: And another example
qq p not q false p false p false not q Proof for q goes into infinite derivation: no conclusion for q no answer false q false q
…
But ~q is true according to the least model semantics!
21
Slide 22: Default reasoning in LP (1):
locomotion(x,Fly) ← isa(x,Bird), not abnormal1(x) locomotion(x,Walk) ← isa(x,Ostrich), not abnormal2(x) isa(x,Bird) ← isa(x,Ostrich) abnormal1(x) ← isa(x,Ostrich) Also known: isa(Fred,Bird), Prove that: ∃x locomotion(Fred,x)
false <- locomotion(Fred,x) {x/Fly} false <- isa(Fred,Bird), not abnormal1(Fred) false <- not abnormal1(Fred) false <- abnormal1(Fred) false <- isa(Fred,Ostrich) false <fails
22
Slide 23: Default reasoning in LP (2):
locomotion(x,Fly) ← isa(x,Bird), not abnormal1(x) locomotion(x,Walk) ← isa(x,Ostrich), not abnormal2(x) isa(x,Bird) ← isa(x,Ostrich) abnormal1(x) ← isa(x,Ostrich) isa(Fred,Bird) Also known: isa(Fred,Ostrich), Prove that: ∃x locomotion(Fred,x) false <- locomotion(Fred,x) {x/Fly} false <- isa(Fred,Bird), not abnormal1(Fred) false <- not abnormal1(Fred) false <- abnormal1(Fred) false <- isa(Fred,Ostrich) false <-
fails (for this branch) backtracking: the 2nd branch
23
Slide 24: Default reasoning (3):
locomotion(x,Fly) ← isa(x,Bird), not abnormal1(x) locomotion(x,Walk) ← isa(x,Ostrich), not abnormal2(x) isa(x,Bird) ← isa(x,Ostrich) abnormal1(x) ← isa(x,Ostrich) isa(Fred,Bird) Also known: isa(Fred,Ostrich), Prove that: ∃x locomotion(Fred,x) false <- locomotion(Fred,x) {x/Walk} false <- isa(Fred,Ostrich), not abnormal2(Fred) false <- not abnormal2(Fred) false <- abnormal2(Fred) false <fails
24
Slide 25: Prolog
A specific programming language based on LP. Uses a depth-first strategy to search linear resolution proofs. incomplete can get stuck in infinite branches Has a bunch of built-in predicates (sometimes without logical meaning) for: Numerical computations, input-output, changing the search strategy, meta-programming, etc. More recent LP languages: Goedel, Mercury, Hal, ..
25
Slide 26: Beyond FOL and Logic Programming
Logic Programming is very useful if you have a COMPLETE knowledge over your predicates FOL is very useful if your knowledge is INCOMPLETE Combine !
Open Logic Programming LP-definitions for the part for which you have a complete knowledge, FOL formulae for the rest.
26
Slide 27: Constraint Logic Programming
Integrate constraint processing techniques (consistency, forward checking, looking ahead, …) with Logic Programming. Advantages of Logic for knowledge representation Advantages of Constraint solving for efficient problem solving A number of languages: CHIP, Eclipse, Sicsus, etc.
27
