AI.THROOP@R20.UTEXAS.EDU (David Throop) (11/08/85)
Received: from CSNET-RELAY.ARPA (csnet-pdn-gw) by rand-unix.ARPA; Fri, 8 Nov 85 06:19:54 pst
Received: from smu by csnet-relay.csnet id ad07516; 8 Nov 85 9:07 EST
Received: by csevax.smu (4.12/4.7)
id AA24841; Thu, 7 Nov 85 11:25:02 cst
Date: 7 Nov 1985 11:23-CST
From: leff%smu.csnet@CSNET-RELAY.ARPA
Subject: Forwarded from AIList to net.math.symbolic
Message-Id: <500232181/leff@smu>
Date: Tue 5 Nov 85 15:21:35-CST
From: David Throop <AI.THROOP@R20.UTEXAS.EDU>
Subject: Seminar - The Boyer-Moore Theorem Prover (UTexas SIGART)
SIGART, the Special Interest Group on ARTificial Intelligence, has its
monthly program meeting WEDNESDAY, 6 Nov, at JIMS restaurant at I-35 and
183 (Anderson). The speaker will be Dr J S Moore, speaking on:
Applications of the Boyer-Moore Theorem Prover to
the Verification of Computer Hardware and Software
J Strother Moore
The Boyer-Moore Theorem Prover is computer program that
proves theorems about recursive functions. The primary
application of the program is to prove formulas that
establish the correctness, reliability, or security of
computer hardware and software.
The proof techniques used by the system include rule driven
simplification, generalization of the conjecture to be
proved, and mathematical induction. Each time a formula is
proved the theorem-prover builds it into an evolving
knowledge base which is used to structure subsequent proofs.
Thus, the human user of the system can improve the system's
performance by having it prove key lemmas first. As the
theorems get harder the user's role in the process more and
more resembles that of the mathematician who sketches proofs
before an assistant who fills in the often large gaps.
In this talk I will informally explain how the system works
and how it is used. I will also discuss some applications
of the system, including its use in finding security flaws
in the formal specifications of computer software, its proof
of the invertibility of the RSA public key encryption
algorithm, and the correctness proofs for a general purpose
microcoded CPU.
____________________________________________________________________________
The following is forwared because of the use of the symbolic
manipulation system, PRESS:
Date: Mon, 4 Nov 85 15:24 EST
From: Tim Finin <Tim%upenn.csnet@CSNET-RELAY.ARPA>
Subject: Seminar - AI in Design and Manufacture (UPenn)
Professor Robin Popplestone
Department of AI at Edinburgh University
will give a lecture on
Applying AI Techniques to Design and Manufacturing
Today: Monday, November 4 at NOON in Towne Building, Room 303
I discuss the representation of mechanical engineering designs in a logic
programming context, and the exploration of a space of different possible
designs. Designs are represented in terms of modules, which are basic
concrete engineering entities (eg. motor, keyway, shaft). Modules interact
via ports, and have an internal structure expressed by the part predicate. A
taxonomic organisation of modules is used as the basis for making design
decisions. Subsystems employed by the design system include the spatial
relational inference mechanism employed in the RAPT robot Language, the Noname
geometric modeller developed at Leeds Univeristy and the Press symbolic
equation solver. The system is being implemented in the POPLOG system. An
assumption based truth maintenance system based on the work of de Kleer is
being implemented to support the exploration of design space.