Subject: AIList Digest V3 #190

From: AIList Moderator Kenneth Laws <seismo!SRI-AI.ARPA!AIList-REQUEST>
Date: Fri 20 Dec 1985 09:25-PST

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 <[email-masked]>
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 <[email-masked]>
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 <[email-masked]>
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 <[email-masked]>
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 <[email-masked]>
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: [email-masked]
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
********************