110721.

Reducing Communication Overhead In Distributed Logic Simulation Of Circuits
- Amar Guettaf,Pirouz Bazargan-sabet
Distributed simulation represents an attractive
and smart way of improving the verification speed
of large VLSI circuits. Unfortunately, this inexpensive
approach suffers from the low performance
of the communication networks used to connect local
workstations. In this paper, we present a partitioning
algorithm that attempt to find a suitable
balance between the communication and the
execution load in a distributed simulator to enhance
its speedup. The main features of this method are
the use of logic replication to reduce the communication
overhead and a realistic cost function that
takes into account the activity of signals. Signals'
activity can be obtained through a probabilistic
evaluation. A distributed simulator implementing
a conservative synchronization method has been
used to...

110722.

David N. Turner, An Teallach Limited,
Two different operational interpretations of intuitionistic
linear logic have been proposed in the literature. The simplest
interpretation recomputes non-linear values every time
they are required. It has good memory-management properties,
but is often dismissed as being too inefficient. Alternatively,
one can memoize the results of evaluating non-linear
values. This avoids any recomputation, but has weaker
memory-management properties. Using a novel combination
of type-theoretic and operational techniques we give a
concise formal comparison of the two interpretations. Moreover,
we show that there is a subset of linear logic where
the two operational interpretations coincide. In this subset,
which is sufficiently expressive to encode call-by-value
lambda-calculus, we can have the best of both worlds: a
simple...

110723.

Implicit Coercions in Type Systems
- Gilles Barthe
. We propose a notion of pure type system with implicit coercions.
In our framework, judgements are extended with a context of
coercions Delta and the application rule is modified so as to allow coercions
to be left implicit. The setting supports multiple inheritance and can be
applied to all type theories with Pi-types. One originality of our work is
to propose a computational interpretation for implicit coercions. In this
paper, we demonstrate how this interpretation allows a strict control on
the logical properties of pure type systems with implicit coecions.
1 Introduction
The increasing importance of mathematical software has been accompanied by
a drift of mainstream mathematics towards mathematical...

110724.

Accurate VHDL Delay and Power Characterization of CMOS Logic Cells
- N. Dumitru,R. Nouta
This paper presents a model for characterizing delay
and power for CMOS logic cells that accounts for input
slope and output capacitance loading. A method
for deriving the model parameters and VHDL modeling
for simple logic gates is presented. The model
makes feasible delay and power estimation at VHDL
simulation speed, the errors of the model prediction
are less than 5% of Spice results.
1 Introduction
Analog circuit simulators suffer from severe memory
and execution time constraints and are hence unsuitable
for VLSI circuits. Logic and timing simulators
are much faster, but their accuracy depends upon the
accuracy of the model used for simulation. Usually,
delay and power models used by logic simulators assume
signal...

110725.

Linear Space Induction in First Order Logic with RELIEFF
- Uros Pompe,Igor Kononenko
Current ILP algorithms typically use variants and extensions of the greedy search. This prevents them to
detect significant relationships between the training objects. Instead of myopic impurity functions, we propose
the use of the heuristic based on RELIEF for guidance of ILP algorithms. At each step, in our ILP-R system,
this heuristic is used to determine a beam of candidate literals. The beam is then used in an exhaustive
search for a potentially good conjunction of literals. From the efficiency point of view we introduce interesting
declarative bias which enables us to keep the growth of the training set, when introducing new variables, within
linear bounds...

110726.

An Algorithm for Exact Bounds on the Time Separation of Events in Concurrent Systems
- Tod Amon,Henrik Hulgaard,Steven M. Burns,Gaetano Borriello
Determining the time separation of events is a fundamental
problem in the analysis, synthesis, and optimization
of concurrent systems. Applications range
from logic optimization of asynchronous digital circuits
to evaluation of execution times of programs for
real-time systems. We present an efficient algorithm
to find exact (tight) bounds on the separation time of
events in an arbitrary process graph without conditional
behavior. The algorithm is based on a functional
decomposition technique that permits the implicit evaluation
of an infinitely unfolded process graph.
1 Introduction
In this paper, we derive an exact algorithm that
determines tight upper and lower bounds on the separation
in time of an arbitrary pair of system events.
Depending on the level...

110727.

A Proof-Theoretic Approach to Knowledge
- Mariko Yasugi,Sobei H. Oda
rators K 1 and K 2 . It is
essentially equivalent to the modal logic S4, with two neccesity operators.
For technical reasons, we employ a sequential calculus.
The cut elimination theorem for KL can be proved by following that of the
propositional part of Gentzen's LK. Two of its consequences (elimination of
3
This work has been supported in part by Grant-in-Aid for Scientific Researches (No.10874024)
and by RIMS
y
This work has been supported in part by Grant-in-Aid for Scienific Researches
(No.09630018)
knowledge operators and separation of formula sets) can be proved similarly to
the corresponding lemmas in [1]. They serve as key lemmas in establishing
various facts to solve the...

110728.

Formal Real-Time Imagination
- Madhura Nirkhe,Sarit Kraus
Formal real-time imagination is a term that may curiously describe the activities
of a commonsense agent in a real-time setting in general, and in a tight
deadline situation in particular. We briefly describe an `active-logic' mechanism
that fits this description. Temporal projection is an essential component of realtime
planning. We draw a parallel between imagination as we understand it in
human context and the capacity of the automated agent to formulate mental images
of possible scenarios and plans of action in the course of its reasoning. We
outline a treatment of temporal issues of significance to a time-situated reasoning
mechanism in a dynamic setting with deadlines. The Yale...

110729.

There's No Substitute for Linear Logic
- Philip Wadler
Surprisingly, there is not a good fit between a syntax for linear logic in the style
of Abramsky, and a semantics in the style of Seely. Notably, the Substitution Lemma
is valid if and only if !A and !!A are isomorphic in a canonical way. An alternative
syntax is proposed, that has striking parallels to Moggi's language for monads. In the
old syntax, some terms look like the identity that should not, and vice versa; the new
syntax eliminates this awkwardness.
1 Introduction
This paper has two purposes: to show that linear logic has no substitute, and to propose
one.
The first part presents a standard syntax and semantics...

110730.

On Semantics of Algorithms with Continuous Time
- Anatol Slissenko
We consider a class of algorithms with explicit continuous time, a logic which suffices to
write requirement specifications for them in a way close to natural language, and, finally, the
corresponding verification problem. Our main goal is to represent the whole problem in one
logic. As algorithms we take block Gurevich machines [Gur95] over a signature with addition
of reals, and as the logic we take an appropriate extension of the theory of real addition. A
definition of semantics of algorithms of this type is given, without infinitesimals as compared to
our previous one [BS97b], however under a condition not too much restricting for applications.
Then we...

110731.

Logical Foundations of Eval/Quote Mechanisms, and the Modal Logic S4
- Jean Goubault-larrecq
Starting from the idea that cut elimination is the precise
meaning of program execution, we design two languages
of constructions for the minimal logic S4, yielding
-calculi with idealized versions of Lisp's eval and
quote. The first, the S4 -calculus, is based on Bierman
and De Paiva's proposal, and has all desirable logical
properties, except for its non-operational flavor. The second,
the evQ-calculus, is more complicated, but has
a clear operational meaning: it is a tower of interpreters
in the style of Lisp's reflexive tower. Remarkably, this
language was developed from purely logical principles,
but nonetheless provides some operational insight into
eval/quote mechanisms.
1 Introduction
Let's consider two dual questions.
The first is: is there...

110732.

Finer Control of Weakening and Contraction: Towards a Separated-Linear Lambda Calculus (Summary)
- John Maraist
nisms by which we introduce the copying
or discarding of terms. A term is discarded when it is substituted for a variable which appears only
on the left side of a typing judgement, which can occur only as the result of applying a weakening
rule; a term is duplicated when it is substituted for a variable which appears more than once on
the right side of a typing judgement, which can occur only by a contraction rule.
In the substructural lambda calculi I [3], A and L [8], the use of (respectively) weakening,
contraction and both are simply banned. These systems are not suOEcient here: while...

110733.

Verification of Logic Programs with Delay Declarations
- Krzysztof R. Apt
. Logic programs augmented with delay declarations form a
higly expressive programming language in which dynamic networks of
processes that communicate asynchronously by means of multiparty channels
can be easily created. In this paper we study correctness these programs.
In particular, we propose proof methods allowing us to deal with
occur check freedom, absence of deadlock, absence of errors in presence
of arithmetic relations, and termination. These methods turn out to be
simple modifications of the corresponding methods dealing with Prolog
programs. This allows us to derive correct delay declarations by analyzing
Prolog programs. Finally, we point out difficulties concerning proofs
of termination.
Notes. The research of the first author was...

110734.

Tractable Approximate Deduction using Limited Vocabularies
- Mukesh Dalal,David W. Etherington
A new approach to tractable deduction from
an expressive knowledge base is presented that
approximates formulae by automatically mapping
them to some restricted language. Various
mappings and their properties are discussed,
and an anytime algorithm to compute approximations
is presented. Several published approaches
prove to be special instances of ours.
To illustrate this, our formalism is used to formalize
hierarchical knowledge bases, and to extend
them by allowing negation and mutual exclusion.
We believe this to be the first comprehensive
theoretical framework for approximate
reasoning.
1 Introduction
It is well known that reasoning with a knowledge representation
system becomes more difficult as the representation
language becomes more expressive [ Levesque and
Brachman, 1985 ] . Reasoning is apparently...

110735.

Handling Infeasible Specifications of Cryptographic Protocols
- Li Gong
In the verification of cryptographic protocols along the
approach of the logic for authentication by Burrows,
Abadi, and Needham, it is possible to write a specification
which does not faithfully represent the real world
situation. Such a specification, though impossible or
unreasonable to implement, can go undetected and be
verified to be correct. It can also lead to logical statements
that do not preserve causality, which in turn can
have undesirable consequences. Such a specification,
called an infeasible specification here, can be subtle and
hard to locate. This note shows how the logic of cryptographic
protocols by Gong, Needham, and Yahalom
can be enhanced with a notion of eligibility to preserve
causality of...

110736.

Automated Deduction in a Graphical Temporal Logic
- L. E. Moser,P. M. Melliar-smith,Y. S. Ramakrishna,G. Kutty,L. K. Dillon
. Real-Time Graphical Interval Logic is a modal logic for reasoning about
time in which the basic modality is the interval. The logic differs from other logics in
that it has a natural intuitive graphical representation that resembles the timing diagrams
drawn by system designers. We have developed an automated deduction system for
the logic, which includes a theorem prover and a user interface. The theorem prover
checks the validity of proofs in the logic and produces counterexamples to invalid
proofs. The user interface includes a graphical editor that enables the user to create
graphical formulas on a workstation display, and a database and proof manager that
tracks...

110737.

Designing Advanced Databases Using Dependency Graph Conducted Schema Transformation Algorithm (Extended Abstract)
- Patrick Van Bommel
Tecnical Note CSI-N9703, March 1997
Current address: Dept. of Information Systems, University of Nijmegen, Toernooiveld
1, NL-6525 ED Nijmegen, The Netherlands. Email: gyurik@cs.kun.nl
Contents
1 Introduction 3
2 Framework for algorithmic schema transformation 4
2.1 Transformation dependency graphs : : : : : : : : : : : : : : : 5
2.2 The transformation algorithm : : : : : : : : : : : : : : : : : : 7
3 From conceptual models to OO databases 9
3.1 Approach : : : : : : : : : : : : : : : : : : : : : :...

110738.

A Three-Valued Linear Temporal Logic for Reasoning about Concurrency
- Beata Konikowska
this paper we
choose the second one, since it allows to preserve most intuitions and methods connected with
the classical case, including classical tautologies on formula level, as well as the classical method
of Hilbert-type axiomatization together with the standard proof of its completeness by canonical
model construction.
3 Syntax and semantics of the language

110739.

Handling Database Updates in Two-dimensional Temporal Logic
- Marcelo Finger
This paper deals with the description of the evolution of the understanding
of the history of a particular world. We have particular interest in describing
certain problems that occur in database systems due to updates. For this
purpose, we introduce a two-dimensional temporal logic as a formalism which
enables the description of both the history and the evolution of the beliefs
about the history. The historical dimension describes the history of the world
according to a certain belief. The belief dimension describes the evolution of
those beliefs.
The historical dimension is then associated with an historical database,
and transactions in the database are associated with changes in belief. Besides
describing...

110740.

Spatial Logic and the Complexity of Diagrammatic Reasoning
- Oliver Lemon,Ian Pratt
. Researchers have sought to explain the observed "efficacy" of diagrammatic reasoning (DR) via the notions of "limited abstraction" and inexpressivity [17, 20]. We argue that application of the concepts of computational complexity to systems of diagrammatic representation is necessary for the evaluation of precise claims about their efficacy. We show here how to give such an analysis. Centrally, we claim that recent formal analyses of diagrammatic representations (DRs) (eg: [14]) fail to account for the ways in which they employ spatial relations in their representational work. This focus raises some problems for the expressive power of graphical systems, related...