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