**Under Construction**

As previously introduced, Prolog is based on formal logic and mathematics (predicate calculus) and with this basis, the fundamental axioms of numbers and set theory assumed to be true. Theorems are additional propositions which may be inferred from initial set.

**Theorem Proving **

**2 Approaches**

**Forward Chaining – **this is bottom up resolution where the system begins with facts/rules and attempts to find a sequence of matching propositions that lead to goal. This works well when the number of possible answers is large as backward chaining introduced below would require a large number of matches to get thae answer.

**Backward Chaining – **this is top down resolution where the system begins with a goal and attempts to find set of matching propositions that lead to set of facts in database. This is Prolog’s mechanism and works well when there is reasonably small set of candidate answers.

**Propositions** are logical statements that may or may not be true and they consist of objects and relationships of objects to each other. These propositions are checked (through inference) to determine validity. Propositions may contain:

**Facts** – defined to be true

**Queries** – a query is also called a goal and its truth is to be determined through matching and inference engine. To prove goal is true the inference engine must find a chain of inference rules and facts in database to establish the validity of the goal. Note if a goal is a compound proposition, each proposition called a subgoal.

**Matching** is the process of proving goals/subgoals through proposition matching (e.g. checking facts and instantiating variables). Proving a subgoal/goal is called **satisfying **the subgoal/goal.

**Variables** assumed to be **universally quantified** (read as **‘FOR ALL’ **?) or **existentially quantified** ( read as ‘**THERE EXISTS’ **?) if the variable appears only in body. Example:

hasachild(X) :- parent(X, Y) %may be read in two ways

1. For all X and Y, If X is a parent of Y then X has a child (you may think of this as beginning with the body/antecedent)

2. For all X, X has a child if there exists a Y such that (st.) X is a parent of Y (you may think of this as beginning with the goal/consequent)

**Closed World Assumption**

Prolog is based on a closed world assumption where Prolog only reports truths which may be proved using its database. In other words, Prolog has no knowledge beyond what is contained in its database and this may be misleading. As an example, if there is insufficient information Prolog will report “False”.

**Recursion **

Recursive programming is fundamental to Prolog programming and is required to solve complex tasks.

**HIERARCHICAL CLASSIFICATION of DATA OBJECTS**

data objects

/ \

simple objects structures

/ \

constants variables

/ \

atoms numbers

PROCEDURE – set of clauses about logically related relations

Question/Query to prolog – sequence of 1 for more goals

Prolog tries to satisfy all goals (e.g. demonstrate the goal is true)

Goal is true (satisfiable) if it logically follows from facts and rules of program

If question contains variables prolog finds instantiations of particular objects to achieve goals

If conclusion proved, instantiated variables are shown

If conclusion can not be proved, prolog returns no

FORMAL DESCRIPTION

Prolog accepts facts and rules as set of **axioms and tautologies**

User’s questions are **conjectured theorem**

Prolog attempts to logically derive theorem from given axioms

Sequence of steps called **proof sequence**

Prolog finds proof sequence in inverse order

Starts with goals and using rules substitutes current goals with new goals

Until new goals happen to be simple facts

1. predecessor(X, Z) :- parent(X, Z).

goal is predecessor(tom, pat)

variables in rule instantiated as follows, X = tom, Z = pat

original goal predecessor(tom, pat) replaced by parent(tom, pat)

there is no clause in program whose head matches goal parent(tom, pat)

therefore goal fails

Prolog back tracks to original goal to try another alternative

Prolog attempts second clause

predecessor(X, Z) :-

parent(X, Y),

predecessor(Y, Z).

variables X and Z become instantiated as X = tom, Z = pat

Y is not instantiated yet

Top goal predecessor(tom, pat) replaced by two goals:

Parent(tom, Y),

Predecessor(Y, pat)

Prolog tries to satisfy them in order they are written

First one easy => matches one of facts and program

Matching forces Y to become instantiated to bob

Thus first goal satisfied remaining goal becomes

Predecessor(bob, pat)

Prolog tries to satisfy this goal using first rule

Notes this application of rule independent of previous application

Uses new set of variables

Predecessor(X’, Z’) :- parent(X’, Z’)

Head must match current goal predecessor(bob, pat)

X’ = bob, Z’ = pat

Current goal replaced by parent(bob,pat)

goal immediately satisfied => appears as fact in program

** note ** proof sequence looks like a tree

?- trace. % invokes trace mechanism and shows instantiations

DECLARATIVE and PROCEDURAL MEANING

DECLARATIVE

Concerned only with relations defined by program

Declarative meaning determines what will be output of program

PROCEDURAL

Determines how output is obtained

How are relations actually evaluated by PROLOG system

PROLOG ADVANTAGES

Prolog’s ability to work out its own procedural details considered an important advantage

Encourages programmers to consider declarative meaning of programs

independently of procedural meaning

Results of program are in principal determined by declarative meaning

Programmer concentrates on declarative meaning e.g. not distracted by execution of details

OTHER AIDS

CTRL-C aborts execution

In conjunction with a on debug line

**Prolog Logic Theory**** `**

PROPOSITIONS

Proposition is logical statement that may or may not be true

Consists of objects and relationships of objects to each other

Formal logic developed to provide method describing propositions

Formally stated propositions then checked for validity

2 modes

FACT proposition stated and defined to be true

QUERY proposition stated and truth is to be determined

OBJECTS

Objects in propositions represented by single terms

2 types

constants

variables

CONSTANT is symbol that represents an object

VARIABLE is symbol that may represent different objects at different times

Much closer to variable in mathematical formalism

than imperative programming language

Not associated with memory cell

ATOMIC PROPOSITION

Simplest proposition consisting of compound terms

COMPOUND TERM

One element of mathematical relation

Written in form that has appearance of mathematical function notation

Mathematical function is mapping

Represented as either

an expression

a table

a list of tuples

Composed of two parts

FUNCTOR function symbol that names the relation

ordered list of parameters

referred to as tuples

COMPOUND PPROPOSITION

2 or more atomic propositions

Connected by logical connectors for operators

(Same manner as constructing logic expressions in imperative languages)

LOGICAL CONNECTORS LISTED IN ORDER OF PRECEDENCE

Quantifiers ?,?

Negation ¬

Conjunction ?

Disjunction ?

Equivalence ?

Implication ?

Variables appear in propositions only when introduced by quantifiers

2 quantifiers exist in predicate calculus

Scope extends to all attached propositions and may be extended with parentheses

UNIVERSAL (?X.P) meaning for all X, P is true

EXISTENTIAL (?X.P) meaning there exists a value for X to make P true

A period between X and P syntactically separates variable from proposition

EXAMPLES

?X.(woman(X) ? human(X))

States for any value X, if X is a woman, X is human

?X.(mother(mary,X) ? male(X))

states there exists a value X such that Mary is mother of X

and X is male

CLAUSAL FORM

There are many different ways of stating propositions that have same meaning

This could possibly lead to redundancy

Not a problem for logicians but it is a problem for automated/computerized system

Proposition in clausal form as following general syntax

B1 ? B2 ? …. ? Bn ? A1 ? A2 ? …? An

A’s and B’s are terms

If all A’s are true then at least 1 B is true

Note the similarity to prolog semantics

SEMANTICS

Existential quantifiers are not required

Universal quantifiers are implicit in variables in atomic propositions

No operators other than conjunction/disjunction required

(they also need not appear in order above)

all predicate calculus propositions may be algorithmically converted to clausal form

ANTECEDENT

Right hand side of clausal form proposition

CONSEQUENT

Left-hand side of clausal form

Consequence of antecedent

THEOREM PROVING

RESOLUTION

Inference rule that allows deferred propositions to be computed from given propositions

Provides method for automatic theorem proving

Devised/developed to be applied to propositions in clausal form

Allows discovery of new theorems inferred from known axioms and theorems

EXAMPLE and EXPLANATION

P1 ? P2

Q1 ? Q2

States P2 implies P1 and Q2 implies Q1

Suppose Q1 is equivalent to P2

If Q2 is true then Q1 and P2 are true and truth of P1 may be inferred

(now we know basis of axiomatic semantics)

SEMANTICS/MECHANICS

Terms of left sides of two propositions ANDed together to make left side of new proposition

Same thing is done to get right side of new proposition

Terms that appear on both sides of new proposition removed from both sides

UNIFICATION

Process of determining useful values for variables

INSTANTIATION

Temporary assigning of values to variables to allow unification

Often variables instantiated with value that fails

(Fails to complete subsequent required matching)

This requires the variable to be unbound and the procedural mechanism to BACKTRACK

PROLOG AND LOGIC PROGRAMMING

PROLOG is declarative language (logic programming is declarative)

Program consists of declarations

Declarations are statements or propositions in symbolic logic

Adheres to strict Mathematical formalism

Given proposition may be concisely determined from statement itself

Logic programming has no side effects

Prolog is not procedural => describe form of result

**imperative semantics requires **

**examination of local declarations **

**knowledge of scoping/referencing environment**

**execution trace to determine values of variables**

PROLOG INFERENCING

BACKWARD CHAINING

Begins with goal and attempts to prove sub goals

Sub goal becomes new goal which in turn may be comprised of sub goals

Prolog uses left to right, depth first order of the evaluation to prove sub goals

One must be careful not to cause infinite loop

Programmer must be aware inferencing process

DEPTH-FIRST

Searches complete sequence of propositions

Completes first subgoal before working on others

note this is a recursive definition/description

prolog designers chose depth first because requires fewer computer resources

**Prolog fails as a pure logical programming paradigm**

**Depth first search requires proper ordering of clauses**

*Definition:* *BREADTH-FIRST*

Works on all sub goals in parallel

*Requires substantial memory and computer resources*

BACKTRACKING

When system fails to show truth of subgoal

System abandons subgoal it could not prove

Unbinds instantiated variables and backtracks to reconsider previous proven sub goals

Creates new instantiations and new traversal of tree

Time consuming process

PROOF by CONTRADICTION

Theorem ? propositions

negate theorem -> GOAL

prove theorem by finding inconsistency in propositions -> HYPOTHESES

May not be efficient

Resolution is finite process if set of propositions is finite

Time required to find inconsistency in large database may be huge (large # of propositions)

Simplify resolution process using HORN CLAUSES

HORN CLAUSES

Special kind of propositions

2 forms

single atomic proposition on left side

rules

empty left side

facts

left side of clausal form called the **head**

right side of clausal form called the **body**

**Under Construction**

*No files found.*