110721.

Compiling Systemic Grammar into Feature Logic Systems
- Renate Henschel
this paper is, therefore, to re-represent
systemic grammar resources in a standard typed feature logic in order (1) to clarify
theoretically the relation between systemic grammar and state-of-the-art feature logics,
and (2) to serve as point of departure for bidirectional processing of systemic grammar.
Four such representations in the feature logic formalisms ale, tfs, cuf and tdl

110722.

GOLEX --- Bridging the Gap between Logic (GOLOG) and a Real Robot
- Dirk Hahnel,Wolfram Burgard,Gerhard Lakemeyer
. The control of mobile robots acting autonomously in the real world is one of the
long-term goals of the field of artificial intelligence. So far the field lacks methods bridging
the gap between the sophisticated symbolic techniques to represent and reason about action
and more and more reliable low-level robot control and navigation systems. In this paper we
present GOLEX, an execution and monitoring system for the logic-based action language
GOLOG and the complex and distributed RHINO control software which operates on RWI
B21 and B14 mobile robots. GOLEX provides the following features: it maps abstract primitive
actions into low-level commands of the robot control system,...

110723.

Jinni: Intelligent Mobile Agent Programming at the Intersection of Java and Prolog
- Paul Tarau
. Jinni (Java INference engine and Networked Interactor), is
a lightweight, multi-threaded, logic programming language, intended to
be used as a flexible scripting tool for gluing together knowledge processing
components and Java objects in distributed applications.
Jinni threads are coordinated through blackboards, local to each process.
Associative search based on term unification (a variant of Linda) is used
as the basic synchronization mechanism. Threads are controlled with tiny
interpreters following a scripting language based on a subset of Prolog.
Mobile threads, implemented by capturing first order continuations in a
compact data structure sent over the network, allow Jinni to interoperate
with remote high performance BinProlog servers for CPU-intensive
knowledge processing and...

110724.

STDL A Portable Language for Transaction Processing
- Philip A. Bernstein,Per O. Gyllstrom,Tom Wimberg
This paper
describes STDL's transaction features: transaction bracketing,
transactional remote procedure call, transactional queuing, recoverable
terminal I/O, and transactional exception handling.
STDL relies on standard C and COBOL for most application logic and
all operations on SQL databases and files. All transactional features of
STDL and new features outside standard C and COBOL are isolated in
procedures written in the STDL language. These procedures are called
tasks. This isolation of transactional features is quite different than
other persistent programming languages: one can use applications
written in standard C or COBOL; and to implement STDL, it is
possible to map clauses of task language onto operations of most any
distributed TP monitor.
Keywords: transactions,...

110725.

Design of Experiments in CAD: Context and New Data Sets for ISCAS'99
- Franc Brglez,Rolf Drechsler
This paper introduces the background and motivation
for the two special sessions at ISCAS'99. The sessions
bring together eight papers, each rooted in the methodology
of experimental design, and contributed by collaborating
teams of distributed participants. The paper briefly outlines
the premises of the companion papers that follow, provides
a brief description of a typical experimental design,
and introduces a design for archival of data sets and results
that are to be readily accessible on the Web.
Keywords: design of experiments, circuit equivalence
classes, benchmarking.
1 Introduction
More than a thousand mathematical problems arising in engineering
and science have been shown to be NP-hard. Data
sets such as ISCAS'85, ISCAS'89, and extensions introduced
at logic...

110726.

Intellectual Property Protection By Watermarking Combinational Logic Synthesis Solutions
- Darko Kirovski,Yean-yow Hwang,Miodrag Potkonjak,Jason Cong
The intellectual property (IP) business model is vulnerable to a
number of potentially devastating obstructions, such as misappropriation
and intellectual property fraud. We propose a new method
for IP protection (IPP) which facilitates design watermarking at the
combinational logic synthesis level. We developed protocols for
embedding designer- and/or tool-specific information into a logic
network while performing multi-level logic minimization and technology
mapping. We demonstrate that the difficulty of erasing author
's signature or finding another signature in the synthesized design
can be made arbitrarily computationally difficult. We also
developed a statistical method which enables us to establish the
strength of the proof of authorship. The watermarking method has
been tested on a...

110727.

Efficiently Supporting Fault-Tolerance in FPGAs
- John Lach,William H. Mangione-smith,Miodrag Potkonjak
While system reliability is conventionally
achieved through component replication, we
have developed a fault-tolerance approach for
FPGA-based systems that comes at a reduced
cost in terms of design time, volume, and
weight. We partition the physical design into
a set of tiles. In response to a component
failure, we capitalize on the unique
reconfiguration capabilities of FPGAs and
replace the affected tile with a functionally
equivalent tile that does not rely on the faulty
component. Unlike fixed structure faulttolerance
techniques for ASICs and
microprocessors, this approach allows a single
physical component to provide redundant
backup for several types of components.
Experimental results conducted on a subset of
the MCNC benchmarks demonstrate a high
level of reliability with low...

110728.

A Hybrid Backward Slicing Algorithm Producing Executable Slices for Prolog
- Campus Universitaire De Beaulieu
ion of a literal) An abstraction of a literal A is the literal A where zero, one
or more arguments have been replaced by anonymous variables.
Definition 3 (Abstraction of a clause) If C is the clause A / B 1 ; : : : ; Bn , an abstraction of C is
either:
ffl the empty clause, denoted by ;, or
ffl a unit clause, denoted by A
0
/, where A
0
is an abstraction of A, or
ffl a clause of the form A
0
/ B
0
1 ; : : : ; B
0
p , derived from C by removing zero, one or more literals of the
body and where all...

110729.

STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems
- Tom'as E. Uribe,Anca Browne,Eddie Chang,Arjun Kapur,Zohar Manna,Henny B. Sipma
. The Stanford Temporal Prover, STeP, combines deductive
methods with algorithmic techniques to verify linear-time temporal logic
specifications of reactive and real-time systems. STeP uses verification
rules, verification diagrams, automatically generated invariants, model
checking, and a collection of decision procedures to verify finite- and
infinite-state systems.
System Description: The Stanford Temporal Prover, STeP, supports the
computer-aided formal verification of reactive, real-time (and, in particular, concurrent)
systems based on temporal specifications. Reactive systems maintain
an ongoing interaction with their environment; their specifications are typically
expressed as constraints on their behavior over time. STeP is not restricted
to finite-state systems, but combines algorithmic and deductive methods to allow
the verification of a broad class...

110730.

Proof-terms for classical and intuitionistic resolution (Extended Abstract)
- Eike Ritter,David Pym,Lincoln Wallen
. We exploit a system of realizers for classical logic, and a
translation from resolution into the sequent calculus, to assess the intuitionistic
force of classical resolution for a fragment of intuitionistic
logic. This approach is in contrast to formulating locally intuitionistically
sound resolution rules. The techniques use the ¯ffl-calculus, a development
of Parigot's ¯-calculus.
1 Introduction
1.1 Local methods for intuitionistic logic
It is standard practice to draw a sharp distinction between local methods of
automated deduction for classical logic, inspired by techniques such as Robinson
's resolution [17] and Maslov's inverse method [9], and global methods, those
inspired by Gentzen's sequent calculus [8] and Smullyan's tableaux systems [18].
For a...

110731.

Deriving Logic Programs From Observations
- David Gilbert,Christopher Hogger
This paper describes a method for deriving logic programs from observations that can
be made of the progress of a computation. Such observations can be regarded as extrinsic
specifications, and can be represented as directed acyclic graphs. Each computation that
the system can perform is represented by a path through the graph which in turn can be
described in first order logic. Logic programs can be derived from these first order logic
descriptions by standard transformations. In this paper we chose to derive sequential logic
programs, but the method is equally applicable to concurrent systems.
Introduction
A logic programming system can be viewed as a black box for...

110732.

A Spatio-Temporal Logic for 2D Multi-Agent Problem Domains
- Wanlin Pang
We formally present a first order logic intended for representing and reasoning about 2D dynamic multiagent
problem domains. The unique feature of the logic is the uniform use of a Cartesian plane as the
basis for both the spatial and temporal ontology. Our temporal structure has an ever changing present.
Relative to each present there is a past and a future. A feature of this temporal structure is its ability
to capture when knowledge is added or updated.
1 Introduction
One important facet of Distributed Artificial Intelligence (DAI) is the composition of groups of agents
at different social levels: groups, organizations, etc. [?]. A requirement is the...

110733.

Default Logic and Autoepistemic Logic: Fixed Points and Common Semantic Framework
- Choh Man Teng
When we work with information from multiple sources, the formats of the knowledge bases
may not be uniform. It would be desirable to be able to combine a knowledge base of default
rules with one containing autoepistemic formulas. Previous works on relating default logic
and autoepistemic logic mostly impose some constraints on autoepistemic logic, and thus
are not suitable for combining the two logics. We first present a fixed point formulation
of autoepistemic logic analogous to that of default logic. Then we introduce a possible
world framework with a partition structure, which corresponds to our intuitive notion of
accessibility as linking alternate "possible" worlds. We show that...

110734.

An Institution of Object Behaviour
- Jos Félix Costa
. An institution for a simple logic of behaviour is built using a
cofibration from a category of transition systems into the envisaged category
of signatures. The chosen propositional, linear temporal logic distinguishes
between event occurrence and event enabling. The satisfaction condition is
proved using a fibered adjunction between transition systems and their
computations. The operational semantics of behaviour specifications is
briefly discussed.
1 Introduction
Consolidating the conjectures in [SernadasA et al 92a], we study the
problem of setting-up a suitable institution (see [Goguen and Burstall 84]) of
linear temporal logic from a given reasonable semantic domain of object
behaviour. For the sake of simplicity we work towards a propositional
fragment. No...

110735.

A Combinator-based Order-sorted Higher-order Unification Algorithm
- Patricia Johann,Fachbereich Informatik
This paper develops a sound and complete transformation-based algorithm for
unification in an extensional order-sorted combinatory logic supporting constant
overloading and a higher-order sort concept. Appropriate notions of order-sorted
weak equality and extensionality --- reflecting order-sorted fij-equality in the
corresponding lambda calculus given by Johann and Kohlhase --- are defined, and
the typed combinator-based higher-order unification techniques of Dougherty are
modified to accommodate unification with respect to the theory they generate. The
algorithm presented here can thus be viewed as a combinatory logic counterpart
to that of Johann and Kohlhase, as well as a refinement of that of Dougherty, and
provides evidence that combinatory logic is well-suited to serve...

110736.

Multi Lingual Sequent Calculus and Coherent Spaces
- Achim Jung,Mathias Kegelmann,M. Andrew Moshier
We study a Gentzen style sequent calculus where the formulas on the left and right
of the turnstile need not necessarily come from the same logical system. Such a
sequent can be seen as a consequence between different domains of reasoning. We
discuss the ingredients needed to set up the logic generalized in this fashion.
The usual cut rule does not make sense for sequents which connect different logical
systems because it mixes formulas from antecedent and succedent. We propose a
different cut rule which addresses this problem.
The new cut rule can be used as a basis for composition in a suitable category of
logical systems. As...

110737.

A Reliable Mobile Agents Architecture
- Manfred Dalmeijer,Eric Rietjens,Michiel Soede,D. K. Hammer,A. T. M. Aerts
This paper describes the design of a novel mobile agent system that supports the flexible
and reliable interaction of autonomous components in an object-oriented distributed
system. It discusses the object-oriented design of the overall system together with a
number of important components in terms of the most important design decisions. A
detailed description of the reliability model is given in terms of the failure hypothesis and
the related recovery protocols. Special emphasis is given to the generality and efficiency
of the implementation and a number of preliminary experiences are described.
1. Introduction
This paper focuses on the design and implementation of an object oriented mobile agent
system. A mobile...

110738.

Sequential Implementation of Parallel Narrowing
Parallel Narrowing is a narrowing strategy which exploits expression parallelism. We
present the ørst implementation by transforming weakly orthogonal, constructor-based programs
into Prolog with the help of parallel deønitional trees. We deøne translation scheme
for the general case of multistep narrowing, which is then extended to parallel narrowing
by additional elimination rules. Our implementation is improved by combining parallel narrowing
with intermediate simpliøcation steps. Advantages of the new strategies and speciøc
challenges of a Prolog implementation are pointed out by comparative measurements.
1 Introduction
Functional logic languages combine the advantages of functional languages, such as higher order
functions and eOEcient evaluation with those of logic languages like search, logical...

110739.

A Survey of Categorical Computation: Fixed Points, . . .
Machine by Curien [Cur86]. It is based upon a weak categorical combinatory logic, viz.
lacking surjective pairing and extensionality, that arose as a direct semantic-to-syntactic translation
of the lambda calculus of tuples. The computational mode was combinator term reduction
through rewriting using a direct left-to-right parse algorithm, initially making the evaluation strategy
inefficiently eager
1
. Application is therefore simply juxtaposition, losing the full expressiveness
of-reduction that computes via substitution. Its overly strong bias towards the lambda calculus
was another factor that limited its expressiveness. On one hand the CAM demanded the existence
of categorical products but on the other it had no coproducts for developing many useful
data structures....

110740.

Definability and Descriptive Complexity on Databases of Bounded Tree-Width
- Martin Grohe,Julian Marino
. We study the expressive power of various query languages on relational
databases of bounded tree-width.
Our first theorem says that fixed-point logic with counting captures polynomial
time on classes of databases of bounded tree-width. This result should be seen
on the background of an important open question of Chandra and Harel [7] asking
whether there is a query language capturing polynomial time on unordered
databases. Our theorem is a further step in a larger project of extending the scope
of databases on which polynomial time can be captured by reasonable query languages.
We then prove a general definability theorem stating that each query on a class
of databases...