Why do these things? Developing a correct program can conceptually be
done in two stages:
Specification. The problem to be solved with the program is specified, along with what information is needed to achieve this solution;So, in some ways, a specification is easier to formulate: it only needs to be correct. A program on the other hand, has to be both correct and efficient. Suppose now that specification language is something that is machine-understandable: like symbolic logic. This makes it possible to test the specification on a computer for simple problems. If the specification language can also be a programming language, then we can go one step further and get (reasonably) efficient programs directly. Consider for example the following specifications concerning an ordered sequence of length n: x = (x1 x2 ... xn):
Efficiency. The problem specification is bound to show up inefficiencies. These are then removed in stages to result in an effective "program".
S1: x is ordered if for 1 <= i,j <= n, if i < j$ then xi < xjBoth are correct, and at the same time both can be thought of as programs. Of course, one of them runs in time proportional to n2, and the other in time proportional to n. Symbolic statements that can act both as specifications and as efficient programs was one of the motivating goals of the field of Logic Programming. The extent to which it has been attained, or indeed is attainable is debatable. But, the goal remains a noble one.
S2: x is ordered if for 1 <= i <= n, xi < xi+1
The first part of the course will be concerned with writing specifications in symbolic logic, and executing them directly as programs. Hence the term "logic programming''. Having learnt how to write logic programs, the second part of the course will look at how a machine could automatically construct them for you. The idea is as follows. You provide partial specifications to the computer as statements in symbolic logic. For example, these might sets of sequences known to be ordered or otherwise:
Provided with this information, and some knowledge of comparing
numbers, can a computer automatically construct one of the specifications
given earlier? How this can be done is called is an area of logic-based
machine learning called "inductive'' logic programming. This
will take up the second part of the course.
Lecture | Contents |
1 (pdf) | Propositional Logic Programming |
|
First-order Logic Programming |
3 (pdf) | Computations and Answers |
4 (pdf) | Introduction to Model Theory |
5 (pdf) | Introduction to Proof Theory |
6 (pdf) | Proof Theory (contd.) |
7 (pdf) | Generality Orderings and Lattices |
8 (pdf) | Generality Orderings and Lattices (contd.) |
9 (pdf) | Abduction and Justification |
10 (pdf) | Hypothesis Formation |
11 (pdf) | Search and Redundancy |
12 (pdf) | Experimental Methodology |
13 (pdf) | Real-world Applications |
14 (pdf) | Revision Class (time permitting) |
|
Contents |
1 | Prolog Programming (Optional) |
|
Prolog Programming (Optional) |
|
Logic Programming without function symbols |
|
Logic Programming with function symbols |
|
Introduction to ILP |
|
Generalisation in ILP |
|
Generalisation in ILP(contd.) |