Thread View: capdist.seminars
1 messages
1 total messages
Started by Pat Keller
Wed, 24 Mar 1999 00:00
SUNYA C. S. Dept. Colloquium
Author: Pat Keller
Date: Wed, 24 Mar 1999 00:00
Date: Wed, 24 Mar 1999 00:00
32 lines
2126 bytes
2126 bytes
PH.D. STUDENT TALKS
University at Albany - State University of New York
Computer Science Department
Unification Revisited
Nobuyuki Shimizu
Thursday, March 25, 1999, at 1:00p.m.****, in LI-98
ABSTRACT
Since published by J. A. Robinson on 1965, the princi-
ples of resolution has been widely used in logic programming
and artificial intelligence, allowing us to make deductions
based on concepts expressed in first order logic. Unifica-
tion is a step in a resolution proof that seeks to unify two
predicates, thereby allowing a chain of reasoning. For
example, suppose there are two prepositions: "Socrates is a
human" and "if x is a human, then x is a mortal." Simply
put, unification is a method to match "Socrates is a human"
and "x is a human," replacing every occurrence of x with
Socrates so that we may infer "Socrates is a mortal."
Although the example above does not follow steps required
for a resolution proof, it illustrates a need for unifica-
tion in reasoning. The topic of this talk is a new formali-
zation of unification that appeared since 1965, which I
believe is mathematically simpler to grasp than the original
formalization.
Thread Navigation
This is a paginated view of messages in the thread with full content displayed inline.
Messages are displayed in chronological order, with the original post highlighted in green.
Use pagination controls to navigate through all messages in large threads.
Back to All Threads