An Evolutionary Approach to Synthetic Biology,
- Thomas S. Ray
Our concepts of biology, evolution and complexity are constrained by having observed
only a single instance of life, life on Earth. A truly comparative biology is needed
to extend these concepts. Because we can not observe life on other planets, we are left
with the alternative of creating artificial life forms on Earth. I will discuss the approach
of inoculating evolution by natural selection into the medium of the digital computer.
This is not a physical/chemical medium, it is a logical/informational medium. Thus
these new instances of evolution are not subject to the same physical laws as organic
evolution (e.g., the laws of thermodynamics), and therefore exist...
Mutual Belief Revision (Preliminary Report)
- Wakamiya Morinosato Atsugi-shi
A semantical theory of belief revision in synchronous
multi-agent systems is presented.
The theory assumes that the world is static,
and that the belief revision methods used
by the agents are common knowledge. It is
shown that the theory has as a special case
the revision of knowledge in a broadcast variant
of Fagin and Vardi's communicating scientists
model, in which knowledge is defined
in terms of an equivalence relation on runs
in a distributed system. Next, the theory
is applied to give a semantic reconstruction
of a default logic theory of speech acts proposed
by Perrault. This reconstruction characterizes
the way the speech act transforms
an only knowing representation of the agent's
belief states. The...
An Automata-Theoretic Approach to Linear Temporal Logic
- Moshe Y. Vardi
. The automata-theoretic approach to linear temporal logic uses the
theory of automata as a unifying paradigm for program specification, verification,
and synthesis. Both programs and specifications are in essence descriptions of
computations. These computations can be viewed as words over some alphabet.
Thus,programs and specificationscan be viewed as descriptions of languagesover
some alphabet. The automata-theoretic perspective considers the relationships
betweenprograms and their specifications as relationships between languages. By
translating programs and specifications to automata, questions about programs and
their specifications canbe reduced to questions about automata. More specifically,
questions such as satisfiability of specifications and correctness of programs with
respect to their specifications can be reduced to questions such...
Feedback Control of Petri Nets Based on Place Invariants
- Katerina Yamalidou,John Moody,Michael Lemmon,Panos Antsaklis
This report describes a method for constructing a Petri net controller for a discrete
event system modeled by a Petri net. The controller consists only of places and arcs
and is computed based on the concept of place invariants of the net. The size of the
controller is proportional to the number of the constraints which must be satisfied. This
method can accommodate constraints written as logic formulas, algebraic inequalities
Keywords: Discrete Event Systems, Petri Nets
Petri nets are a very appropriate tool for the study of discrete-event dynamical systems
because of their power and flexibility. In the past they have been used extensively to...
Fixed-Choice and Independent-Choice Logics
- Andreas Blass,Yuri Gurevich
We study extensions of first-order logic with the choice construct (choose x : '(x)).
We prove some results about Hilbert's " operator, but in the main part of the paper
we consider the case when all choices are independent.
Partially supported by NSF grant DMS 95-05118
Partially supported by NSF grant CCR 95-04375
This investigation was motivated by the choice construct in ASM programs, that is the
programs of abstract state machines [Gurevich 1995]. The ASM choice terms have the form
(choose x : '(x))
where '(x) is a formula (that is a Boolean-valued term
). Intuitively (choose x : '(x)) is an
element of the set fx :...
A System for Computing Constrained Default Logic Extensions
- G. Antoniou,A. P. Courtney,J. Ernst
The aim of this paper is to describe the algorithmic foundations of the
part of the program Exten responsible for the computation of extensions
in Constrained Default Logic. Exten is a system that computes extensions
for various default logics.
The efficiency of the system is increased by pruning techniques for the
search tree. We motivate and present these techniques, and demonstrate
that they can cut down the size of the search tree significantly. Quite
importantly, they complement well the recently developed stratification
method. This technique has to be modified to work properly with Constrained
Default Logic, and we show how this can be done.
Exten supports experimentation with default logic,...
The Integration of Rule and Example Sets
- Christian Posthoff,Michael Schlosser,Jens Zeidler
The integration of knowledge bases is a well-known and important problem, before
all when the knowledge has different representations and/or different forms. Very characteristic
examples are, for instance, rule sets given by an expert, example sets (possibly
noisy), rule sets given by more than one expert and so on. The present paper will show
a methodology that allows a complete solution of the integration problem using logic
equations and enables the knowledge engineer to gain deep and complete insights in the
In  and many other publications, the integration of different knowledge sources is considered.
This is necessary, for example, if the knowledge is acquired...
Some issues about Petri net application to manufacturing and process supervisory control
- Robert Valette
After some general considerations concerning modeling issues, the paper concentrates on the fact that places are generally interpreted as logical conditions. There are various kind of logical propositions, some (the resources) are consumed when they are used in the same way tokens are removed from places when transitions are fired. Linear logic has pointed out the fact that resources had to be handled with a restricted set of logical rules and that they could not easily be handled concurrently with classical logic propositions. This can be exploited for developing modeling methods based on Petri nets. Then two cases of combining...
Logic-Based Switching Control of a Nonholonomic System With Parametric Modeling Uncertainty
- Jo~ao P. Hespanha,Daniel Liberzon,A. Stephen Morse
This paper is concerned with control of nonholonomic systems in the presence of parametric
modeling uncertainties. The specific problem considered is that of parking a wheeled mobile
robot of unicycle type with unknown parameters, whose kinematics can be described by the
nonholonomic integrator after an appropriate state and control coordinate transformation. We
employ the techniques of supervisory control to design a hybrid feedback control law that solves
this problem. The proposed procedure seems to have several advantages over conventional
Keywords: Nonholonomic system; modeling uncertainty; hybrid feedback control; estimatorbased
Control systems with nonholonomic motion constraints have been extensively studied in the recent
years, particularly in the context...
Computational Representations of Herbrand Models Using Grammars
- Robert Matzinger
. Finding computationally valuable representations of models of predicate logic
formulas is an important subtask in many fields related to automated theorem proving,
e.g. automated model building or semantic resolution. In this article we investigate the
use of context-free languages for representing single Herbrand models, which appear to be
a natural extension of "linear atomic representations" already known from the literature.
We focus on their expressive power (which we find out to be exactly the finite models)
and on algorithmic issues like clause evaluation and equivalence test (which we solve by
using a resolution theorem prover), thus proving our approach to be an interesting base for
A Mechanized Theory of the
- T. F. Melham
: The ß-calculus is a process algebra for modelling concurrent systems in which the
pattern of communication between processes may change over time. This paper describes the
results of preliminary work on a definitional formal theory of the ß-calculus in higher order logic
using the HOL theorem prover. The ultimate goal of this work is to provide practical mechanized
support for reasoning with the ß-calculus about applications.
The ß-calculus [17, 18] is a process algebra proposed by Milner, Parrow and Walker for modelling
concurrent systems in which the pattern of interconnection between processes may change over
time. This paper describes work on a mechanized formal theory of...
Strong Modes can Change the World!
- Fergus Henderson
We investigate compile-time garbage collection, structure reuse, and destructive assignment
for logic programming languages, using an expressive strong mode system. By
attaching groundness and uniqueness information to each node of a variable's type tree,
the mode system forms the basis for carrying out these optimizations. Our system allows
polymorphic mode definitions to achieve a high level of expressiveness. We implement a
simple preprocessor that does structure re-use optimization for Prolog programs annotated
with mode declarations. Finally, we show how our mode system can be used to
provide declarative I/O for logical programming languages.
I'd like to thank Lee Naish (my supervisor), Harald Søndergaard, Jeff Schultz, Alistair
Moffat, Will Winsborough,...
Safe, Untrusted Agents using Proof-Carrying Code
- George C. Necula,Peter Lee
. Proof-Carrying Code (PCC) enables a computer system to
determine, automatically and with certainty, that program code provided
by another system is safe to install and execute without requiring
interpretation or run-time checking. PCC has applications in any computing
system in which the safe, efficient, and dynamic installation of
code is needed. The key idea of Proof-Carrying is to attach to the code
an easily-checkable proof that its execution does not violate the safety
policy of the receiving system. This paper describes the design and a typical
implementation of Proof-Carrying Code, where the language used for
specifying the safety properties is first-order predicate logic. Examples of
safety properties that are...
Relational Computations in Medical KBS CLINAID: the means for integrating Interval, Symbolic logic and Neural network techniques
- Ladislav J. Kohout,Isabel Stabile
Natural Ideal Operators in Inductive Logic Programming
- Fabien Torre
. We present in this paper the original notion of natural relation,
a quasi order that extends the idea of generality order: it allows the
sound and dynamic pruning of hypotheses that do not satisfy a property,
be it completeness or correctness with respect to the training examples,
or hypothesis language restriction.
Natural relations for conjunctions of such properties are characterized.
Learning operators that satisfy these complex natural relations allow
pruning with respect to this set of properties to take place before inappropriate
hypotheses are generated.
Once the natural relation is defined that optimally prunes the search
space with respect to a set of properties, we discuss the existence of
Reconciling the Event Calculus with the Situation Calculus
- Robert Kowalski,Fariba Sadri
In this paper, to compare the situation calculus and event calculus we formulate both as
logic programs and prove properties of these by reasoning with their completions
augmented with induction. We thus show that the situation calculus and event calculus
imply one another. Whereas our derivation of the event calculus from the situation
calculus requires the use of induction, our derivation of the situation calculus from the
event calculus does not. We also show that in certain concrete applications, such as the
missing car example, conclusions that seem to require the use of induction in the
situation calculus can be derived without induction in the event calculus....
Real-Time Logics: Fictitious Clock as an Abstraction of Dense Time
- Pierre-yves Schobbens,B Namur
In this paper we study two possible semantics for the logic MTL (Metric Temporal Logic). In the first semantics, called dense time semantics, time is modeled by the positive real numbers. In the second one, called fictitious clock semantics, real-time information is delivered by a global fictitious clock. We show that the fictitious clock semantics can be viewed as an abstraction of the dense time semantics. This abstraction relation is formalized by a parametric conservative connection, a kind of Galois connection, a favorite structure of abstract interpretation [5, 6]. This formalization can be used to partially decide undecidable problems in...
Sorted HiLog: Sorts in Higher-Order Logic Data Languages
- Weidong Chen,Michael Kifer
HiLog enhances the modeling capabilities of deductive databases and logic programming with
higher-order and meta-data constructs, complex objects, and schema browsing. Its distinctive feature,
a higher-order syntax with a first-order semantics, allows for efficient implementation with speeds
comparable to Prolog. In fact, HiLog implementation in XSB [30, 26] together with tabulated query
evaluation offers impressive performance with negligible penalty for higher-order syntax, thereby bringing
the modeling capabilities of HiLog to practical realization.
The lack of sorts in HiLog, however, is somewhat of a problem in database applications, which led
to a number of HiLog dialects such as DataHiLog . This paper develops a comprehensive theory
of sorts for...
On the Role of Semantic Approximations in Validation and Diagnosis of Constraint Logic Programs
This paper presents some on-going work in the ESPRIT project DiSCiPl. The project aims at
devising advanced tools for debugging of constraint logic programs.
A central problem in program development is obtaining a program which satisfies the user's
expectations. When considering a given program, a natural question is then whether or not it
fulfils expectations of some kind (requirements). To be able to formulate this question, some
formal or informal way of specifying such requirements is needed. That is, a (formal or informal)
program semantics is needed, in which one can express what the program computes and what...
The Foundations of Psychology - A logico-computational inquiry into the concept of mind
- Jon Doyle,For Gerald Jay Sussman
We compare certain trains of thought in philosophy of mind and artificial intelligence
which lead to a remarkable convergence of ideas. Demands from philosophy that psychological
theories have predictive power join with demands from artificial intelligence
that machines adaptively maintain their own mental state to suggest a conception of
minds as narrowly realized psychological theories. We use this conclusion both to clarify
the domains of study and scientific aims of psychology and artificial intelligence,
and to suggest some methodological principles for constructing intelligent machines.
This paper is revised from one dated February 18, 1982 and written while the author was with Carnegie
Mellon University. Copyright c fl 1981,1982,1990...