Minimal Logic Re-Synthesis For Engineering Change
- Gitanjali Swamy,Sriram Rajamani,Chris Lennard,Robert K. Brayton
Logic synthesis refers to the process of optimizing a logic description
of a circuit, given as a net-list of logic (boolean) gates
. This representation can be optimized for area(minimum), delay
(minimum or meeting requirements), and power(minimum).
Since these problems are hard to solve exactly, heuristic algorithms
are generally used. However, these algorithms are unstable;
if a small change is made in the network function, the output of
the synthesis algorithm may vary greatly from the previous implementation.
A designer can invest effort in optimizing the original
design by hand, so it is desirable that most of the hand-designed
or optimal parts be preserved, even when changes are made to...
Compiler-Directed Early Load-Address Generation
- Ben-chung Cheng,Daniel A. Connors,Wen-mei W. Hwu
Two orthogonal hardware techniques, table-based address
prediction and early address calculation, for reducing
the latency of load instructions have been recently
proposed. The key idea behind both of these
techniques is to speculatively perform loads early in
the processor pipeline using predicted values for the
loads' addresses. These techniques have required either
a large hardware table or complex register bypass
logic to be implemented in order to accurately predict
the important loads in the presence of a large number of
less-important loads. This paper proposes a compilerdirected
approach that allows a streamlined version of
both of these techniques to be effectively used together.
The compiler provides directives to indicate which prediction
mechanism to use...
Empirical Evaluation of the CRAY-T3D: A Compiler Perspective
- Remzi H. Arpaci,David E. Culler,Arvind Krishnamurthy,Steve G. Steinberg,Katherine Yelick
Most recent MPP systems employ a fast microprocessor surrounded by a shell of communication and synchronization logic. The CRAY-T3D 1 provides an elaborate shell to support global-memory access, prefetch, atomic operations, barriers, and block transfers. We provide a detailed empirical performance characterization of these primitives using micro-benchmarks and evaluate their utility in compiling for a parallel language. We have found that the raw performance of the machine is quite impressive and the most effective forms of communication are prefetch and write. Other shell provisions, such as the bulk transfer engine and the external Annex register set, are cumbersome and of...
Programming and Interface Specification Language of JIVE - Specification and Design Rationale
- Peter Muller,Jorg Meyer,Arnd Poetzsch-heffter,Fachbereich Informatik,Fernuniversitat Hagen
This report describes the programming and interface specification language of the Java
Interactive Verification Environment Jive. The Jive system is a prototype implementation
of a logic-based programming-environment for an object-oriented programming language.
Logic-based programming-environments are language-dependent software development tools
that support formal specification and verification.
We summarize the properties of an ideal programming language for the prototype and
argue that Java is a good candidate. The design of the supported Java subset is discussed
and a formal definition of the abstract syntax is presented.
Program specifications are denoted in an interface specification language. This report
discusses the design of the Jive interface specification language and presents its abstract
- Henry Prakken,Marek Sergot
We investigate under what conditions contrary-to-duty (CTD) structures lacking
temporal and action elements can be given a coherent reading. We argue, contrary
to some recent proposals, that CTD is not an instance of defeasible reasoning, and
that methods of nonmonotonic logics are inadequate since they are unable to distinguish
between defeasibility and violation of primary obligations. We propose
a semantic framework based on the idea that primary and CTD obligations are
obligations of different kinds: a CTD obligation pertains to, or pre-supposes, a
certain context in which a primary obligation is already violated. This framework
is presented initially as an extension of Standard Deontic Logic (SDL), a normal
Application Of Esop Minimization In Machine Learning And Knowledge Discovery
- Marek A. Perkowski Tim Ross,Dave Gadd,Jeffrey A. Goldman,Ning Song
This paper presents a new application
of an Exclusive-Sum-Of-Products (ESOP) minimizer
EXORCISM-MV-2: to Machine Learning, and particularly,
in Pattern Theory. An analysis of various
logic synthesis programs has been conducted at
Wright Laboratory for machine learning applications.
Creating a robust and efficient Boolean minimizer
for machine learning that would minimize a decomposed
function cardinality (DFC) measure of functions
would help to solve practical problems in application
areas that are of interest to the Pattern Theory Group
- especially those problems that require strongly unspecified
multiple-valued-input functions with a large
number of variables. For many functions, the complexity
minimization of EXORCISM-MV-2 is better
than that of Espresso. For small functions, they are
worse than those of the...
Fixpoint 3-Valued Semantics for Autoepistemic Logic
- Marc Denecker,Victor Marek
The paper presents a constructive 3-valued semantics
for autoepistemic logic (AEL). We introduce
a derivation operator and define the semantics
as its least fixpoint. The semantics is
3-valued in the sense that, for some formulas,
the least fixpoint does not specify whether they
are believed or not. We show that complete fixpoints
of the derivation operator correspond to
Moore's stable expansions. In the case of modal
representations of logic programs our least fixpoint
semantics expresses well-founded semantics
or 3-valued Fitting-Kunen semantics (depending
on the embedding used). We show that, computationally,
our semantics is simpler than the semantics
proposed by Moore (assuming that the
polynomial hierarchy does not collapse).
We describe a 3-valued semantics for modal theories
Permissive Subsorted Partial Logic in CASL
- Maura Cerioli,Anne Haxthausen
. This paper presents a permissive subsorted partial logic used
in the CoFI Algebraic Specification Language. In contrast to other ordersorted
logics, subsorting is not modeled by set inclusions, but by injective
embeddings allowing for more general models in which subtypes can
have different data type representations. Furthermore, there are no restrictions
like monotonicity, regularity or local filtration on signatures at
all. Instead, the use of overloaded functions and predicates in formulae
is required to be sufficiently disambiguated, such that all parses have the
same semantics. An overload resolution algorithm is sketched.
During the past decades a large number of algebraic specification languages have
been developed. The presence of...
Ambiguity and the Principle of Idiosyncratic Interpretation
- Kees Van Deemter
This paper discusses logics whose premisses and/or conclusions can contain ambiguous material. Two different kinds of applications
are sketched for these logics. First, the paper discusses how logics with ambiguous expressions can shed light on
the way in which human hearers or readers understand certain `paradoxical' logical arguments, in which crucial use is made
of ambiguous material. Second, the paper uses practical (i.e., computational) applications to show how a logic of ambiguous
expressions can be used to avoid interpretational deadlock in such systems. Here a key role is played by the Principle of Idiosyncratic
Interpretation, which states that, in a given context of occurrence, different...
A Uniform Framework for Concept Definitions in Description Logics
- Maurizio Lenzerini
Most modern formalisms used in Databases and Artificial Intelligence for describing an
application domain are based on the notions of class (or concept) and relationship among
classes. One interesting feature of such formalisms is the possibility of defining a class,
i.e., providing a set of properties that precisely characterize the instances of the class.
Many recent articles point out that there are several ways of assigning a meaning to a
class definition containing some sort of recursion. In this paper, we argue that, instead of
choosing a single style of semantics, we achieve better results by adopting a formalism that
allows for different semantics to coexist. We...
Logic Programming with Constructor-based Type Constraints
- Hans-joachim Goltz
A concept of types and type sorts for logic programming is introduced, where types and type
sorts are regarded as constraints. Instead of defining "well-sorted" terms and substitutions, type
constraints and type sort constraints are defined. The approach is based on term models. A type is
interpreted as a set of object terms and a type sort is interpreted as a set of types. Parameters of
types can be object variables, object terms, and type variables. Types are defined by means of type
rules which can be regarded as rules for the generation of the elements belonging to the corresponding
type. The definitions of types and...
Correct-schema-guided Synthesis of Steadfast Programs
- Pierre Flener,Kung-kiu Lau,Mario Ornaghi
It can be argued that for (semi-)automated software development,
program schemas are indispensable, since they
capture not only structured program design principles, but
also domain knowledge, both of which are of crucial importance
for hierarchical program synthesis. Most researchers
represent schemas purely syntactically (as higher-order expressions)
. This means that the knowledge captured by a
schema is not formalised. We take a semantic approach and
show that a schema can be formalised as an open (firstorder)
logical theory that contains an open logic program.
By using a special kind of correctness for open programs,
called steadfastness, we can define and reason about the
correctness of schemas. We also show how to use...
A New Continuous Propositional Logic
- Riccardo Poli,Mark Ryan,Aaron Sloman
In this paper we present Minimal Polynomial Logic (MPL), a generalisation
of classical propositional logic which allows truth values in the
continuous interval [0; 1] and in which propositions are represented by
multi-variate polynomials with integer coefficients.
The truth values in MPL are suited to represent the probability of an
assertion being true, as in Nilsson's Probabilistic Logic, but can also be
interpreted as the degree of truth of that assertion, as in Fuzzy Logic.
However, unlike fuzzy logic MPL respects all logical equivalences, and unlike
probabilistic logic it does not require explicit manipulation of possible
In the paper we describe the derivation and the properties of this
Equational Reasoning with 2-dimensional Diagrams
- Yves Lafont
The significance of the 2-dimensional calculus, which goes back to Penrose, has already been pointed
out by Joyal and Street. Independently, Burroni has introduced a general notion of n-dimensional
presentation and he has shown that the equational logic of terms is a special case of 2-dimensional
Here, we propose a combinatorial definition of 2-dimensional diagrams and a simple method
for proving that certain monoidal categories are finitely 2-presentable. In particular, we consider
Burroni's presentation of finite maps and we extend it to the case of finite relations.
This paper should serve as a reference for our future work on symbolic computation, including a
theory of 2-dimensional rewriting...
1st Order Logic Formal Concept Analysis: from logic programming to theory
- Vol Nr,Laurent Chaudron,Nicolas Maille
In this paper, we analyze and define the introduction of 1st order
logic in Formal Concept Analysis (FCA); the aims are both
theoretical (as a complete model is needed) and applied (so as
to improve expression power of FCA as a knowledge mining tool
and the relevance of its results).
Our contribution consists in: i) the implementation of classical
FCA in logic programming and the analysis of real cases,
ii) the design of a complete 1st order FCA model, iii) the implementation
of this 1st order FCA.
Keywords: Formal Concept Analysis, Knowledge Representation,
Concepts Discovery, Rule induction, Logic Programming.
Authors' affiliation and address:
2 avenue Edouard Belin
F-31055 Toulouse Cedex 04...
A Linear Logic View of Gamma Style Computations as Proof Searches
- Paola Bruscoli,Alessio Guglielmi
Using the methodology of abstract logic programming in linear
logic, we establish a correct and complete translation between the language
Nabla and first order linear logic. Nabla is a modification of the coordination
language Gamma with parallel and sequential composition. Nabla,
without modifying Gamma basic computational model, is amenable to this
kind of analysis, at the price of a weaker expressive power. The translation
is correct and complete in the sense that we establish a two way correspondence
between computations in Nabla and the search for proofs in a
suitable fragment of first order linear logic. Moreover, the translation is not
an encoding, meaning that to the algebraic structure...
A Theory of Nonmonotonic Inheritance Based on Annotated Logic
- Krishnaprasad Thirunarayan,Michael Kifer
We propose a logical language for representing networks with nonmonotonic multiple
inheritance. The language is based on a variant of annotated logic studied in [5, 6,
17, 18, 19, 20, 21]. The use of annotated logic provides a rich setting that allows to
disambiguate networks whose topology does not provide enough information to decide
how properties are to be inherited. The proposed formalism handles inheritance via
strict as well as defeasible links. We provide a formal account of the language, describe
its semantics, and show how a unique intended model can be associated with every
inheritance specification written in the language. Finally, we present an algorithm
Tunable Formalism In Object-Oriented Systems Analysis: Meeting The Needs Of Both Theoreticians And Practitioners
- Stephen W. Clyde,David W. Embley,Scott N. Woodfield
This work has been partially supported by HewlettPackard
through graduate fellowships and equipment
Object-oriented Systems Analysis (OSA)
 meets the needs of both theoreticians and
practitioners by providing tunable formalism. In
this paper, we show how an OSA user's use of
formalism can be tuned from completely
informal to completely formal. We give OSA's
underlying formal definition that makes this
possible as a two-step process involving a
temporal, first-order logic language, and a
mathematical interpretation. We also show how
the formal definition provides answers to
fundamental, practical questions related to
object-oriented software development. Finally,
we show how OSA allows varying levels of
abstraction and completion so that engineers,
tool builders, and researchers can tune the
formalism to suit...
Desiderata for Interactive Verification Systems DRAFT
- Konrad Slind,Christian Prehofer
What facilities should an interactive verification system provide? We take the
pragmatic view that the particular logic underlying a proof system is not as important
as the support that is provided. Although a plethora of logics have been
implemented, we think that there is a common kernel of support that a proof system
ought to provide. Towards this end, we give detailed suggestions for verification
support in three major areas: formalization, proof, and interface. Although our
perspective comes from experience with highly expressive logics such as set theory,
higher order logic, and type theory, we think our analyses apply more generally.
Currently, theorem provers are used in the...
Logic Is Not Enough: Why Reasoning About Another Person's Beliefs Is Reasoning Under Uncertainty
- Anthony Jameson
A system that reasons about the beliefs of a person must in general be able to ascribe
a good deal of general background knowledge to that person, often in the absence of
reliable evidence that the person possesses that knowledge. In some cases it is possible
to make the necessary inferences within a logical framework, often as default inferences,
using as premises information about the person's membership in some group
or information about the system's own knowledge. But these approaches do not in
general adequately deal with the uncertainty that pervades the ascription of general
background knowledge. An explicitly probabilistic framework, intuitive psychometrics,
was developed to provide a...