E1AR0002@SMUVM1.BITNET (06/04/86)
%A M. A. Fulk
%T A Study of Inductive Inference Machines
%R 85-10
%D August 1985
%I SUNY Buffalo Computer Science
%K AI04
%X Inductive inference machines (IIMs) model learning and
scientific theory formation.
We investigate
IIMs that attempt to synthesize (in the limit) a program for
a function as they receive data (in the form of input-output pairs)
about that function.
We show that a postdictively consistent IIM can be
effectively replaced with a postdictively complete IIM
that succeeds on all of the functions that the original did.
We also investigate IIMs that attempt to synthesize (again in the limit)
a program that enumerates an r.e. set as they receive data
consisting of the elements of that set.
Finally, we propose new criteria
for success in inductive inference.
%R 85-11
%A J. S. Royer
%T A connotational theory of program structure
%D September 1985
%I SUNY Buffalo Computer Science
%K AA08
%R 85-12
%T Local symmetry computation for shape description
%A G. W. Lee
%A S. N. Srihari
%D September 1985
%I SUNY Buffalo Computer Science
%K AI06
%R 85-13
%T ROCS: A system for reading off-line cursive script
%A R. M. Bo\o'z\(hc'inovi\o'c\(aa'
%A S. N. Srihari
%D September 1985
%I SUNY Buffalo Computer Science
%K AI06
%R UMCS-85-8-1
%A David E. Rydeheard
%A Rod M. Burstall
%T The Unification of Terms: A Category-Theoretic Algorithm
%I The University of Manchester, Department of Computer Science
%K AI11
%X no charge
As an illustration of the role of abstract mathematics in
program design, an algorithm for the unification of terms is derived
from constructions of colimits in category theory.
%A Trevor P. Hopkins
%R UMCS-85-9-2
%T Image Transfer by Packet-switched Network
%I The University of Manchester, Department of Computer Science
%K AI06
%X no charge
The advantages and disadvantages of
using packet-switching technology for the transfer of image information
in real time are considered. An experimental implementation
of parts of a system based on a high-speed
Local Area Network is described; these include a
simple screen output device and a real-time camera input device. The
generation of images using a number of microprocessors is also
described. A number of applications for such a system are
investigated and the extension of this approach to implement an
Integrated Information Presentation system is considered.
%A Howard Barringer
%R UMCS-85-9-3
%T Up and Down the Temporal Way
%I The University of Manchester, Department of Computer Science
%K AA08 elevator
%X no charge
A formal specification of a multiple lift system is constructed.
The example illustrates and justifies one of many possible
system specification styles based on temporal techniques.
%A Ru-qian Lu
%T Expert Union: United Service of Distributed Expert Systems
%R 85-3
%I University of Minnesota-Duluth
%C Duluth, Minnesota
%D June, 1985
%K AI01 H03
%X A scheme for connecting expert systems in a network called an {\nit
expert union} is described. Consultation scheduling algorithms used to
select the appropriate expert(s) to solve problems are proposed, as
are strategies for resolving contradictions.
%R No 27
%T The Complexity of a Translation
of L-calculus to
Categorical Combinators
%A R D Lins
%D April 1985
%I University of Kent at Canterbury
%A Sheldon Klein
%T The Invention of Computationally Plausible Knowledge Systems
in the Upper Paleolithic
%D December 1985
%R TR 628
%I Computer Sciences Department, University of Wisconsin
%C Madison, WI
%K AI08
%X Abstract: The problem of computing human behavior by rules can become
intractable with large scale knowledge systems if the human brain, like a
computer, is a finite state automaton. The problem of making such
computations at a pace fast enough for ordinary social interaction can be
solved if appropriate constraints apply to the structure of those rules.
There is evidence that systems of such constraints were invented in the
Upper Paleolithic, and were of sufficient power to guarantee that the time
necessary for computation of behavior would increase only linearly with
increases in the size and heterogeneity of world knowledge systems.
Fundamentally, there was just one type of computational invention, capable
of unifying the full range of human sensory domains, and consisting of an
analogical reasoning method in combination with a global classification
scheme. The invention may have been responsible for the elaboration of
language and culture structures in a process of co-evolution. The encoding
of the analogical mechanism in iconic visual imagery and myth structures
may have given rise to the phenomenon of Shamanism. The theory is testable,
and one of its implications is that the structuralism of Levi-Strauss has
an empirical foundation.
%A G.T. NGUYEN
%A J. OLIVARES
%D JAN 1985
%R IMAG RR TIGRE 26
%C Grenoble, France
%T SYCSLOG - systeme logique d'integrite semantique
%A M. ADIBA
%A Q.N. BUI
%A J. PALAZZO DE OLIVEIRA
%D JAN 1985
%R IMAG RR TIGRE 23
%C Grenoble, France
%T Notion de temps dans les bases de donnees generalisees
%A A. DANDACHE
%D APR 1985
%R IMAG RR 516
%C Grenoble, France
%T Etude de structures regulieres PLA - ROM dans la partie controle de
microprocesseurs
%A S. GRAF
%A J. SIFAKIS
%D FEB 1985
%R IMAG RR 526
%C Grenoble, France
%T From synchronization tree logic to acceptance model logic
%A H. BALACHEFF
%D MAY 1985
%R IMAG RR 528
%C Grenoble, France
%T Processus de preuves et situations de validation
%A Michel COSNARD
%A Yves ROBERT
%A Denis TRYSTRAM
%D JUL 1985
%R IMAG RR 552
%C Grenoble, France
%T Resolution parallele de systemes lineaires denses par diagonalisation
%K AI11
%A Yves ROBERT
%A Denis TRYSTRAM
%D JUL 1985
%R IMAG RR 553
%C Grenoble, France
%T Un reseau systolique orthogonal pour le probleme du chemin algebrique
%A J.R. BARRA
%A M. BECKER
%A D. BELAID
%A F. CHATELIN
%A C. MAZEL
%D JUN 1985
%R IMAG RR 542
%C Grenoble, France
%T Realisation d'un logiciel d'analyses factorielles avec systeme
d'assistance intelligente a l'utilisateur
%A Jean FONLUPT
%A Denis NADDEF
%D SEP 1985
%R IMAG RR 557
%C Grenoble, France
%T The traveling salesman problem in graphs with some excluded minors
%A Yves DEMAZEAU
%D APR 1985
%R IMAG RR 502
%C Grenoble, France
%T La programmation des jeux: programmation classique et intelligence
artificielle
%K AA17
%A Hicham AL NACHAWATI
%D 1985
%I These Universite, GRENOBLE
%K SEGMENTATION
%K PROCESSUS ARBORESCENT
%K ANALYSE VARIANCE
%K CLASSIFICATION AUTOMATIQUE
%T Processus de classification sequentiels non arborescents pour l'aide au
diagnostic
%W IMAG Mediatheque
%A Xin an PAN
%D 1985
%I These Universite, GRENOBLE
%K MINIMA
%K ALGORITHME ITERATIF
%K RESEAU AUTOMATE
%K AUTOMATE
%K RECONNAISSANCE CARACTERE
%K DISTANCE
%T Experimentation d'automates a seuil pour la reconnaissance de caracteres
%W IMAG Mediatheque
%A Laurent BERGHER
%D 1985
%I These doct. ing., GRENOBLE
%K ANALYSE
%K POTENTIEL
%K VLSI
%K MICROPROCESSEUR
%K ANALYSE IMAGE
%K TEST
%K CAPTEUR IMAGE
%T Analyse de defaillances de circuits VLSI par microscopie electronique a
balayage
%W IMAG Mediatheque
%A Philippe VIGNARD
%D 1985
%I These doct. ing., GRENOBLE
%K REPRESENTATION CONNAISSANCE
%K EXPLOITATION
%K FILTRAGE
%K DISTRIBUTION
%K SEMANTIQUE
%K ANALOGIE
%K TYPOLOGIE
%T Un mecanisme d'exploitation a base de filtrage flou pour une representation
des connaissances centree objets
%W IMAG Mediatheque
%A Prabhaker Mateti
%T Correctness Proof of an Indenting Program
%R Technical Report 80/2
%I Department of Computer Science, University of Melbourne
%D September 1980
%P 59
%K verification, correctness proof, pretty printing, pascal
%O also in Software - Practice and Experience
%K AA08
%X
The correctness of an indenting program for Pascal is proven at an
intermediate level of rigour. The specifications of the program are given
in the companion paper [TR 80/1]. The program is approximately 330 lines
long and consists of four modules: io, lex, stack, and indent. We prove
first that the individual procedures contained in these modules meet their
specifications as given by the entry and exit assertions. A global proof
of the main routine then establishes that the interaction between modules
is such that the main routine meets the specification of the entire program.
We argue that correctness proofs at the level of rigour used here serve
very well to transfer one's understanding of a program to others. We believe
that proofs at this level should become commonplace before more formal
proofs can take over to reduce traditional testing to an inconsequential
place.
%A Joxan Jaffa
%T Presburger Arithmetic with Array Segments
%R Technical Report 81/1
%I Department of Computer Science, University of Melbourne
%D January 1981
%P 8
%K verification, assertion language, decision procedure
AA08
%A John W. Lloyd
%T An Introduction to Deductive Database Systems
%R Technical Report 81/3
%I Department of Computer Science, University of Melbourne
%D April 1981 (revised April 1983)
%P 24
%K T02 AA14 AA09
%O also in Australian Computer Journal, vol.15, 1983
%X
This paper gives a tutorial introduction to deductive database systems.
Such systems have developed largely from the combined application of the
ideas of logic programming and relational databases. The elegant theoretical
framework for deductive database systems is provided by first order logic.
Logic is used as a uniform language for data, programs, queries, views
and integrity constraints. It is stressed that it is possible to build
practical and efficient database systems using these ideas.
%A John W. Lloyd
%T Implementing Clause Indexing for Deductive Database Systems
%R Technical Report 81/4
%I Department of Computer Science, University of Melbourne
%D October 1981
%P 22
%K AA14 AA09
%X
The paper presents a file design for handling partial-match
queries which has wide application to knowledge-based artificial
intelligence systems and relational database systems. The
advantages of the design are simplicity of implementation, the
ability to cope with dynamic files and the ability to optimize
performance with respect to the average number of disk access
required to answer a query.
%A Joxan Jaffar
%A Jean-Louis Lassez
%T A Decision Procedure for Theorems about Multisets
%R Technical Report 81/7
%I Department of Computer Science, University of Melbourne
%D July 1981
%P 37
%K automatic theorem proving, verification, domain dependent reasoning
AI11 AA13
%A Lee Naish
%T An Introduction to MU-Prolog
%R Technical Report 82/2
%I Department of Computer Science, University of Melbourne
%D March 1982 (Revised July 1983)
%P 16
%K T02 muprolog AI10 control negation
%X
As a logic programming language, PROLOG is deficient in two areas:
negation and control facilities. Unsoundly implemented negation
affects the correctness of programs and poor control facilities
affect the termination and efficiency. These problems are illustrated
by examples.
MU-PROLOG is then introduced. It implements negation soundly and
has more control facilities. Control information can be added
automatically. This can be used to avoid infinite loops and find
efficient algorithms from simple logic. MU-PROLOG is closer to the
ideal of logic programming.
%A Joseph Stoegerer
%T Specification Languages - A Survey
%R Technical Report 82/5
%I Department of Computer Science, University of Melbourne
%D June 1982
%P 62
%K software specification, requirements languages, software development tools,
integrated software development support systems, non-procedural languages,
automated analysis tools AA08
%A Joxan Jaffar
%A Jean-Louis Lassez
%A John W. Lloyd
%T Completeness of the Negation-as-failure Rule
%R Technical Report 83/1
%I Department of Computer Science, University of Melbourne
%D January 1983
%P 20
%O also in Proceedings of the Eigth International Joint Conference
on Artificial Intelligence, Karlsruhe, Germany, 1983
%K AI10 finite failure, completion of a program
%X
Let P be a Horn clause logic program and comp(P) be its completion in the
sense of Clark. Clark gave a justification for the negation as failure rule
by showing that if a ground atom A is in the finite failure set of P, then
~A is a logical consequence of comp(P), that is, the negation as failure
rule is sound. We prove here that the converse also holds, that is, the
negation as failure rule is complete.
%A Jean-Louis Lassez
%A Michael J. Maher
%T Closures and Fairness in the Semantics of Logic Programming
%R Technical Report 83/3
%I Department of Computer Science, University of Melbourne
%D March 1983
%P 17
%K semantics, chaotic iteration, SLD resolution, finite failure, T92
%O also in Theoretical Computer Science, vol.29, 1984
%A Jean-Louis Lassez
%A Michael J. Maher
%T Optimal Fixedpoints of Logic Programming
%R Technical Report 83/4
%I Department of Computer Science, University of Melbourne
%D March 1983
%P 15
%K theory, semantics AA08 AI10
%O also in Theoretical Computer Science, vol.30, 1985
%X
From a declarative programming point of view, Manna and Shamir's
optimal fixedpoint semantics is more appealing than the least
fixedpoint semantics. However in standard formalisms of recursive
programming the optimal fixedpoint is not computable while the least
fixedpoint is. In the context of logic programming we show that the
optimal fixedpoint is equal to the least fixedpoint and is computable.
Furthermore the optimal fixedpoint semantics is consistent with Van Emden
and Kowalski's semantics of logic programs.
%A Lee Naish
%T Automatic Generation of Control for Logic Programming
%R Technical Report 83/6
%I Department of Computer Science, University of Melbourne
%D July 1983 (Revised September 1984)
%P 24
%K T02 O02 muprolog, control facilities, coroutines, automatic programming
%O also as Automating Control for Logic Programs'' in Journal of Logic Progrmm
ing, vol.5, 1985
%X
A model for the coroutined execution of PROLOG programs is presented
and two control primitives are described. Heuristics for the control
of database and recursive procedures are given, which lead to algorithms
for generating control information. These algorithms can be incorporated
into a pre-processor for logic programs. It is argued that automatic
generation should be an important consideration when designing control
primitives and is a significant step towards simplifying the task of
programming.
%A Lee Naish
%A James A. Thom
%T The MU-Prolog Deductive Database
%R Technical Report 83/10
%I Department of Computer Science, University of Melbourne
%D November 1983
%P 16
%K muprolog, partial match retrieval, unix T02 AA09 AA14
%X
This paper describes the implementation and an application of a
deductive database being developed at the University of Melbourne.
The system is implemented by adding a partial match retrieval system
to the MU-PROLOG interpreter.
%A David A. Wolfram
%A Jean-Louis Lassez
%A Michael J. Maher
%T A Unified Treament of Resolution Strategies for Logic Programs
%R Technical Report 83/12
%I Department of Computer Science, University of Melbourne
%D December 1983
%P 25
%K soundness, completeness, unification, negation as failure AI10
%O also in Proceedings of the Second International Logic Programming Conference,
Uppsala, Sweden, 1984
%A Lee Naish
%T Heterogeneous SLD Resolution
%R Technical Report 84/1
%I Department of Computer Science, University of Melbourne
%D January 1984
%P 11
%K T02 AI10 resolution, control facilities, intelligent backtracking
%O also in Journal of Logic Programming, vol.4, 1984
%X Due to a significant oversight in the definition of computation rules,
the current theory of SLD resolution is not general enough
to model the behaviour of some PROLOG implementations with advanced
control facilities.
In this paper, Heterogeneous SLD resolution is defined.
It is an extension of SLD resolution which increases the \*(lqdon't care\*(rq
non-determinism of computation
rules and can decrease the size of the search space.
Soundness and completeness, for success and finite failure, are
proved using similar results from SLD resolution.
Though Heterogeneous SLD resolution was originally devised to model current
systems, it can be exploited more fully than it is now.
As an example, an interesting new computation rule is described. It can be seen
as a simple form of intelligent backtracking with few overheads.
%A Koenraad Lecot
%A Isaac Balbin
%T Prolog & Logic Programming Bibliography
%R Technical Report 84/3
%I Department of Computer Science, University of Melbourne
%D May 1984
%P 55
%K classified bibliography AT21 T02 AI10
%O a considerably expanded version appeared as Logic Programming:
A Classified Bibliography'', Wildgrass Books, 1985
%A Lee Naish
%T All Solutions Predicates in Prolog
%R Technical Report 84/4
%I Department of Computer Science, University of Melbourne
%D June 1984
%P 15
%K logic programming, negation, coroutines T02 AI10
%O also in Proceedings of IEEE Symposium on Logic Programming, Boston, 1985
%A Michael J. Maher
%A Jean-Louis Lassez
%A Kmball G. Marriott
%T Antiunification
%R Technical Report 84/5
%I Department of Computer Science, University of Melbourne
%D to appear
%P ?
%K AI10 unification
%A Lee Naish
%A Jean-Louis Lassez
%T Most Specific Logic Programs
%R Technical Report 84/6
%I Department of Computer Science, University of Melbourne
%D to appear
%P ?
%K AI10
%A Rodney W. Topor
%A Teresa Keddis
%A Derek W. Wright
%T Deductive Database Tools
%R Technical Report 84/7
%I Department of Computer Science, University of Melbourne
%D June 1984 (revised August 1985)
%P 27
%K database management, deductive database, query language,
integrity constraint, logic programming, T02 AA14 AA09 T02
AI10
%O also in Australian Computer Journal, vol.?, 1985
%X
A deductive database is a database in which data can be represented
both explicitly by facts and implicitly by general rules. The use of
typed first order logic as a definition and manipulation language for
such deductive databases is advocated and illustrated by examples.
Such a language has a well-understood theory and provides a uniform
notation for data, queries, integrity constraints, views and programs.
We present algorithms for implementing domains, for using atoms with
named attributes, for evaluating queries, and for checking static and
transition integrity constraints. The implementation is by translation
into Prolog and can be performed using a standard Prolog system. The
paper assumes some familiarity with relational databases, logic and Prolog.
%R CSL T.R. 85-281
%T Prolog Memory-Referencing Behavior
%A Evan Tick
%D September 1985
%K T02
%I Computer Systems Laboratory, Stanford University
%X This report describes Prolog data and instruction memory-referenci
ng
characteristics. Prolog exhibits unconventional referencing behavior of
backtracking; the saving and subsequent restoration of a program state.
Backtracking introduces memory bandwidth requirements above those of procedural
languages. The significance of this and other characteristics was measured by
emulating a Prolog architecture running three benchmark programs and simulating
various memory models. The results indicate that so-called determinate
programs require substantial memory bandwidth because of a limited form of
backtracking (shallow). However, this referencing behavior exhibits spatial
locality enabling small memory buffers to reduce the bandwidth requirement. A
modification to the Prolog architecture having the advantage of further
increasing locality is described.