Prolog Interpreter

  • backward chaining: begin with the thing it is trying to prove and work backwards looking for things that would imply it, until it gets to facts. Usually can construct an AND/OR tree.

Resolution Principle

If the head of some C1 matches one of the terms in the body of C2, then we can replace the term in C2 with the body of C1. The pattern matching used to associate variables with constants is unification. Variables given values as result of unification are instantiated.

Ex.

C :- B, D
B :- E
C :- E, D

This unification is similar to Hindley-Milner type inference in ML.

For math, use the built in operator is.

Examples in S & K of programs written in Prolog.

Theoretical foundations

Does proof by contradiction.

Prolog requires a predicate to be given as a Horn clause.

G :- A, B,..., F

Horn clause. A logical formula of a particular rule-like form which gives it useful properties. Specifically, it is a clause (a disjunction of literals) with at most one positive literal. Prolog requires a predicate to be given as a Horn clause.

Resolution of two Horn clauses is a Horn clause. Convenience!

In Prolog, anything that can’t be proved via facts in the database is assumed False. Closed World Assumption. Prologic is Homoiconic - it can define itself.

The “cut operator” is used to prune a search tree when proving, limits backtracking.