AIList-REQUEST@SRI-AI.ARPA (AIList Moderator Kenneth Laws) (01/23/86)
AIList Digest Thursday, 23 Jan 1986 Volume 4 : Issue 13
Today's Topics:
Seminars - Controlling Backward Inference (SRI) &
Automata Approach to Program Verification (MIT) &
Problem Solving for Distributed Systems (MIT) &
Problem-Solving Languages (CSLI) &
Pointwise Circumscription (SU) &
Methodological Issues in Speech Recognition (Edinburgh) &
Intuitionistic Logic Programming (UPenn)
----------------------------------------------------------------------
Date: Wed 15 Jan 86 15:22:41-PST
From: LANSKY@SRI-AI.ARPA
Subject: Seminar - Controlling Backward Inference (SRI)
CONTROLLING BACKWARD INFERENCE
Dave Smith (DE2SMITH@SUMEX-AIM)
Stanford University
11:00 AM, MONDAY, January 20
SRI International, Building E, Room EJ228 (new conference room)
Effective control of inference is a critical problem in Artificial
Intelligence. Expert systems have made use of powerful
domain-dependent control information to beat the combinatorics of
inference. However, it is not always feasible or convenient to
provide all of the domain-dependent control that may be needed,
especially for systems that must handle a wide variety of inference
problems, or must function in a changing environment. In this talk a
powerful domain-independent means of controlling inference is
proposed. The basic approach is to compute expected cost and
probability of success for different backward inference strategies.
This information is used to select between inference steps and to
compute the best order for processing conjuncts. The necessary
expected cost and probability calculations rely on simple information
about the contents of the problem solvers database, such as the number
of facts of each given form and the domain sizes for the predicates
and relations involved.
------------------------------
Date: 01/16/86 17:18:02
From: LISA at MC.LCS.MIT.EDU
Subject: Seminar - Automata Approach to Program Verification (MIT)
[Forwarded from the MIT bboard by SASW@MC.LCS.MIT.EDU.]
DATE: Thursday, January 23, 1986
TIME: 3:45 p.m......Refreshments
4:00 p.m......Lecture
PLACE: NE43 - 512A
"AN AUTOMATA-THEORETIC APPROACH TO
AUTOMATIC PROGRAM VERIFICATION"
MOSHE Y. VARDI
IBM Almaden Research Center
We describe an automata-theoretic approach to automatic verification of
concurrent finite-state programs by model checking. The basic idea underlying
the approach is that for any temporal formula PHI we can construct an automaton
A(PHI) that accepts precisely the computations that satisfy PHI. The
model-checking algorithm that results from this approach is much simpler and
cleaner than tableaux-based algorithms. We also show how the approach can be
extended to probabilistic concurrent finite-state programs.
Albert Meyer
Host
------------------------------
Date: Thu 16 Jan 86 11:49:34-EST
From: John J. Doherty <JOHN@XX.LCS.MIT.EDU>
Subject: Seminar - Problem Solving for Distributed Systems (MIT)
[Forwarded from the MIT bboard by SASW@MC.LCS.MIT.EDU.]
Date: January 24, 1986
Place: NE43-512A
Time: Refreshments 2:15 P.M.
Seminar 2:30 P.M.
Problem Solving for Distributed Systems:
An Uplifting Experiment in Progress
Herb Krasner
Member of the Technical Staff
MCC
Software Technology Project
This presentation describes the empirical studies efforts of the STP
Design Process Group focusing on models of the design process.
Preliminary findings of the "lift" experiment are reported, from which
a model of expert designer behavior and high leverage characteristics is
being derived. Goals of the pilot study, experimental setup, problem,
data analysis technique, hypotheses and subsequent activities are
discussed. The "lift" experiment was initiated to examine the early
stages of design problem solving behavior prototypical of users of
the futuristic software design environment LEONARDO. It addresses
the large effect of individual differences on productivity data,
and differs from previous studies in its focus on large-scale
design problems.
Host: Irene Greif
------------------------------
Date: Wed 15 Jan 86 16:52:56-PST
From: Emma Pease <Emma@SU-CSLI.ARPA>
Subject: Seminar - Problem-Solving Languages (CSLI)
[Excerpted from the CSLI Newsletter by Laws@SRI-AI.]
CSLI ACTIVITIES FOR NEXT THURSDAY, January 23, 1986
2:15 p.m. CSLI Seminar
Computer Problem Solving Languages, Programming
Languages and Mathematics
Curtis Abbott (Abbott@xerox)
Computer Problem Solving Languages,
Programming Languages and Mathematics
by the
Semantically Rational Computer Languages Group
Programming languages are constrained by the requirement that their
expressions must be capable of giving rise to behavior in an
effective, algorithmically specified way. Mathematical formalisms,
and in particular languages of logic, are not so constrained, but
their applicability is much broader than the class of problems anyone
would think of ``solving'' with computers. This suggests, and I
believe, that formal languages can be designed that are connected with
the concerns associated with solving problems with computers yet not
constrained by effectiveness in the way programming languages are. I
believe that such languages, which I call ``computer problem solving
languages,'' provide a more appropriate evolutionary path for
programming languages than the widely pursued strategy of designing
``very high level'' programming languages, and that they can be
integrated with legitimate programming concerns by use of a
transformation-oriented methodology. In this presentation, I will
give several examples of how this point of view impacts language
design, examples which arise in Membrane, a computer problem solving
language I am in the process of designing. --Curtis Abbot
------------------------------
Date: 17 Jan 86 1639 PST
From: Vladimir Lifschitz <VAL@SU-AI.ARPA>
Subject: Seminar - Pointwise Circumscription (SU)
Pointwise Circumscription
Vladimir Lifschitz
Thursday, January 23, 4pm, MJH 252
(I have a few copies of the paper in my office, MJH 362).
ABSTRACT
Circumscription is logical minimization, that is, the
minimization of extensions of predicates subject to restrictions
expressed by predicate formulas. When several predicates are to be
minimized, circumscription is usually thought of as minimization with
respect to an order defined on vectors of predicates, and different
ways of defining this order correspond to different kinds of
circumscription: parallel and prioritized.
The purpose of this paper is to discuss the following
principle regarding logical minimization:
Things should be minimized one at a time.
This means, first of all, that we propose to express the
circumscription of several predicates by the conjunction of several
minimality conditions, one condition for each predicate. The
difference between parallel and prioritized circumscription will
correspond to different selections of predicates allowed to vary in
each minimization.
This means, furthermore, that we propose to modify the
definition of circumscription so that it will become an "infinite
conjunction" of "local" minimality conditions; each of these
conditions expresses the impossibility of changing the value of the
predicate from True to False at one point. (Formally, this "infinite
conjunction" will be represented by means of a universal quantifier).
This is what we call "pointwise circumscription".
We argue that this approach to circumscription is conceptually
simpler than the traditional ``global'' approach and, at the same
time, leads to generalizations with the additional flexibility and
expressive power needed in applications to the theory of commonsense
reasoning. Its power is illustrated, in particular, on a problem posed
by Hanks and McDermott, which apparently cannot be solved using other
existing formalizations of non-monotonic reasoning.
------------------------------
Date: Tue, 21 Jan 86 10:44:43 GMT
From: Gideon Sahar <gideon%edai.edinburgh.ac.uk@cs.ucl.ac.uk>
Subject: Seminar - Methodological Issues in Speech Recognition (Edinburgh)
Department of Artificial Intelligence, University of Edinburgh,
and Artificial Intelligence Applications Institute
Edinburgh Artificial Intelligence Seminars
Speaker - Dr. Henry Thompson, Dept. of A.I., University of Edinburgh
Title - Methodological issues in Speech Recognition
Abstract - What methodological issues arise from the belief that fully
automatic high quality unrestricted speech recognition is impossible,
when one has overall technical responsibility for a multi-year
multi-million pound Alvey Large Scale Demonstrator? I will give a
brief overview of the overall structure of the project, and discuss at
more length two basic issues:
- Why top-down vs. bottom-up is the wrong question, and selectional vs.
instructional interaction is the right question, and what the right
answer is.
- How giving up on fully automatic ... changes the way you do things
in surprising ways.
------------------------------
Date: Tue, 21 Jan 86 23:27 EST
From: Tim Finin <Tim%upenn.csnet@CSNET-RELAY.ARPA>
Subject: Seminar - Intuitionistic Logic Programming (UPenn)
From: Dale Miller <Dale@UPenn>
UPenn Math-CS Logic Seminar
An Intuitionistic Basis for Extending Logic Programming
Dale Miller
Tuesday 28 Jan 86, 4:30 - 6:00, 4E17 DRL
There is a very natural extension to Horn clauses which involves extending
the use of implication. This extension has a natural operational semantics
which is not sound with respect to classical logic. We shall show that
intuitionistic logic, via possible worlds semantics, provides the necessary
framework to give a sound and complete justification of this operational
semantics. This will be done by providing a least fix-point construct of a
Kripke-model. We shall also show how this logic can be used to provide
logic programming languages with a logical foundations for each of the
following programming features: program modules, recursive call memo-izing,
and local environments (permanent vs. temporary asserts). This extension to
logic programming can also simulate various features of negation - not
through logical incompleteness as in negation-by-failure, but through
constructing proofs of a certain kind.
------------------------------
End of AIList Digest
********************