Subject: From: AIList Moderator Kenneth Laws <AIList-REQUEST%sri-ai.arpa@CSNET-RELAY>

From: [email-masked]
Date: Thu, 23 Jan 86 02:46:24 est

Received: from sri-ai.arpa by CSNET-RELAY.ARPA id a001571; 22 Jan 86 16:40 EST
Date: Wed 22 Jan 1986 13:17-PST
Reply-to: AIList%sri-ai.arpa@CSNET-RELAY
US-Mail: SRI Int., 333 Ravenswood Ave., Menlo Park, CA  94025
Phone: (415) 859-6467
Subject: AIList Digest   V4 #13
To: AIList%sri-ai.arpa@CSNET-RELAY
Received: from rand-relay by vpi; Thu, 23 Jan 86 02:28 EST

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

                  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 <[email-masked]>
Subject: Seminar - Problem Solving for Distributed Systems (MIT)

       [Forwarded from the MIT bboard by [email-masked].]

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