110721.

Call-By-Value Games
- Samson Abramsky,Guy Mccusker
A general construction of models of call-by-value from models of callby
-name computation is described. The construction relies on the fact
that common denotational models of programming languages are also
models of linear logic. When applied to categories of games, it yields
fully abstract models of the call-by-value functional language PCFv and
of a language with imperative features similar to the references of Standard
ML.

110722.

A Genetic Programming Approach to Logic Function Synthesis by means of Multiplexers
- Arturo Hern'andez Aguirre,Carlos A. Coello Coello,Bill P. Buckles
This paper presents an approach based on the use
of genetic programming to synthesize logic functions.
The proposed approach uses the 1-control line multiplexer
as the only design unit, defining any logic function
(defined by a truth table) through the replication of
this single unit. Our fitness function first explores the
search space trying to find a feasible design and then
concentrates in the minimization of such (fully feasible)
circuit. The proposed approach is illustrated using
several sample Boolean functions.

110723.

Multi-Modal Control of Systems with Constraints
- T. John Koo,Shankar Sastry
In multi-modal control paradigm, a set of controllers
of satisfactory performance have already been designed
and must be used. Each controller may be designed
for a di#erent set of outputs in order to meet the given
performance objectives and system constraints. When
such a collection of control modes is available, an important
problem is to be able to accomplish a variety
of high level tasks by appropriately switching between
the low-level control modes. In this paper, we
propose a framework for determining the sequence of
control modes that will satisfy reachability tasks. Our
framework exploits the structure of output tracking
controllers in order to extract a finite graph where the
mode switching problem...

110724.

Doing Two-Level Logic Minimization
- Olivier Coudert
Two-level logic minimization consists in finding a minimal
cost sum-of-products, i.e, disjunctive normal form, of a given
Boolean function. This paper presents a new algorithm
to solve this problem, and gives experimental evidences
showing that it outperforms the leading minimizers of several
orders of magnitude. We suspect that it may be possible to
explain this improvement in performance theoretically, and
hope that our empirical results will stimulate research along
these line.

110725.

Analysing resource use in the A-calculus by type inference
- S. A. Courtenage,C. D. Clack
If we view functions as processes, then their resources
are their arguments, supplied through application,
and used by the function to produce a
result. In this paper, we define resource use for
functions, based on the syntactic notion of needed
redexes from [BKKS86]. We introduce a variant
of neededhess, tail-neededness, and define packets
of needed descendants of redexes in order to mea-
sure the degree of neededhess. These results are
generalised to produce a semantic characterisation
of the resource use properties of functions, using
a term-model. By means of the Curry-Howard
isomorphism, we apply these ideas to proof trees
of propositions in Intuitionistic Logic to demonstrate
that propositions, i.e. types, can be used
to express...

110726.

PVS: Combining Specification, Proof Checking,
- S. Owre,S. Rajan,J. M. Rushby,N. Shankar,M. Srivas
typed higher-order
logic, but the type system has been augmented with subtypes and dependent
types. Though typechecking is undecidable for the PVS type system, the PVS
typechecker automatically checks for simple type correctness and generates proof
obligations corresponding to predicate subtypes. These proof obligations can be
discharged through the use of the PVS proof checker. PVS also has parametric
theories so that it is possible to capture, say, the notion of sorting with respect to
arbitrary sizes, types, and ordering relations. By exploiting subtyping, dependent
typing, and parametric theories, researchers at NASA Langley Research Center
and SRI have developed a very general bit-vector library. Paul Miner at NASA
The development...

110727.

Actors, Actions, and Initiative in Nor-
- R. J. Wieringa,J. -j. Ch. Meyer
The logic of norms, called deontic logic, has been used to specify normative
constraints for information systems. For example, one can specify in
deontic logic the constraints that a book borrowed from a library should be
returned within three weeks, and that if it is not returned, the library should
send a reminder. Thus, the notion of obligation to perform an action arises
naturally in system specification.

110728.

A New Class of Decidable Hybrid Systems
- Gerardo Laerriere,Sergio Yovine
One of the most important analysis problems of hybrid systems
is the reachability problem. State of the art computational tools perform
reachability computation for timed automata, multirate automata,
and rectangular automata. In this paper, we extend the decidability frontier
for classes of linear hybrid systems, which are introduced as hybrid
systems with linear vector fields in each discrete location. This result is
achieved by showing that any such hybrid system admits a finite bisimulation,
and by providing an algorithm that computes it using decision
methods from mathematical logic.

110729.

A Structured Logic Programming Approach
- Enrico Denti,Antonio Natali,Andrea Omicini,Francesco Zanichelli
This paper discusses an approach to robot programming based on Prolog, properly extended
with control capabilities toward program structuring (contextual programming) and
(pseudo)concurrence (communicating Prolog units). This Prolog-based programming system supports
the definition, both static and dynamic, of extendible software components, promoting at the same time
incremental design and development of software systems. Moreover, it suggests an approach to
integration between object-oriented, knowledge-based and logic programming, introducing powerful
concepts such as backtrackable objects and dynamic object configuration. Finally, the system, which is
embedded in a simple architecture constituted by several Prolog machines sharing a data-base acting as
an evolving world, provides an effective way to reduce the gap...

110730.

A Mini-course on Temporal Databases
- David Toman
Temporal Databases
9 Basic Building Blocks
10 The Snapshot Model
11 Snapshots: Example
12 Histories
13 The Timestamp Model
14 Timestamp Example
15 Query Languages
16 First-order Temporal Connectives
17 Examples of Temporal Connectives
18 Propositional Temporal Logic
19 First-order Temporal Logic: syntax
20 FOTL: semantics
21 Examples
22 Temporal Relational Calculus: syntax
23 Temporal RC: Semantics
24 Examples
25 Examples (cont.)
26 Expressive Power
27 Expressive Power (cont.)
28 How do we prove it?
29 Scope of Temporal Variables
30 Ehrenfeucht-Frassb Games
31 Ehrenfeucht-Frassb Games (cont.)
32 Ehrenfeucht-Frassb Games (cont.)
33 Ehrenfeucht-Frassb Games (cont.)
34 EF Games and Temporal Logic
35 Compatibility of Variables in FOTL
36 Databases not distinguishable by FOTL
37 Communication Complexity
38 Consequences for Temporal Queries
39 Temporal Relational Algebra
40 TRA: example
41 Temporal Logic TL(FO)
42 Plan
43...

110731.

Using Logic for Querying XML Data
- Nick Bassiliades,Ioannis Vlahavas,Dimitrios Sampson
In this chapter, we propose the use of first-order logic, in the form of deductive database rules, as a
query language for XML data and we present X-DEVICE, an extension of the deductive object-oriented
database system DEVICE for storing and querying XML data. XML documents are stored into the
OODB by automatically mapping the DTD to an object schema. XML elements are treated either as
classes or attributes based on their complexity, without loosing the relative order of elements in the
original document. Furthermore, this chapter describes the extension of the system's deductive rule
query language with second-order variables, general path and ordering expressions, for querying...

110732.

An Algebraic Perspective of Constraint Logic Programming
- Ra Di Pierro
We develop a denotational, fully abstract semantics for constraint logic programming
(clp) with respect to successful and failed observables. The denotational approach
turns out very useful for the definition of new operators on the language as the counterpart
of some abstract operations on the denotational domain. In particular, by
defining our domain as a cylindric Heyting algebra, we can exploit, to this aim, operations
of both cylindric algebras (such as cylindrification), and Heyting algebras (such
as implication and negation). The former allows us to generalize the clp language by
introducing an explicit hiding operator; the latter allows us to define a notion of negation
which extends the classical...

110733.

Multiple Model Adaptive Control, Part 2: Switching
- Jogo Hespanha,Daniel Liberzonll,A. Stephen Morse,Brian D. O. Anderson,Thomas S. Brinsmead,Franky De Bruyne
This paper addresses the problem of controlling a continuous-time linear system with large
modeling errors. We employ an adaptive control algorithm consisting of a family of linear candidate
controllers supervised by a high-level switching logic. Methods for constructing such controller
families have been discussed in the recent paper by the authors. The present paper concentrates
on the switching task in a multiple model context. We describe and compare two different
switching logics, and in each case study the behavior of the resulting closed-loop hybrid system.

110734.

Linear Deductive Planning
- Gerd Groe,Th Darmstadt,Steffen Holldobler Tu Dresden
Recently, three approaches to deductive planning were developed, which solve the technical frame problem without the need to state frame axioms explicitly. These approaches are based on the linear connection method, an equational Horn logic, and linear logic. At first glance these approaches seem to be very different. In the linear connection method a syntactical condition --- each literal is connected at most once --- is imposed on proofs. In the equational logic approach situations and plans are represented as terms and SLDE-resolution is applied as an inference rule. The linear logic approach is a Gentzen style proof system without...

110735.

Coalgebras and Modal Logic
- Colebrs Nd Modl Loi,Alexander Kurz
and Concrete Categories. John
Wiley & Sons, 1990.

110736.

On the Benefits of Rewrite Logic as a Semantics for Algebraic Petri Nets in Computing Siphons and Traps
- Nasreddine Aoumeur,I Gunter Saake
A lot of research is being done to directly apply to high level nets structural techniques
similar to those existing for place transition nets. In particular, the question of computing
siphons for high level nets is of intrest since the well known results about relations between
liveness of a net and control of its siphons. In this paper, we show how one can derive an
efficient computing of siphons containing a given place from an appropriate interpretation of
algebraic Petri nets in rewrite logic as a true concurrent semantics. Within this method, the
verification procedure of symbolic siphons is reduced to two easy-understandable inference
rewrite rules instead...

110737.

A Correct, Precise and Efficient Integration of Set-Sharing, Freeness and Linearity for the Analysis of Finite and Rational Tree Languages
- Patricia M. Hill,Enea Zaffanella,Roberto Bagnara
It is well-known that freehess and linearity information positively interact
with aliasing information, therefore allowing both the precision and
the efficiency of the sharing analysis of logic programs to be improved. In
this paper we present a novel combination of set-sharing with freehess
and linearity information, which is characterized by an improved abstract
unification operator. We provide a new abstraction function and prove
the correctness of the analysis for both the finite tree and the rational tree
cases. Moreover, we show that the same notion of redundant information
as identified in [3] also applies to this abstract domain combination: this
allows for the implementation of an abstract unification operator...

110738.

Mirror Mirror In My Hand: a duality between specifications and models of process behaviour
- J. L. Fiadeiro,J. F. Costa
Since Pnueli's seminal paper in 1977, Temporal Logic has been
used as a formalism for specifying and verifying the correctness of reactive
systems. In this paper, we show that, besides its expressive power, Temporal
Logic enjoys a very strong structural property: it is categorical on processes.

110739.

Unknown
- Riddle Of Induction
ts the fact that depending on the space of alternative hypotheses,
means-ends analysis may select a different hypothesis on the same evidence: "all emeralds are
green" in my Goodmanian Riddle, and "all emeralds are grue" in his. To my mind, his example
proves that means-ends epistemology is not biased towards green-blue rather than grue-bleen. (A
formal demonstration that means-ends analysis is language-invariant for all inductive problems
appears in my paper "The Logic of Reliable and Efficient Inquiry" [Schulte 99].) Chart,
however, concludes that "means-ends epistemology does not resolve Goodman's problem". That
depends on what one takes Goodman's problem to be. If the problem is to find the...

110740.

Tuning Of A Neuro-Fuzzy Controller By Genetic Algorithms With An Application To A Coupled-Tank Liquid-Level Control System
- Teo Lian Seng,Marzuki Khalid,Rubiyah Yusof,Universiti Teknologi Malaysia
Fuzzy logic, neural networks and genetic algorithms are three popular artificial
intelligence techniques that are widely used in many applications. Due to their distinct
properties and advantages, they are currently being investigated and integrated to form new
models or strategies in the areas of system control. In this paper, a neuro-fuzzy controller
(referred to as NFCGA) based on the radial basis function neural network is tuned
automatically using genetic algorithms (GA). A linear mapping method is used to encode the
GA chromosome, which consists of the width and centre of the membership functions, and also
the weights of the controller. Dynamic crossover and mutation probabilistic rates are...