Copy Link
Add to Bookmark
Report
AIList Digest Volume 5 Issue 115
AIList Digest Monday, 11 May 1987 Volume 5 : Issue 115
Today's Topics:
Seminars - Reporting the Non-Monotonic News (BTL) &
Should McCarthy and Feigenbaum Talk to Each Other (SU) &
Qualitative Mechanical Reasoning (UPenn) &
Semi-Automatic Construction of Control Software (UPenn) &
Explaining and Refining Decision-Theoretic Choices (UPenn) &
General E-Unification (UPenn)
----------------------------------------------------------------------
Date: Thu 23 Apr 1987 13:50:34
From: dlm.allegra%btl.csnet@RELAY.CS.NET
Subject: Seminar - Reporting the Non-Monotonic News (BTL)
May 7th 10:30 AM
AT&T Bell Laboratories - Murray Hill 1E-449
REPORTING THE NON-MONOTONIC NEWS:
Keeping the Beat Local
Benjamin Grosof
Stanford University
"Non-monotonic" reasoning systems are ones in which some conclusions
have a default or retractable status. A prime motivation for such
systems is to build agents that revise their beliefs in response to
news from their environment. Efficient updating is problematic,
however, because adding new information in general may require the
revision of many, or even all, previous retractable conclusions. An
understanding is needed of the "partial monotonicities" of updating,
i.e. of the irrelevance of updates to parts of the previous
retractable conclusions.
To define non-monotonic theories, we introduce a formalism based on
McCarthy's circumscription that directly expresses, as axioms, both
default beliefs and preferences among default beliefs. It has a
strong semantics based on first- and second-order logic. We
characterize non-monotonic theories as hierarchically decomposable
in a manner more analogous to programming languages than to ordinary
monotonic logics. We then give a set of results about partial
monotonicities of updating. We discover some surprising differences
between updates consisting of default axioms and those consisting of
non-retractable axioms. These results bear on a wide variety of
applications of non-monotonic reasoning.
Sponsor: R.J.Brachman
------------------------------
Date: 22 Apr 87 1556 PDT
From: Vladimir Lifschitz <VAL@SAIL.STANFORD.EDU>
Subject: Seminar - Should McCarthy and Feigenbaum Talk to Each Other
(SU)
SHOULD JOHN MCCARTHY AND ED FEIGENBAUM
TALK TO EACH OTHER?
Thursday, April 23, 4:15pm
Bldg. 160, Room 161K
Matt Ginsberg
In this talk, I discuss one possible way to bridge the apparently
widening gap between the "neats" and the "scruffies" in AI. According
to Kuhn, a necessary step in resolving the differences between the
two camps is that one attack problems of interest to the other.
I attempt to do this by suggesting that the scruffy programs
are doing essentialy two things: a recognizable approximation
to first-order inference (such as MYCIN's backward chaining), and
some sort of bookkeeping with the results returned (e.g., manipulation
of certainty factors).
Formalizing this bookkeeping is attractive for a variety of reasons:
it will allow precise statements to be made about what the scruffies'
programs are doing, and may lead to more effective implementations of
their ideas. There are also advantages for the neats, since understanding
some of the proposed extensions to first-order inference in this fashion
appears to lead to computationally tractable algorithms for some simple
non-mononotonic logics.
If time permits, I will present a formalization which appears to
have the properties described in the previous paragraph.
------------------------------
Date: Fri, 24 Apr 87 22:29:33 AST
From: tim@linc.cis.upenn.edu (Tim Finin)
Subject: Seminar - Qualitative Mechanical Reasoning (UPenn)
Qualitative reasoning of mechanical devices and repair automation
Pearl Pu
COmputer and Information Science
University of Pennsylvania
216 Moore School
1pm April 28, 1987
A knowledge representation scheme, QUORUM (QUalitative reasoning of
Repair and Understanding of Mechanisms), has been constructed to apply
qualitative techniques to the mechanical domain, which is an area that
has been neglected in qualitative reasoning field. In addition, QUORUM
aims at providing foundations for the construction of a repair expert
system.
The problem in constructing a representation is the difficulty of
recognizing a feasible ontology with which we can express the behavior
of mechanical devices and, more importantly, faulty behaviors of a
device and its cause. Unlike most other approaches, our ontology
employs the notion of force and energy transfer, and motion
propagation. We discuss how the overall behavior of a device can be
derived from the knowledge about the structure and topology of the
device, and how faulty behaviors can be predicted based on information
about the perturbation of some of the original conditions of the
device. Necessary predicates and functions are constructed to express
the physical properties of a wide variety of basic and complex
mechanisms, and the interconnection relationships among the parts of a
mechanism. Several examples analyzed with QUORUM include a pair of
gears, a spring-driven cam mechanism, and a pendulum clock. An
algorithm for the propagation of force, motion, and causality is
proposed and examined.
------------------------------
Date: Mon, 27 Apr 87 16:31:00 EDT
From: tim@linc.cis.upenn.edu (Tim Finin)
Subject: Seminar - Semi-Automatic Construction of Control Software
(UPenn)
CIS COLLOQUIUM
UNIVERSITY OF PENNSYLVANIA
The Semi-Automatic Construction of Large Software Control System
David Bourne, Research Scientist, Robotics Institute, Carnegie Mellon
Large manufacturing software systems have taken many man-years of
effort to build in the past. For example, it is not uncommon for even a
small robotic cell to take several man years of effort to construct. Most
of this effort is spent over-coming the communication incompatibilities
(protocols and programming languages) that exist between machines from
multiple vendors. This talk presents a new AI programming language (CML -
the Cell Management Language) that greatly simplifies these major
difficulties. In addition, control systems for manufacturing will be
logically decomposed into several layers, and for each layer a semi-automatic
software tool will be described for constructing that layer in a new
application.
Thursday, April 30, 1987
3:00 - 4:30
Room 216
The Faculty Lounge
2:30 - 3:00
------------------------------
Date: Tue, 28 Apr 87 23:59:45 EDT
From: tim@linc.cis.upenn.edu (Tim Finin)
Subject: Seminar - Explaining and Refining Decision-Theoretic Choices
(UPenn)
EXPLAINING AND REFINING DECISION-THEORETIC CHOICES
Doctoral Thesis Proposal
Dave Klein
Computer and Information Science
University of Pennsylvania
As the need to make complex choices among competing alternative actions
is ubiquitous, the reasoning machinery of many intelligent systems will
include an explicit model for making choices. Decision analysis is
particularly useful for modelling such choices, and its potential for use
in intelligent systems motivates the construction of facilities for
automatically explaining decision-theoretic choices and for helping
users to incrementally refine the knowledge underlying them.
The proposed thesis addresses the problem of providing such
facilities. Specifically, we propose the construction of a
domain-independent facility called UTIL for explaining and refining a
restricted but widely applicable decision-theoretic model called the
additive multiattribute value model. We anticipate that this research
will provide contributions to both AI and decision analysis. In this
talk, the relevant issues are addressed in the context of examples
from the domain of intelligent process control.
Thursday, 30 April 1987
10:00 AM
5th floor conference room
Committee:
Dr. T.W. Finin (advisor)
Dr. N.I. Badler (chairman)
Dr. A.K. Joshi
Dr. E.K. Clemons (Wharton/Penn CIS)
Dr. E.H. Shortliffe (Stanford)
Dr. M.O. Weber (Institute fuer Wirtschaftswissenschaften, RWTH Aachen,
Germany)
------------------------------
Date: Wed, 29 Apr 87 00:04:32 EDT
From: tim@linc.cis.upenn.edu (Tim Finin)
Subject: Seminar - General E-Unification (UPenn)
PhD Dissertation Proposal
General E-Unification:
Complete Transformations for Equational
Theorem Proving and Logic Programming
Wayne Snyder
Computer and Information Science
University of Pennsylvania
There has been much work in the past two decades on the problem of
incorporating methods for equational reasoning into computational
logic. Unfortunately, the ``substitution of equals for equals'' which
forms the basis of equational reasoning is fundamentally different
from the analytic methods used for non-equational reasoning, which are based
on an interpretation of the connectives in the language. This dicotomy
has convinced many researchers that we should stratify theorem provers
into a (non-equational) refutation mechanism and an E-unification
mechanism which performs equational reasoning during unification steps,
so that two terms E-unify if they are unifiable modulo the congruence
on terms induced by the set of equations E. Many special purpose E-unification
procedures have been designed for particular equational theories, and
several also for the class of theories which can be compiled into
rewrite rules via the Knuth-Bendix procedure. So far the problem
of E-unification for arbitrary equational theories has received little
attention, and in general there seems to be a need for some integrated
approach which will show the structure of the class of all
E-unification problems.
Our current research attempts to address the problem of general
E-unification and higher-order unification by extending the method
of transformations on term systems, developed in the context of
standard unification by Martelli and Montanari. We hope that this
approach will provide not only a basis for practical procedures, but
also a means for analysing unification problems in an abstract and
mathematically elegant fashion. Our results so far include a completeness
proof for our procedure and a new analysis of the occur check problem
in E-unification. We propose to extend these methods to refutation
methods incorporating equality, to a fundamentally new form of
E-unification which has come up in the study of equational matings,
and to the problem of higher-order E-unification. It is our hope that
this research will not only yield interesting theoretical results,
but will also help us to find practical algorithms for theorem proving
and logic programming in the presence of equality.
Friday, May 1, 10:00am
556 Moore (Conference Room)
Supervisor: Dr. Jean Gallier
Committee: Dr. Dale Miller (Chairman)
Dr. Peter Buneman
Dr. Frank Pfenning (CMU)
Dr. Paliath Narendran (GE)
Dr. Andre Scedrov
------------------------------
End of AIList Digest
********************
