Tuesday, 14 February 2023

4 - Proving New Facts By Deduction



The power of prolog is not in finding simple matches to facts in a database. Prolog's power lies in its rather persistent search that can combine together several facts to, in effect, prove a new fact.

Let's explore at a minimal example of this power.


% Example 04 - Deduction

% facts
mammal(dog). 
mammal(cat).

% relation
animal(X) :- mammal(X). 

The first two lines of code establish simple facts, that a thing called dog has a property mammal, and that a thing called cat has a property mammal too. That is, a cat and a dog are mammals.


Relation Between Properties

The last line of code takes a form that is new to us, so let's break it down. It says that a thing X has a property animal if that same thing X has a property mammal

The symbol :- is equivalent to logical implication ← from right to left. Here mammal(X) being true implies animal(X) being true, but not the other way around. That is, animal(X) does not imply mammal(X)

In plain English, this says that if a thing is a mammal, then it is also an animal. It does not say that if a thing is an animal, then it is also a mammal, which makes sense. A fish is an animal, but is not a mammal.

What this line of code establishes is a relation between two properties. These are also called rules, with a head to the left of the :- symbol, and a body to the right.


Deduction

A relationship between properties allows us to say something about one of the properties (the head) if we know something about the other (the body).

Let's try it.


?- animal(cat).

true

We're asking if a cat is an animal. The database has a fact that explicitly states a cat is a mammal, but none that says a cat is an animal.

Prolog has used the relationship between mammal and animal to deduce that a cat is also an animal.

Let's walk through how Prolog finds this answer. The query is animal(cat), and although there is no fact in the database that directly matches this query, Prolog does find it matches the head of the rule animal(X):-mammal(X) with X=cat. Prolog's task is then to see if can satisfy the body of this rule, mammal(cat). This is easily done because the database does contain mammal(cat). Therefore animal(cat) is provable.

We mighty ask why prolog's task was to satisfy the body of the rule animal(X):-mammal(X) once the head had matched the query animal(cat). The reason is because the body of a rule implies the head. To prove the head, all prolog needs to do is prove the body. So proving the body becomes its temporary goal.

If prolog wants to match with the head of a rule, where does this leave matching simple facts like mammal(dog) or tasty(apple)? The simple facts we first met are in fact rules with a head but an empty body. That is, the head is always true because the condition, the body, for the head to be true is empty.

Although this is example is small, what we've seen is pretty amazing. Prolog is not just searching for facts that match a query directly, but is using a relation between properties to deduce the truth of a new fact - a fact that was not explicitly stated in the database.

The following diagram visualises how prolog solves this query using deduction. We can see how combining the initial query goal with a rule leads to a new query goal.

 


Key Points

  • In addition to simple facts, we can define relations between properties. These are called rules.
  • Rules have the form head(X):-body(X). The symbol :- is equivalent to the logical implication ← from right to left. 
  • animal(X):-mammal(X) says the property animal holds if property mammal holds for a thing X. It does not mean the property mammal holds if property animal holds for a thing X. 
  • Prolog makes use of rules by matching a query to the head of a rule, then trying to satisfy the body. Satisfying the body of a rule is enough to prove the head.
  • Simple facts are rules with a head but an empty body. The head is always true because the condition is empty.
  • Prolog can use relations between properties to prove a statement that is not explicitly in its database by deduction