The Course Logic Programming ID2213 Thomas Sjöland sjoland@kth.se
SCS, Software and Computer Systems
ICT - School of Information and Communication Technology
KTH, The Royal Institute of Technology
The Course Logic Programming ID2213 Thomas Sjöland sjoland@kth.se
SCS, Software and Computer Systems
ICT - School of Information and Communication Technology
KTH, The Royal Institute of Technology
These lecture notes are meant as a complement to the textbook and to the programming manual. We give here the structure of the course as it has been redesigned in 2001. It now contains five two hour lectures and four two hour tutorials where the course material is presented.
Outline of lectures W35:
F1: Theory, Elementary Programs, unification
Theory, Model Theory of LP, proof trees and search trees
W36:
F2: Programming Style, recursion, equality primitives, representation
Advanced Recursive Techniques, accumulators, diff-structures, ADT
W37:
F3: Search Based Programming, cut and negation
Concurrency, Search Based Programming, state space, puzzles, games
W38:
F4: Logic programming and Grammars, parsing with DCG
W39:
F5: Program Transformation. Higher-order programming.
Metaprogramming, Expert Systems
W40:
F6: Case study: A compiler for a simple stack machine
W41:
F7: Case study: Support for reasoning about electronic circuits
Red1: Project presentation 4 hours
W42: Written Examination
F1: Theory and simple programs Sterling and Shapiro ch. 1,2,4,5,6
Nilsson and Maluszynski ch.1,2,3,6
Theory for Logic Programming
Outline Informal introduction to logic programming theory
Data in logic programs: Individual constants, term constructors, logical variables, compound terms, trees and lists
Equality theory, Unification
Logic Programs: Definite (Horn) Clauses
Model theory (least Herbrand model, term interpretation)
Proof theory and operational semantics of Prolog
(SLD-resolution, proof trees)
Simple databases
Recursive rules
Logic Programming Using proofs to compute
To each proof you can order a computation
To each computation you can order a proof
Representation of
knowledge and computations
- algorithms
- functions
- relations
Data in Logic Programs Programs express facts about a world of objects
Constants
Functors
Numbers
Compounded structures (normally finite)
Lists
Trees
Objects in Logic Programs Individual constants
a b foo 4711 -37 34.5
Functors
structure names of trees and graphs
same syntax as non-numerical constants
Arity (number of arguments):
term/4, a/0
Syntax example:
term(a,b,-4711,other(b,a))
Logical Variables - Syntax Syntax: begin with a capital letter (or '_')
X Y Z Foo _Bar _
Variables can occur wherever constants or structures occur
Range over logical objects
_ is "anonymous" or "void"
Programs are Theories sets of relations (predicates) over objects
The classical form of a definition is as a clausal form where a positive literal P has exactly one occurrence:
P or not Q1 or ... or not Qn
This can be written as P if Q1 & ... & ... Qn.
If all goals Qi are true the clause becomes P.
Program = Definitions + Query The general form of a relation definition is
P if (Q11 & ... & Q1n)
or ...or
(Qm1 & ... & Qmn).
1..m and 1..n are index sets large enough to cover all goal atoms, Qij
Program = Definitions + Query Elementary literals (atoms)
true, false, X=Y
cannot be redefined
(only used in queries and definition bodies)
Defined literals (p above)
Definite Clauses: Facts Facts: statements of form P :- true.
Also written simply as P.
Example:
brother(nils,karl).
Means that the binary relation brother holds between individual constants nils and karl.
Definite Clauses: Rules Rules:
conditional formulae of the form
P :- Q1,....,Qn.
P is called the head and Q1,...,Qn the body of the clause and P, Q1,...,Qn are atomic formulas (relation symbols). Some of the Qi may be predefined relation symbols (=, <)
":-" is read as "if", "," is read as "and"
Definite Clauses: Rules, example Example of a rule:
grandfather(X,Y) :- father(X,Z), father(Z,Y).
The binary relation grandfather holds between two individuals represented by variables X and Y if the relation father holds between X and some Z and between that Z and Y.
Clause Syntax Example :
p(17).
p(X) :- X<8, q(X).
p(X) :- q(X), X=s(Y), p(Y).
In english the above example could be stated as follows:
- The property p holds for the constant 17.
- The property p holds for a term denoted by the variable X if X<8 and q holds for X.
- The property p holds for X if q holds for X, X equals a term s(Y) and p holds for Y.
Programs are Theories Definitions are collections of facts and rules
- sets of relations (predicates) over the objects
e.g. (for predicate p/2 using q/2 and r/2)
p(foo,bar).
p(Foo,Bar) :- q(Foo,Baz), r(Baz,Bar).
Functions are special cases of relations (deterministic)
Query, Goal formula to be verified (or falsified)
Questions posed to the system are of the form
?- Q1,...,Qn.
for example
?- q(Foo,Baz), r(Baz,Bar).
If the system succeeds to prove the formula, the values of the variables (the bindings) that are the result are shown, otherwise the proof attempt has failed or possibly loops.
Note that more than one solution is possible.
How Prolog works A user query ?- p(Args).
is proven using resolution
- look for all definition clauses of p
- pick one, save others as alternatives
- match the arguments in Args with the terms in the head of the clause, create necessary variable bindings
- if the matching unification fails, try next alternative
- else prove the goal clauses of the body from left to right
- if all proofs are done, the bindings are presented
Database for family relationships parent(Parent, Child), male(Person) and female(Person)
parent(erik, jonas). male(erik). parent(erik, eva). male(jonas). parent(lena, jonas). female(lena).
?- parent(lena, jonas).
Yes
?-parent(X,Y). X=erik, Y=jonas; X=erik, Y=eva; X= lena, Y= jonas
?- parent(X, jonas). X=erik; X=lena
Comments