AIList-REQUEST@SRI-AI.ARPA (AIList Moderator Kenneth Laws) (12/20/85)
AIList Digest Friday, 20 Dec 1985 Volume 3 : Issue 190
Today's Topics:
Seminars - Example-Based Reasoning (UPenn) &
Clausal Intuitionistic Logic (UPenn) &
Robot Control with Kinesthetics (UPenn) &
HORNLOG: Horn Clause Logic with Graph Rewriting (UPenn),
Course - Deduction and Computation (CMU) &
Symbolic Computation (UTexas)
----------------------------------------------------------------------
Date: Tue, 17 Dec 85 09:50 EST
From: Tim Finin <Tim%upenn.csnet@CSNET-RELAY.ARPA>
Subject: Seminar - Example-Based Reasoning (UPenn)
3pm Tuesday, December 17, 1985
Room 216 Moore School
University Of Pennsylvania
EXAMPLE-BASED REASONING
EDWINA L. RISSLAND, HARVARD
In this talk, I shall discuss example-based reasoning, particularly in the
contexts of assisting in the preparation of legal arguments and offering
on-line explanations. In the case of legal argumentation, I discuss how
hypotheticals serve a central role in analyzing the issues in a case and
describe a program, called HYPO, which generates legal hypotheticals, and an
environment, called COUNSELOR, which provides support for legal reasoning and
other strategic tasks, like resource management. I'll briefly describe our
current work on on-line assistance and how we are trying to make it more
intelligent by embedding custom-tailored examples in the explanations. I'll
also discuss some general issues about examples such as their generation,
structure and importance in reasoning, especially in the domains of mathematics
and the law.
------------------------------
Date: Tue, 17 Dec 85 09:50 EST
From: Tim Finin <Tim%upenn.csnet@CSNET-RELAY.ARPA>
Subject: Seminar - Clausal Intuitionistic Logic (UPenn)
3pm Thursday, December 19, 1985
Room 216 Moore School
University of Pennsylvania
FIXED POINT SEMANTICS AND TABLEAU PROOF PROCEDURES
FOR A CLAUSAL INTUITIONISTIC LOGIC
L. THORNE MCCARTY
COMPUTER SCIENCE DEPARTMENT
RUTGERS UNIVERSITY
Since the advent of Horn clause logic programming in the mid-1970's, there have
been numerous attempts to extend the expressive power of Horn clause logic
while preserving some of its attractive computational properties. This talk
will present a clausal language which extends Horn clause logic by adding
negations and embedded implications to the right hand side of a rule, and which
interprets these new rules intuitionistically, in a set of partial models. The
resulting system will be shown to have a fixed point semantics which resembles
the fixed point semantics of Horn clauses, and a tableau proof procedure which
generalizes Horn clause refutation proofs. Soundness and Completeness results
will also be presented. Finally, the talk will outline some connections
between this clausal intuitionistic logic and several familiar forms of
non-monotonic reasoning.
------------------------------
Date: Thu, 19 Dec 85 14:10 EST
From: Tim Finin <Tim%upenn.csnet@CSNET-RELAY.ARPA>
Subject: Seminar - Robot Control with Kinesthetics (UPenn)
Ph.D. Dissertation Proposal Presentation
3:00pm Friday, Dec. 20, 1985
554 Moore School
University of Pennsylvania
ROBOT CONTROL WITH KINESTHETICS: A REAL TIME EXPERT SYSTEM
Russell L. Andersson
The utility of robots is directly determined by the activities they can
perform and the speed with which they can perform them. The purpose of
this research is to develop means to improve the performance of robots,
both in speed and especially in functionality. We maintain that the
robots are already being limited by their controllers; rather than
redesign the robot itself, we address the problem of how to improve the
controller. Our approach is to create a sense of kinesthetics: to make
more information about the robot available to the controller, and to
find ways to use it. Kinesthetics requires operation in both the
numeric and symbolic domains, so the system must be capable of using
and interconverting both domains. We propose an expert system and a
means to compile it to a form executable in real time.
------------------------------
Date: Thu, 19 Dec 85 14:10 EST
From: Tim Finin <Tim%upenn.csnet@CSNET-RELAY.ARPA>
Subject: Seminar - HORNLOG: Horn Clause Logic with Graph Rewriting (UPenn)
Ph.D. Dissertation Proposal Presentation
3:00pm Friday, Dec. 20, 1985
554 Moore School
University of Pennsylvania
INVESTIGATIONS INTO HORNLOG:
A HORN CLAUSE INTERPRETER BASED ON GRAPH REWRITING
Stan Raatz
HORNLOG, due to Jean Gallier, is a Horn clause proof procedure that can
be used to interpret logic programs. The system is not resolution-based,
but rather is based on a form of graph-rewriting and a linear-time
algorithm for testing the unsatisfiability of propositional Horn
formulae. HORNLOG applies to a class of logic programs which is a
proper superset of the class of logic programs handled by PROLOG
systems. In particular, negative Horn clauses used as assertions and
queries consisting of disjunctions of negations of Horn clauses are
allowed. This class of logic programs admits answers which are
indefinite, in the sense that an answer can consist of a disjunction of
substitutions. The method does not use negation by failure semantics in
handling these extensions.
In this proposal, using the HORNLOG procedure, we develop a theory and
give examples of a type of logic programming called "general Horn clause
programming. We give soundness and completeness results,
show that the procedure has an immediate parallel interpretation, and argue
that the method compares favorably with SLD-resolution in a parallel
environment. In addition, two extensions are outlined: (1) the inclusion of
term-rewriting to handle certain instances of equational programming,
and (2) an uncertainty calculus for expert system applications.
------------------------------
Date: 16 Dec 1985 1005-EST
From: Lydia Defilippo <DEFILIPPO@C.CS.CMU.EDU>
Subject: Course - Deduction and Computation (CMU)
[Forwarded from the CMU bboard by Laws@SRI-AI.]
DEDUCTION AND COMPUTATION
A Spring Seminar Proposal
Gerard huet
Course No.: 15-850B
Starting Date: 9 January 1986
Tuesdays and Thursdays from 10:00 - 11:30 am
Place: 5409 Wean Hall
The seminar will consist in two distinct phases. The first phase will be
a standard course, and will last 8 weeks. The topics covered include basics of
proof theory, such as sequent calculus, equational logic, canonical rewriting
and natural deduction, and foundations of applicative programming languages,
such as lambda calculus, combinators, sequential computations, types and
polymorphism. The course ends with a more advanced section on the
Constructions Calculus. The course is completely self-contained, there is no
pre-requisite. Course notes will be available.
The second phase, for the remaining 6 weeks, will be an advanced seminar
on the computer automation of constructive mathematics. The participants will
group themselves in teams, and attempt to develop mechanical proofs of selected
theorems on the implementation of the Constructions Calculus. A team may
consist in 1 to 3 participants. It is expected that terms will balance
mathematical and programming talents for maximum efficiency. Each team will
have access to a computer running an implementation of the Constructions
Calculus. The goal of the seminar is to produce a uniform document describing
the results of the experiments.
------------------------------
Date: Tue 17 Dec 85 18:48:00-CST
From: AI.HASSAN@MCC.ARPA
Subject: Course - Symbolic Computation (UTexas)
[Forwarded from the UTexas bboard by Laws@SRI-AI.]
SYMBOLIC COMPUTATION
Graduate Seminar Proposal
CS395-T
Spring 1986
Dr. Hassan Ait-Kaci
This course is intended as a bridge between Theory and Practice. It
will consist of a tutorial on symbolic computation models based on
functional, algebraic, and logical calculi, as well as advanced
state-of-the-art in next-generation programming language research. The
main focus will be on explaining how some abstract concepts derived
from Logic and Universal Algebra can be used to describe symbolic
computation and data structures, and how these concepts may be
implemented efficiently. During the course, many existing as well as
original experimental examples will be scrutinized in detail.
TENTATIVE OUTLINE
1. Mathematics for Symbolic Computation
a. Lambda-Calculus
b. Universal Algebra
c. Predicate Logic
2. Functional Computation
a. Applicative Programming
b. Interpreting the Lambda-Calculus
c. Compiling the Lambda-Calculus (SECD Machine)
d. Extensions
i. Delayed-Evaluation and Streams
ii. Non-Deterministic Computations
iii. Binding by Unification
3. Algebraic Computation
a. Term Rewriting
b. Knuth-Bendix Completion Method
c. Rewriting Termination
d. Resolution of Equations (Narrowing, Congruence Closure)
e. Equational Logic Programming
4. Logic Computation
a. Horn Clause Resolution
b. Compiling Horn Clause Resolution
c. Extensions
i. Building-In Equations
ii. Building-In Inheritance
iii. Non-Horn Logic Programming
iv. Higher-Order Logic Programming
5. Unifying Principle: The Categorical Abstract Machine
6. Data Types
a. Algebraic Abstract Data Types
b. Polymorphic Types (Universal and Existential)
c. Constructive Type Theory
PREREQUISITE: Although meant to be self-contained, this course will
offer optimal benefit to anyone acquainted with senior-level discrete
mathematics and computer programming. The only *real* prerequisite is
an open mind.
PARTICIPATION: Students will be expected to participate actively in
presentations of assigned readings, implementation of experimental
programs, and in completing either a term paper or a programming
project.
TEXT: Most of the material covered will be taken from articles, and
extensive notes written by the instructor. A (far from exhaustive)
list of recommended books would be (1) Burge's "Recursive Programming
Technique", (2) Henderson's "Functional Programming" (3) Campbell's
(Ed.) "Implementations of Prolog", as well as anything else related to
the outlined topics.
ENROLLMENT: This course will be given only if at least 5 students
register. Anybody interested in *registering* is encouraged to contact
Hassan Ait-Kaci at 834-3354, ARPA address "Hassan@mcc", AS SOON AS
POSSIBLE!
------------------------------
End of AIList Digest
********************