Transcript Prolog 1 - Department of Computer Science

CS345 Fall 2012 Midterm Exam Grades
71 As, 40 Bs, 32 Cs, 24 Ds, 17 Fs
20
Number of students with this grade
18
16
14
12
10
8
6
4
2
0
30
40
50
60
70
80
90
100
110
Grade out of 100 (i.e., percentage grade)
[The number grade you got on the exam will be your percentage grade, not your grade out
of 110 points (i.e., small curve was built in).]
Dr. Philip Cannata
1
Dr. Philip Cannata
2
Programming Languages
Prolog Part 1
Dr. Philip Cannata
3
Proof by Contradiction
Database
P1
P2
It is now my intention to follow another and, as I think, a very
beautiful way of proving these same truths without the help of any
assumption. I shall proceed as follows: I shall take the
contradictory of the proposition to be proved and elicit the
required result from this by a straight-forward demonstration –
Gerolamo Sachere (1167-1733).
1). Let P = It’s raining, I’m outside (comma means “&&”)
2). P1. (P1 is True, i.e., it’s raining)
Facts
Rule
3). P2. (P2 is True, i.e., I’m outside)
4). Q :- P = I’m wet :- It’s raining, I’m outside. (if it’s raining and I’m
outside then I’m wet)
(To answer the Query “Am I wet” against the Database, assume I’m not wet)
5). –Q
6). –(It’s raining, I’m outside)
7). –I’m outside
8). Contradiction – Therefore I’m wet
( From 4 and 5 and Pattern 1 )
( From 2 and 6 and Pattern 2 )
( From 3 and 7 and Pattern 3 )
Pattern 1 (Modus
Tollens):
Q :- (P1, P2).
-Q
 -(P1, P2)
P
Pattern 2
(Affirming a
Conjunct):
R
P1.
-(P1, P2)
S
 -P2
Pattern 3:
P2.
-P2
 Contradiction
Dr. Philip Cannata
4
Running Prolog
Don’t forget the dot
Turn on trace.
To download prolog for windows go to:
http://www.gprolog.org/#download
For Linux it should be - /lusr/opt/gprolog-1.3.0/bin/gprolog
You need to set your PATH environment variable as follows:
export PATH=“/lusr/opt/gprolog-1.3.0/bin”:$PATH
Make sure you’re using the “bash” shell for this.
Dr. Philip Cannata
Turn off trace.
5
Proof by Contradiction, Unification, Resolution and Backtracking
Pattern 1 (Modus
Tollens):
Q :- (P1, P2).
-Q
 -(P1, P2)
Pattern 2 (Affirming
a Conjunct):
P1.
-(P1, P2)
 -P2
Pattern 3:
P2.
-P2
 Contradiction
Dr. Philip Cannata
1). parent(hank,ben).
2). parent(ben,carl).
3). parent(ben,sue).
4). grandparent(X,Z) :- parent(X,Y) , parent(Y,Z).
5). –grandparent(A, B)
(Unify A to X) (Unify B to Z) then Resolve 5 & 4
6). –(parent(A, Y), parent(Y, B)).
(Unify A to hank) (Unify Y to ben)
(Unify B to carl) then Resolve 6 & 1
7). –parent(ben, carl)
Contradiction  grandparent(hank, carl)
Backtrack to 6 and
(Unify B to sue) then Resolve 6 & 1
9). –parent(ben, sue)
Contradiction  grandparent(hank, sue)
6
Proof by Contradiction, Unification, Resolution and Backtracking
1). parent(hank,ben).
2). parent(ben,carl).
3). parent(ben,sue).
4). grandparent(X,Z) :- parent(X,Y) , parent(Y,Z).
5). –grandparent(A, B)
(Unify A to X) (Unify B to Z) then Resolve 5 & 4
6). –(parent(A, Y), parent(Y, B)).
(Unify A to hank) (Unify Y to ben)
(Unify B to carl) then Resolve 6 & 1
7). –parent(ben, carl)
Contradiction  grandparent(hank, carl)
Backtrack
(Unify B to sue) then Resolve 6 & 1
9. –parent(ben, sue)
Contradiction  grandparent(hank, sue)
Dr. Philip Cannata
7
Proof by Contradiction with Horn Clauses is a Complete, and Sound
Logic Systems that Finds SAT, and Valid Logic Formulas Upon
Request
parent(hank,ben).
In 1965, John Alan Robinson showed
parent(hank,denise).
that a proof by contradiction resolution
parent(irene,ben).
technique when coupled with a
parent(irene,denise).
complete search algorithm, yields a
parent(alice,carl).
sound and complete algorithm for
parent(ben,carl).
deciding the satisfiability of a
parent(denise,frank).
propositional formula, and, by
extension, the validity of a sentence
parent(denise,gary).
under a set of axioms.
parent(earl,frank).
parent(earl,gary).
grandparent(X,Z) :- parent(X,Y) , parent(Y,Z).
logEquiv2 (\ p q -> p ==> q) (\ p q -> not p || q)
not( parent(X,Y), parent(Y,Z) ) || grandparent(X,Z)
logEquiv2 (\ p q -> not (p && q)) (\ p q -> not p || not q)
not(parent(X,Y)) || not(parent(Y,Z) || grandparent(X,Z)
A Horn clause is a disjunction of Predicates in which at
most one of the Predicates is not negative
Dr. Philip Cannata
8
Horn Clause ?
reads(X) || writes(X) :- literate(X).
logEquiv2 (\ p q -> p ==> q) (\ p q -> not p || q)
not(literate(X)) || reads(X) || writes(X)
Prolog only deals with Horn Clauses
Dr. Philip Cannata
9
Prolog Example
parent(hank,ben).
parent(hank,denise).
parent(irene,ben).
parent(irene,denise).
parent(alice,carl).
parent(ben,carl).
parent(denise,frank).
parent(denise,gary).
parent(earl,frank).
parent(earl,gary).
grandparent(X,Z) :- parent(X,Y) , parent(Y,Z).
Besides being a Prolog Program this is also an example of a
Compression.
Dr. Philip Cannata
10
Composition of Relations
r
{(1,2),(2,3),(2,4),(2,5),(2,6),(6,7),(6,8)}
ComposeR r 2
{(1,3),(1,4),(1,5),(1,6),(2,7),(2,8)}
ComposeR r 3
{(1,7),(1,8)}
ComposeR r 4
{}
Dr. Philip Cannata
{(1,2),(2,3),(2,4),(2,5),(2,6),(6,7),(6,8)}
composed with
{(1,2),(2,3),(2,4),(2,5),(2,6),(6,7),(6,8)}
{(1,3),(1,4),(1,5),(1,6),(2,7),(2,8)}
composed with
{(1,2),(2,3),(2,4),(2,5),(2,6),(6,7),(6,8)}
{(1,7),(1,8)}
composed with
{(1,2),(2,3),(2,4),(2,5),(2,6),(6,7),(6,8)}
11
Composition of Relations
r
{(1,2),(2,3),(2,4),(2,5),(2,6),(6,7),(6,8)}
ComposeR r 2
{(1,3),(1,4),(1,5),(1,6),(2,7),(2,8)}
ComposeR r 3
{(1,7),(1,8)}
If 1 is rose, 2 is phil, 3 is nicolette, 4 is antoinette, 5 is jeanette,
6 is philJ, 7 is philJJ and 8 is patrick
{(rose,phil),(phil,nicolette),(phil,antoinette),(phil,jeanette),
(phil,philJ),(philJ,philJJ),(philJ,patrick)}
{(rose,nicolette),(rose,antoinette),(rose,jeanette),(rose,philJ),
(phil,philJJ),(phil,patrick)} Grandparent Relation
{(rose,philJJ),(rose,patrick)}
Great Grandparent Relation
ComposeR r 4
{}
Dr. Philip Cannata
12
Composition of Relations
This is not the last time we’ll see something similar to Composition of Relations:
parent(hank,ben).
parent(hank,denise).
parent(irene,ben).
parent(irene,denise).
parent(alice,carl).
parent(ben,carl).
parent(denise,frank).
parent(denise,gary).
parent(earl,frank).
parent(earl,gary).
grandparent(X,Z) :- parent(X,Y) , parent(Y,Z).
List Comprehension
Main> [(empno, ename, job, sal, dname) | (empno,
ename, job, _, _, sal, edeptno) <- emp, (deptno, dname,
loc) <- dept, edeptno == deptno ]
Dr. Philip Cannata
13
Proof by Contradiction, Unification, Resolution and Backtracking
Pattern 1 (Modus
Tollens):
Q :- (P1, P2).
-Q
 -(P1, P2)
Pattern 2 (Affirming
a Conjunct):
P1.
-(P1, P2)
 -P2
Pattern 3:
P2.
-P2
 Contradiction
Dr. Philip Cannata
1). factorial(0, 1).
2). factorial(N, Result) :- N > 0, M is N -1, factorial(M, S),
Result is N * S.
3). –factorial(2, X)
(Unify 2 to N) (Unify X to Result) then Resolve 3 & 2
6). –(2 > 0, M is 1, factorial(1, S), X is 2 * S.
(Unify 1 to N) (Unify S to Result) then Resolve 6 & 2
7). –(1 > 0, M is 0, factorial(0, S1), S is 1 * S1.
(Unify 0 to N) (Unify S1 to Result) then Resolve 7 & 2
9). –factorial(0, 1)
Contradiction  There is a factorial 2, now return from the
proof with the answer.
14
Hmm Runtime Stack for Factorial 3
Calling function: factorial
BasePtr = 3, printing runtime stack
null: null
n: 3
null: null
answer: null
number: 3
Calling function: factorial
BasePtr = 5, printing runtime stack
null: null
n: 2
null: null
n: 3
null: null
answer: null
number: 3
Calling function: factorial
BasePtr = 7, printing runtime stack
null: null
n: 1
null: null
n: 2
null: null
n: 3
null: null
answer: null
number: 3
Calling function: factorial
BasePtr = 9, printing runtime stack
null: null
n: 0
null: null
n: 1
null: null
n: 2
null: null
n: 3
null: null
answer: null
number: 3
Dr. Philip Cannata
int factorial(int n) {
if(n < 1) {
return 1;
}
else
{
return n * factorial(n - 1);
}
}
int main() {
int number, answer;
number = 3;
answer = factorial(number);
print(answer);
}
Exiting function: factorial
BasePtr = 9, printing runtime stack
null: null
n: 0
return#factorial: 1
n: 1
null: null
n: 2
null: null
n: 3
null: null
answer: null
number: 3
Exiting function: factorial
BasePtr = 7, printing runtime stack
return#factorial: 1
n: 1
return#factorial: 1
n: 2
null: null
n: 3
null: null
answer: null
number: 3
Exiting function: factorial
BasePtr = 5, printing runtime stack
return#factorial: 1
n: 2
return#factorial: 2
n: 3
null: null
answer: null
number: 3
Exiting function: factorial
BasePtr = 3, printing runtime stack
return#factorial: 2
n: 3
return#factorial: 6
answer: null
number: 3
15
Proof by Contradiction, Unification, Resolution and Backtracking
1). factorial(0, 1).
2). factorial(N, Result) :- N > 0, M is N -1, factorial(M, S), Result is N * S.
3). –factorial(2, _16)
(Unify 2 to N) (Unify _16 to Result) then Resolve 3 & 2
6). –(2 > 0, _113 is 1, factorial(1, _138), _16 is 2 * _138.
(Unify 1 to N) (Unify _138 to Result) then Resolve 6 & 2
7). –(1 > 0, _190 is 0, factorial(0, S_215), _138 is 1 * _215.
(Unify 0 to N) (Unify S_215 to Result) then Resolve 7 & 2
9). –factorial(0, 1)
Contradiction  There is a factorial of 2, now return from the
proof with the answer.
Note: the trace shows _243 is 1*1 but then that value gets moved
into _138
Dr. Philip Cannata
16
Some Sample Prolog Programs
factorial(0, 1).
factorial(N, A) :- N > 0, M is N - 1, factorial(M, A1), A is N * A1.
appendList([],L,L).
appendList([X|Y],L,[X|A]) :- appendList(Y,L,A).
mapsq([],[]).
mapsq([X|Y],[Z|A]) :- Z is X*X, mapsq(Y,A).
even([],[]).
even([X|Y],[X|A]) :- 0 is X mod 2, even(Y,A).
even([X|Y],A) :- 1 is X mod 2, even(Y,A).
map(FunctionName,[H|T],[NH|NT]):- Function=..[FunctionName,H,NH], call(Function), map(FunctionName,T,NT).
map(_,[],[]).
neg(A,B):-B is -A.
inc(A,B):-B is A+1.
dec(A,B):-B is A-1.
lambda(P,Body,R):Function=..[Body,P,R],
call(Function).
% Remember(let (x 5) x*2) -> (lambda x:x*2)(5)
let(V,Body,A) :- lambda(V,Body,A).
Dr. Philip Cannata
17
Haskell
Prolog
head :: [a] -> a
head (x : _ ) = x
head( [ X | _ ], X).
tail :: [a] -> [a]
tail ( _ : xs) = xs
null( [] ).
null :: [a] -> Bool
null [] = True
null ( _ : _ ) = False
tail( [ _ | Xs ], Xs).
This Prolog Code can be found
in 11Prolog Examples.p
lastelem :: [a] -> a
lastelem [x] = x
lastelem ( _ : xs) = lastelem xs
lastelem( [ X ], X).
lastelem( [ _ | Xs ], Y) :- lastelem(Xs, Y).
initelem :: [a] -> [a]
initelem [ _ ] = []
initelem (x : xs) = x : initelem xs
initelem( [ _ ], []).
initelem( [ X | Xs ], [ X | Ys ]) :- initelem(Xs, Ys).
listlength :: [a] -> Int
listlength [] = 0
listlength ( _ : l) = 1 + listlength l
listlength( [], 0).
listlength( [ _ | L ], N) :- listlength(L, N0), N is 1+N0.
sumList :: (Num a) => [a] -> a
sumList [] = 0
sumList (x : xs) = x + sumList xs
sumList( [], 0).
sumList( [ X | Xs], N):- sumList(Xs, N0), N is X+N0.
append :: [a] -> [a] -> [a]
append [] ys = ys
append (x : xs) ys = x : append xs ys
appendList( [], Ys, Ys).
appendList( [X | Xs], Ys, [X | Zs]) :- appendList(Xs, Ys, Zs).
Dr. Philip Cannata
18
Types of Reasoning
Deductive Reasoning
(Backward Chaining)
Inductive Reasoning
(Forward Chaining)
:hasSSN rdf:type owl:InverseFunctionalProperty
:John :hasSSN
123-45-6789
:Johny :hasSSN
123-45-6789
=>
:John
owl:sameAs :Johny
:Johny owl:sameAs :John
• The “fool” says in his heart “There is no God” (see Psalm 14). But is he/she talking about “that than which nothing greater can be thought”?
Because, if the “fool” can conceive of such a being, this being exists in his or her understanding, therefore . . .
• A monk named Gaunilo, complained that if Anselm’s argument proved the existence of a greatest conceivable being, it also proved the
existence of an island than which no greater island can be thought.
• Kant argued that even if Anselm’s argument works for properties, it does not work for “existence.” because existence is not a property.
• Alvin Plantinga and Kurt Gödel argued that although the argument may not work for existence, it will work for necessary existence, because
of the modality of “necessity.” Other modal logicians such as Peter Geach argued otherwise.
• Since conclusions of any valid deduction are “contained in its premises” (otherwise, it wouldn’t be valid), then every deductive argument is
“question-begging” or “circular” and produce nothing new (i.e., a priori arguments, in general, yield only analytic conclusions, not synthetic
ones, see the next page for definitions)
• Professor James H. Hall’s view in “Philosophy of Religion” at the Teaching Company is that the valid conclusion of the ontological argument
(as Anslem’s argument is sometimes called) is either “All gods exist” or “All gods necessarily exist,” not “God exists” or “God necessarily
exists”, that is the ontological argument is a valid, sound (and strong) argument against idolatry.
• My take on Anselm’s argument is a bit different than all of these but maybe that’s neither here nor there.
Dr. Philip Cannata
19
Logical Systems
Definitions:
•
“a priori knowledge” is knowledge known independently of experience (conceptual knowledge)
•
“a posteriori knowledge” is knowledge proven through experience.
•
An “analytic proposition” is one whose predicate concept is contained in its subject concept, e.g., "All bachelors are unmarried."
•
An “synthetic proposition” is one whose predicate concept is not contained in its subject concept, e.g., "All bachelors are unhappy."
Knowledge / Judgments
http://en.wikipedia.org/wiki/Logic
Analytic
Yes
No
Synthetic
?
Yes
A priori
Consistency, validity, soundness, and completeness are among
A posteriori
the important properties that logical systems can have:
Consistency, which means that no theorem of the system contradicts another.
Validity, which means that the system's rules of proof will never allow a false inference from true premises.
Completeness, of a logical system, which means that if a formula is true, it can be proven (if it is true, it is a theorem of the system).
Soundness, the term soundness has multiple separate meanings, which creates a bit of confusion throughout the literature. Most commonly,
soundness refers to logical systems, which means that if some formula can be proven in a system, then it is true in the relevant
model/structure (if A is a theorem, it is true). This is the converse of completeness. Unsoundness usually violates our innate notion of
Excluded Middle – but so do so many other important discoveries and doctrines. A distinct, peripheral use of soundness refers to
arguments, which means that the premises of a valid argument are true in the actual world.
Some logical systems do not have all four properties. As an example, Kurt Gödel's incompleteness theorems show
that sufficiently rich formal systems of arithmetic cannot be consistent and complete; however, first-order
predicate logics not extended by specific axioms to be arithmetic formal systems with equality can be complete
and consistent.
Other useful notions are that a formula (e.g., t in the Prolog example) is Satisfiable if it is possible to find an interpretation (model) that
makes the formula true, and a formula is Valid if all interpretations make the formula true (see also Haskell 2 Notes, page 6).
Recommended Reading for Anselm’s Argument:
•
Anselm, Monologion, Proslogion, and the exchange with Gaunilo, in Anselm: Basic Writings.
•
Sandra Visser and Thomas Williams, “The Argument of the Proslogion,” in Anselm.
•
Brian Davies, “The Ontological Argument,” in Brian Davies and Brian Leftow, eds., The Cambridge Companion to Anselm.
•
Norman Malcolm, “The Second Form of the Ontological Argument,” reprinted in Hick, Reader, pp. 350ff.
•
J.J.C. Smart, “The Existence of God,” reprinted in Robinson, God, pp. 44–57.
Dr. Philip Cannata
20
Gödel's Incompleteness Theorems – see Delong pages, 165 - 180
Gödel showed that any system rich enough to express primitive recursive
arithmetic (i.e., contains primitive recursive arithmetic as a subset of
itself) either proves sentences which are false or it leaves unproved
sentences which are true … in very rough outline – this is the reasoning
and statement of Gödel's first incompleteness theorem. [ DeLong page,
162]
Wikipedia - The first incompleteness theorem states that no consistent
system of axioms whose theorems can be listed by an "effective
procedure" (e.g., a computer program, but it could be any sort of
algorithm) is capable of proving all truths about the relations of the
natural numbers (arithmetic). For any such system, there will always be
statements about the natural numbers that are true, but that are
unprovable within the system. The second incompleteness theorem, an
extension of the first, shows that such a system cannot demonstrate its
own consistency.
Dr. Philip Cannata
21
Gödel Numbering
1
3
5
7
9
11
13
17
19
23
‘0’
‘’’
‘-’
‘=>’
‘V’
‘(‘
‘)
‘x’
‘y’
‘z’
29
31
37
41
43
47
53
…
‘=‘
‘+’
‘.’
‘x1’
‘y1’
‘z1’
‘z2’
…
1 = (0)’ = 211 x 31 x 513 x 73
The following proof would be a sequence of symbols which would
correspond to a single Gödel number (see DeLong page 167 for
another example
(0’’ 0 0’’)
(0’’ 0’ (0’’ 0 x)’)
=> (0’’ 0’ (0’’)’) => (0’’ 0’ 0’’’)
Dr. Philip Cannata
22
Gödel's Incompleteness Theorem
If “proof” is a proof of “statement”
then P is True.
If you have a statement g with variable x and if, when
you substitute g for x, you produce “statement” then Q is
True.
not P(proof, statement) && Q(x, statement) = g
Let g be the
Gödel number for
this statement,
A recursive notion.
But now science, spurred on by its powerful delusion, hurtles inexorably towards its limits where the
optimism hidden in the essence of logic founders. For the periphery of the circle of science has an
infinite number of points and while there is no telling yet how the circle could ever be fully surveyed,
the noble and gifted man, before he has reached the middle of his life, still inevitably encounters such
peripheral limit points and finds himself staring into an impenetrable darkness. If he at that moment
sees to his horror how in these limits logic coils around itself and finally bites its own tail - then the
new form of knowledge breaks through, tragic knowledge, which in order to be tolerated, needs art as a
protection and remedy.
Friedrich Nietzsche (1844 - 1900) The Birth of Tragedy
not P(proof, statement) && Q(g, statement) = s
Let s be the Gödel number
for this statement but by
the definition of Q that
means “statement” is “s”.
not P(proof, s) && Q(g, s) - I am a statement that is not provable.
There are Predicate Logic Statements that are True that can’t be proved True
(Incompleteness) and/or there are Predicate Logic Statements that can be proved True that
are actually False ( Inconsistent Axioms or Unsound inference rules).
i.e., If Gödel's statement is true, then it is a example of something that is true for which there is no proof.
If Gödel's statement is false, then it has a proof and that proof proves the false Gödel statement true.
Dr. Philip Cannata
23
Limitive Theorems
Limitive Theorems
Theorem
Language of Psychology
Gödel's first incompleteness
theorem
There is no consistent human
computer capable of formulating
a program which, if carried out,
would produce all the true and
only the true sentences of
arithmetic.
There is no consistent
computing machine which can
be programmed to produce all
the true and only the true
sentences of arithmetic.
Gödel's second incompleteness
theorem
No consistent human computer
can prove an effective or
constructive expression of its
own consistency (see page 222).
No consistent computing
machine can be programmed to
prove a computable or
computably enumerable
expression of its own
consistency (see page 222).
See page 200
(This depends on Church’s
theorem).
Dr. Philip Cannata
Language of Physics
(This depends on Church’s
theorem).
Church’s theorem
There exists a set of problems
which no consistent human
computer can solve.
There exists a set of problems
which no consistent computing
machine can be programmed to
solve.
Skolem’s theorem
No consistent human computer
can (categorically) formalize the
notion of natural number.
No consistent computing
machine can be programmed to
produce a (categorical)
formalization of the notion of
natural number.
24
Gödel's Incompleteness Theorem
I am a statement that is not provable.
There are Predicate Logic Statements that are True that can’t be proved True
(Incompleteness) and/or there are Predicate Logic Statements that can be proved True that
are actually False ( Inconsistent Axioms or Unsound inference rules).
i.e., If Gödel's statement is true, then it is a example of something that is true for which there is no proof.
If Gödel's statement is false, then it has a proof and that proof proves the false Gödel statement true.
Logic/Math/CS
Physics
Theology
Philosophy
Plotinus
Unsound
Superposition
S
L
F
T
P
Consubstantial
G
W
F
S
The ONE
Is nothing else but The ONE,
it can’t even be finite.
H
Plato
The Forms (e.g. Justice)
Opposite is Excluded Middle
~p or p
Dr. Philip Cannata
Self
Other
Trace of
The One
Finite
…
25
Gödel's Incompleteness Theorem
Dr. Philip Cannata
26
Dr. Philip Cannata
27
Dr. Philip Cannata
28
From “An
American
Election Season”,
Scientific
American,
November, 2012
Dr. Philip Cannata
29
Dr. Philip Cannata
30