A Calculus Supporting Structured Proofs
- I. Dahn,Andreas Wolf
: Proofs in standard logical calculi have a simple structure (mostly a sequence, tree
or set of related formulas). Therefore, formal proofs are hard to understand or to present in an
intelligible way. The Block Calculus for first order logic introduced in this paper is a variant of
natural deduction that has highly structured proofs. These proofs can be presented in many
ways by hiding blocks of subproofs. Moreover it can be easily extended by other calculi. We
characterize the semantics of incomplete proof structures in the Block Calculus and prove it's
soundness and completeness.
1. Introduction 1
2. Some Definitions 3
3. Rules 5
4. Examples 7
5. Completeness and...
Applications of Circuit Probability Computation Using Decision Diagrams
- M. A. Thornton
Digital circuit output probabilities provide meaningful
information regarding the behavior of combinational
logic circuits. The computation of the probability
values can be computationally expensive when
Boolean equations or netlists are used. When the circuits
are represented by compact decision diagrams
(DD), efficient algorithms exist for determining the
probability values. The use of the probabilities based
on decision diagram representations are examined
here. Specifically, research results of investigations
into spectra computation, synthesis, symmetry detection
and DD reordering are surveyed.
The circuit output probability for a combinational
logic circuit can be defined as the probability that a
given output will yield a logical-1 value given the distributions
of the inputs. These probability values have
proven to be...
Modelling Garbage Collection Algorithms
- Howard Bowman,John Derrick,Richard Jones
We show how abstract requirements of garbage collection can be captured using temporal
logic. The temporal logic specification can then be used as a basis for process algebra
specifications which can involve varying amounts of parallelism. We present two simple CCS
specifications as an example, followed by a more complex specification of the cyclic reference
counting algorithm. The verification of such algorithms is then briefly discussed.
Keywords: Concurrency, garbage collection, temporal logic, CCS.
The memorymanagement of simple static programming languages, such as Fortran, can be handled
entirely by the compiler. The location of all variables can be fully determined at compile-time and
no run-time support for memory...
Retrieval of Complex Objects Using a Four-Valued Logic
- Thomas Rolleke,Norbert Fuhr
The aggregated structure of documents plays a key role in
full-text, multimedia, and network Information Retrieval
(IR). Considering aggregation provides new querying facilities
and improves retrieval effectiveness. We present a
knowledge representation for IR purposes which pays special
attention to this aggregated structure of objects. In addition,
further features of objects can be described. Thus,
the structure of full-text documents, the heterogeneity and
the spatial and temporal relationships of objects typical for
multimedia IR, and meta information for network IR are
representable within one integrated framework.
The model we propose allows for querying on the content
of documents (objects) as well as on other features.
The query result may contain objects having different
Non-Terminating Processes in the Situation Calculus
- Eugenia Ternovskaia,Ray Reiter
this paper -- an office coffee-delivery robot might be implemented as an infinite loop in
which the robot responds to exogenous requests for coffee that are maintained on a queue. Since a future
coffee request is always possible, the program never terminates.
As is the case for more conventional programs, we want some reliability assurances for robot controllers.
This paper describes the approach being taken by our Cognitive Robotics Group to expressing
and proving properties of non-terminating programs expressed in GOLOG, a high level logic programming
language for modeling and implementing dynamical systems. The kinds of properties we have in
mind are traditional in computer science: liveness,...
Iterative Combinational Logic Synthesis Techniques Using Spectral Data
- Mitchell Aaron Thornton,V. S. S. Nair
The spectral information of a Boolean function yields data regarding the correlation
between the input variables and the output of the function. This paper introduces a
spectral based methodology for combinational logic synthesis using linear transforms.
An analysis of the properties of the spectra obtained from these transforms is provided
and a synthesis algorithm using spectral techniques is presented. This result is significant
since it provides an algebraic method for including the XOR gate in the synthesis
process without resorting to manipulation of symbolic Boolean equations.
The design and development of digital systems is becoming increasingly complex and automated.
With the evolution of greater amounts of circuitry...
Fault Injection for Logic Synthesis Design using VHDL 1 of 8
- Todd A. Delong,Anup K. Ghosh,Barry W. Johnson,Joseph A. Profeta
Fault injection provides a method of assessing the dependability of a system under test.
Traditionally fault injection is employed near the end of the design process after hardware and
software prototypes have been developed. In order to eliminate costly re-designs near the end of
the design process, a methodology for performing fault injection throughout the design process is
described in this paper. This methodology incorporates a fault injection technique that can be used
with any VHDL model, including behavioral, synthesizeable VHDL models. The technique
separates the fault-free VHDL descriptions from the fault injection process so that existing models
can be used with minimal changes to the existing...
Asynchronous Pipeline Design using GaAs PDLL Logic and new CMOS dynamic techniques
- Shannon V. Morton,Michael J. Liebelt
We explore the potential for extremely
high asynchronous logic performance in CMOS and
GaAs dynamic logic structures. By using a new class of
GaAs dynamic logic, Pseudo-Dynamic Latched Logic,
we develop asynchronous control structures capable of
high-speed operation. We show how these techniques can
be used for CMOS design, and give performance estimates.
Asynchronous approaches have long been touted as
the ideal replacement for synchronous designs when clock
skew problems and power consumption become unmanageable.
However, the lack of asynchronous method
acceptance seems to indicate that these views are not
shared by the design community as a whole. This is
primarly due to the lower performance level offered by
asynchronous solutions in a...
Last Parallel Call Optimization and Fast Backtracking in And-parallel Logic Programming Systems
- Tang Dongxing,Enrico Pontelli,Manuel Carro,Gopal Gupta
In this paper we present a novel optimization called Last Parallel Call Optimization. The last parallel call optimization can be regarded as an extension of last call optimization, found in sequential systems, to and parallel systems. The last parallel call optimization leads to improved time and space performance for a majority of and-parallel programs. The last parallel call optimization is presented in detail in this paper and its advantages discussed at length. The last parallel call optimization can be incorporated in a parallel system (such as RAPWAM) through relatively minor modifications to the runtime machinery. We also present some experimental...
Foundations Of Temporal Query Languages
- David Toman
Temporal Databases are repositories of information dependent on time. The major difference
from standard, e.g., relational database systems, is the need of storing possibly infinite
objects, e.g., time spans.
In recent years, there have been numerous proposals that introduce time into standard
relational systems. Unfortunately, most of the attempts have been based on ad-hoc extensions
of existing database systems and query languages, e.g., TQUEL and TSQL. Such
extensions often create many problems, when precise semantics needs to be developed, if one
exists at all. In a recent survey by J. Chomicki, a clean way of defining temporal databases
based on logic was proposed. This methodology views temporal databases...
- Jan Chomicki,David Toman
ing of Temporal Databases and Temporal Query
Languages. We briefly survey the classical results. However, the main emphasis is on recent
developments in the area of temporal databases. In the light of several recent results
[Abiteboul et al., 1996, Chomicki and Kuper, 1995, Chomicki et al., 1996, Kanellakis et al., 1995,
Toman and Niwinski, 1996, Toman, 1996, Toman, 1997] many of the above issues have taken
an unexpected turn and the correctness of several mainstream approaches has to be reevaluated.
In many temporal data models, new features are added without considering their interaction with existing
2 Detailed Outline of the Tutorial
temporal dimensions of data
Efficient Integration of Declarative Paradigms into Symbolic Computation Systems
- Georgios Grivas
. This paper describes the efficient integration of the functional, logic and constraint
paradigms into symbolic computation systems. Moreover, it proposes the constraint
logic paradigm for the programming language of symbolic computation systems. First, it
describes the integration of a separate constraint logic inference engine with the functional
language of the symbolic computation system AlgBench. The procedural, functional, and
APL-like programming styles are inherited from Mathematica and are integrated on top of
its term-rewriting mechanism. The proposed language could serve as a stand alone programming
language. Second, it shows the efficient compilation of the resulting language to
an intermediate code. The compiler generates code for a uniform abstract...
O(N³) Algorithm for Bisimulation Equivalence w.r.t CTL* without the Next-Time Operator between Kripke Structures
- Mahesh Girkar,Robert Moll
Concurrent systems are often modeled by labeled state--transition graphs called Kripke Structures
. To reason about such systems, one standard approach is to provide a temporal semantic
for the structure. Properties of interest regarding concurrency can then be expressed using a temporal
logic formula. In this paper we consider the following problem: Given a Kripke structure,
determine for all pairs of states s and s
whether they are equivalent with respect to CTL
(i.e. s and s
model the same set of formulas in CTL
, a new logic, incorporates
the features of both Linear Temporal Logic and Branching Temporal Logic. In Logic CTL
the nexttime operator is discarded,...
Automatic Symbolic Verification of Embedded Systems
- Rajeev Alur,Thomas A. Henzinger,Pei-hsin Ho
. We present a model-checking procedure and its implementation for the automatic
verification of embedded systems. The system components are described as Hybrid
Automata---communicating machines with finite control and real-valued variables
that represent continuous environment parameters such as time, pressure, and temperature.
The system requirements are specified in a temporal logic with stop watches, and
verified by symbolic fixpoint computation. The verification procedure---implemented
in the Cornell Hybrid Technology Tool, HyTech---applies to hybrid automata whose
continuous dynamics is governed by linear constraints on the variables and their derivatives.
We illustrate the method and the tool by checking safety, liveness, time-bounded,
and duration requirements of digital controllers, schedulers, and distributed algorithms.
On Constructive Negation for Disjunctive Logic Programs
- Jorge Lobo
Answers for queries in logic programs, can be seen as formulas involving only equality
and inequality predicates. This representation permits the extension of proofprocedures
as SLDNF-resolution to handle non-ground negative queries. In this
paper, we extend these ideas to the class of disjunctive logic programs.
Keywords: Theory, Constructive Negation, Disjunctive programs.
Procedural interpretations for rules of negation in logic programming generally
have been confined to ground literals [2, 19]. The restriction is imposed
since answers for queries provided by these procedures are based solely on
substitutions and most general unifiers. However, recently a new approach
to the form of an answer, termed constructive negation , has permitted
A Matrix Characterization for MELL
- Christoph Kreitz
. We present a matrix characterization of logical validity in the
multiplicative fragment of linear logic with exponentials. In the process
we elaborate a methodology for proving matrix characterizations correct
and complete. Our characterization provides a foundation for matrixbased
proof search procedures for MELL as well as for procedures which
translate machine-found proofs back into the usual sequent calculus.
Linear logic  has become known as a very expressive formalism for reasoning
about action and change. During its rather rapid development linear logic has
found applications in logic programming [14,19], modeling concurrent computation
, planning , and other areas. Its expressiveness, however, results in
a high complexity. Propositional linear...
Neuronal Architectures for Pattern-theoretic Problems
- David Mumford
this paper is the proposition that the computational
analysis of vision -- and speech, tactile sensing, motor control, etc. -- (the theory
of the computation as Marr called it (Marr, 82)) has is reaching a point where
it can provide a clearer and deeper description of the essential tasks of vision
as well as a wide range of other cognitive tasks. For instance, the development
of algorithms for character recognition or for face recognition or for road
tracking from a moving vehicle (three problems which have been much studied
on account of their potential applications) forces the researcher to deal with
noisy, complex real world data. In doing...
Formal Reasoning about Actor Programs Using Temporal Logic
- Susanne Schacht
We here present an approach to reasoning about actor programs on the basis of temporal
logic. Temporal logic is particularly appropriate for the specification of concurrent programs,
but most known temporal logic proof systems for concurrent computations rely on imperative
language constructs, ignoring, e.g., the creation of processes and the dynamic configuration of
communication channels, which are crucial for actor based programming.
This work was supported by a grant from DFG under account Ha2097/1-3.
1 Temporal logic as a tool for specification and verification
Temporal logic is particularly appropriate for reasoning about programs for which a corresponding
statement in terms of their operational or denotational semantics is too...
Sequent Calculus and the Specification of Computation - Lecture Notes
- C Dale Miller
2 Overview and motivation 5
2.1 Roles for logic in the specific of computations . . . . . . . . . . . . . . . . . . 5
2.2 Desiderata for declarative programming . . . . . . . . . . . . . . . . . . . . . 6
2.3 Relating algorithm and logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
3 A First-Order Logics 8
3.1 Types and signatures . ....
Tabulated Resolution for Well Founded Semantics
- Roland Bol,Lars Degerstedt
Based on the search forest for positive programs as defined by Bol and
Degerstedt, we define a tabulated version of SLS-resolution that is sound
and complete w.r.t. well founded semantics. In contrast to SLS-resolution
as proposed by Przymusinski and by Ross, a positivistic computation rule is
not required. This proposal is closely related to that of Chen and Warren,
but it relies on tabulation for both positive and negative recursion. In this
way, only one forest needs to be constructed, rather than a forest for each
negative context. For function-free programs, the resulting search forest is
Keywords: logic programming, deductive databases, well founded
semantics, tabulation, search forest, SLS-resolution,