110721.

An Exact Constraint Logic Programming Algorithm for the Traveling Salesman Problem with Time Windows
- Gilles Pesant,Michel Gendreau,Jean-yves Potvin,Jean-marc Rousseau
This paper presents a constraint logic programming model for the traveling
salesman problem with time windows which yields an exact branchand
-bound optimization algorithm without any restrictive assumption on
the time windows. Unlike dynamic programming approaches whose performance
relies heavily on the degree of discretization applied to the data,
our algorithm does not suffer from such space-complexity issues. The
data-driven mechanism at its core more fully exploits pruning rules developed
in operations research by using them not only a priori but also
dynamically during the search. Computational results are reported and
comparisons are made with both exact and heuristic algorithms. On
Solomon's well-known test bed, our algorithm is instrumental in...

110722.

Adaptive Extensions to a Multi-Branch Run-to-Run Controller for Plasma Etching
- James R. Moyne,Nauman Chaudhry
Fuzzy logic and database learning mechanisms have been incorporated into a
generic plasma etching run-to-run controller, resulting in a very dynamic, adaptable
and robust system. The system features an Applied 8300 RIE controlled by a
Techware II equipment controller. A TCP/IP connection links this equipment
controller to the run-to-run controller residing on a SUN. The run-to-run control
environment is generic in that the basic control framework and controller
development results are applicable to VLSI manufacturing in general. The
controller is multi-branch as it utilizes multiple algorithms in complementary fashion
to achieve process optimization and control. The current implementation utilizes
three branches: (1) a linear approximation control algorithm, (2) an...

110723.

A Logic for Concurrent Events and Action Failure
- David Morley,Liz Sonenberg
When reasoning about agents interacting in a dynamic world, two problems present themselves:
other events and actions may occur while an agent is acting; and an agent's actions may
fail. We present a more expressive formalism for representing the different ways that events can
occur together and extend a recently introduced logic of events to handle concurrent events. We
apply the approach of Traverso and Spalazzi to handle actions and failure to obtain a logic that
allows for concurrent events and admits reasoning with failure.
1 Introduction
Reasoning about the actions of autonomous agents has been a problem of continuing interest to
researchers in AI. When agents are...

110724.

Deriving Partial Correctness Logics From Evolving Algebras
- Arnd Poetzsch--heffter
Introduction
This extended abstract gives an introduction into the development of partial correctness
logics for programming languages specified by evolving algebras. A partial correctness
logic is a programming logic that allows to prove program properties of the form: "whenever
program point P is reached during execution, assertion A is true". We derive a basic
axiom (schema) from an evolving algebra and use this axiom to prove more convenient
logics correct.
This work aims to develop the foundations for programming environments that support
formal reasoning about programs. One of the major problems with this challenge
is the systematic design of programming logics for realistic programming languages. Experiences
e.g. with Hoare logic...

110725.

Towards Integrating Partial Evaluation in a Specialization Framework based on Generic Abstract Interpretation (Extended Abstract)
Interpretation
Germ'an Puebla
John Gallagher
y
Manuel Hermenegildo
(Extended Abstract)
1 Introduction
Partial evaluation [JGS93, DGT96] specializes programs for known values of the input. Partial
evaluation of logic programs has received considerable attention [Neu90, LS91, Sah93, Gal93,
Leu97] and several algorithms parameterized by different control strategies have been proposed
which produce useful partial evaluations of programs. Regarding the correctness of such transformations,
two conditions, defined on the set of atoms to be partially evaluated, have been identified
which which ensure correctness of the transformation: "closedness" and "independence" [LS91].
From a practical point of view, effectiveness, that is, finding suitable control strategies which
provide an appropriate level of specialization while ensuring termination, is a crucial...

110726.

A Quadratic Optimiser in a Constraint Logic Programming Paradigm
This paper presents a quadratic optimiser for solving quadratic programming optimisation
problem in constraint logic programming paradigm. Quadratic programming optimisation
problems are a subclass of the general nonlinear programming optimisation problems in
operational research. The optimiser showed fast convergence over the tested problems.
It enriched the CLP(R) in Sicstus Prolog with the capability of quadratic programming
optimisation in addition to the existing capability of linear programming optimisation
which opens further domain of applications to CLP. Moreover, it could be extended to
be used by successive quadratic programming method to solve a large class of nonlinear
optimisation problems.
Introduction
Logic programming (LP) languages are a form of declarative languages based on...

110727.

Interpolation, Preservation, and Pebble Games
- Jon Barwise,Johan Van Benthem
Preservation and interpolation results are obtained for L1! and sublogics
L ` L1! such that equivalence in L can be characterized by suitable
back-and-forth conditions on sets of partial isomorphisms.
1 Introduction
In the heyday of infinitary logic in the 1960's and 70's, most attention was focused
on L!1! and its fragments (see e.g. Keisler [19]), since countable formulas
seemed best behaved. The past decade has seen a renewed interest in L1! and
its finite variable fragments L
(k)
1! (for 2 k ! !) and the modal fragment L
Pi
1!
(see e.g. Ebbinghaus and Flum [17] on the former and Barwise and Moss [9] on
the latter), due to various connections...

110728.

Simulation and Analysis of Business Processes Using GOLOG
- Dimitris Plexousakis
This paper describes a novel approach to simulating and
analyzing business processes using GOLOG, a high-level
logic programming language suitable for defining complex
behaviors and capable of simulating action execution.
The language is based on an extended version of the
situation calculus and incorporates a formal theory of
action. Business processes can be viewed as actions
(physical or perceptual) that affect the state of affairs
or an agent's knowledge of this state. Using GOLOG,
business processes can be specified, synthesized and tested
for feasibility and consistency. The theoretical framework
behind GOLOG includes a solution to the frame problem
for perceptual and complex actions, as well as, a formal
method for process analysis. The...

110729.

Some Monoidal Closed Categories of Stable Domains and Event Structures
- Guo-qiang Zhang
This paper introduces the following new constructions on stable domains and event
structures: the tensor product, the linear function space, and the exponential. It gives
rise to a monoidal closed category of dI-domains as well as one of stable event structures
which can be used to interpret intuitionistic linear logic. Finally, the usefulness of the
category of stable event structures for modeling concurrency and its relation to other
models are discussed.
CONTENTS

110730.

An Agent Architecture That Combines Backward and Forward Reasoning
- R. A. Kowalski,F. Sadri,F. Toni
. We present a proof procedure that combines backward reasoning
with logic programs and forward reasoning with integrity constraints.
We illustrate the use of the proof procedure as the inference
engine underlying agents. Roughly speaking, the backward reasoning
component of the proof procedure is responsible for the deliberative behaviour
of agents, whereas the forward reasoning component is responsible
for their reactive behaviour.
1 Introduction
Recent years have seen a shift in the treatment of agents in artificial intelligence.
In conventional approaches, intelligent agents reason and plan within a closed
environment, producing a complete plan before they start executing it. In more
recent, and arguably more realistic approaches, intelligent agents reason and
plan...

110731.

Programming Languages for Distributed Applications
- Seif Haridi,Peter Van Roy,Christian Schulte
Much progress has been made in distributed computing in the areas of distribution structure,
open computing, fault tolerance, and security. Yet, writing distributed applications remains difficult
because the programmer has to manage models of these areas explicitly. A major challenge
is to integrate the four models into a coherent development platform. Such a platform should
make it possible to cleanly separate an application's functionality from the other four concerns.
Concurrent constraint programming, an evolution of concurrent logic programming, has both the
expressiveness and the formal foundation needed to attempt this integration. As a first step, we
have designed and built a platform that separates an application's functionality...

110732.

The Logic of Propagation in The Inscape Environment
- Dewayne E. Perry
The Inscape Environment research project addresses issues in
supporting the development of large systems by large numbers
of programmers. One aspect of this research is the "constructive
use" of formal module interface specifications - that is,
given that you have formal specifications, what can you do with
them. In Inscape, the specifications form the basis for providing
an environment that is knowledgeable about the process of
developing and evolving software systems, an environment that
works in symbiosis with the programmer to develop and evolve
a software system.
In this discussion, I present how Inscape uses operation
specifications (based on Hoare's input/output predicate approach)
as the basis for synthesizing the interfaces for such...

110733.

Dyana --- The Pilot Project For Investigation Of Distributed Programs And Computer Systems
- A. G. Bakhmurov,R. L. Smeliansky
The tool of distributed computer environment simulation and analysis is described.
The key features of this tool are: the possibility of both quantitative and
algorithmic analysis of system to be modeled; the time complexity estimation subsystem
which helps to avoid the instruction-level simulation of target computer
system. A model development language overview is presented. Certain attention
is paid to the algorithmic analysys and specification features along with the
technology of model development.
Keywords: Simulation, performance analysis, distributed computer systems, temporal
logic
1. Introduction
The DYANA system (DYnamic ANAlyzer) is the software system which is
proposed to help analyze distributed computer environment operation. The design
and development of the system were aimed at...

110734.

Strictness Analysis in Logical Form
- Thomas P. Jensen
This paper presents a framework for comparing two strictness analysis techniques:
Abstract interpretation and non--standard type inference. The comparison is based
on the representation of a lattice by its ideals. A formal system for deducing inclusions
between ideals of a lattice is presented and proved sound and complete. Viewing
the ideals as strictness properties we use the formal system to define a program logic
for deducing strictness properties of expressions in a typed lambda calculus. This
strictness logic is shown to be sound and complete with respect to the abstract interpretation,
which establishes the main result that strictness analysis by type--inference
and by abstract interpretation are equally powerful...

110735.

Confinement Properties for Programming Languages
- Dennis Volpano,Geoffrey Smith
ation is to use digital signatures. Here
you would verify a digital signature that is computed over the program using TrustMe's
private key. But this is not much help in the scenario above. It merely provides you with
confirmation that the program came from TrustMe so that they can be held accountable
if some day you discover that the program did misbehave. By that time there is no telling
how many "data warehouses" [13] already store the information.
To appear in SIGACT News, 1998
But suppose we have a formal system, or logic, in which to reason about a program's
ability to preserve privacy. Then our trust in...

110736.

Techniques for Preventing Recomputation in Logic Programs
- Paulo Jorge,Sousa Azevedo
In this thesis we investigate techniques for preventing recomputation in the execution of logic
programs. One can reduce recomputation by eliminating subquery redundancy. This can be
achieved by storing intermediate results, which are shared between identical subqueries. This is
known as the tabulation technique. We consider top-down evaluation procedures incorporating a
tabulation or `lemmatization' mechanism and also bottom-up evaluation with goal orientation, as
exemplified by the `magic sets' transformation. By assessing these two forms of evaluation and by
pointing out some relationships between them we proceed towards a recomputation-free evaluation.
Several top-down evaluation strategies that use tabulation have been proposed in the literature.
However, all of these mechanisms...

110737.

Higher-Order Logic Programming as Constraint Logic Programming
- Spiro Michaylov,Frank Pfenning
Higher-order logic programming (HOLP) languages are particularly useful for various kinds of metaprogramming
and theorem proving tasks because of the logical support for variable binding via -
abstraction. They have been used for a wide range of applications including theorem proving, programming
language interpretation, type inference, compilation, and natural language parsing. Despite their
utility, current language implementations have acquired a well-deserved reputation for being inefficient.
In this paper we argue that HOLP languages can reasonably be viewed as Constraint Logic Programming
(CLP) languages, and show how this can be expected to lead to more practical implementations
by applying the known principles for the design and implementation of...

110738.

Constructive Natural Deduction And Its "omega-Set" Interpretation
- Eugenio Moggi
. Various Theories of Types are introduced, by stressing the analogy "propositionsas
-types" : from propositional to higher order types (and Logic). In accordance with this,
proofs are described as terms of various calculi, in particular of polymorphic (second order) l-
calculus. A semantic explanation is then given by interpreting individual types and the
collection of all types in two simple categories built out of the natural numbers (the modest sets
and the universe of w-sets). The first part of this paper (syntax) may be viewed as a short
tutorial with a constructive understanding of the deduction theorem and some work on the
expressive power of first...

110739.

Introducing Some Classical Elements of Modal Logic to the Propositional Logics of Qualitative Probabilities
- Dimitar P. Gelev
This paper presents the construction of canonical models for a number of logics of qualitative
probabilities by introducing a conservative infinitary rule into their axiomatizations.
These logics include the minimal logic of qualitative probabilities [Seg71, Gar75] and a
new multioperator propositional logic, that contains qualitative probabilistic analogons of
operations essential to propositional dynamic logic. These operations capture some basic
laws for stochastic processes into this new logic's semantics and are given a complete
axiomatization.
The paper also presents qualitative probabilistic versions of the modal logic techniques
of unravelling and filtration.
All the constructs and arguments in this paper are suitable to be combined with their
counterparts for other propositional, e.g....

110740.

Local Specification of Distributed Families of Sequential Objects
- Hans-dieter Ehrich
. Fully concurrent models of distributed object systems are
specified using linear temporal logic that does not per se cope with concurrency.
This is achieved by employing the principle of local sequentiality:
we specify from local viewpoints assuming that there is no intraobject
concurrency but full inter-object concurrency. Local formulae are
labelled by identity terms. For interaction, objects may refer to actions
of other objects, e.g., calling them to happen synchronously. A locality
predicate allows for making local statements about other objects. The
interpretation structures are global webs of local life cycles, glued together
at shared communication events. These interpretation structures are
embedded in an interpretation frame that is a...