Acceptable Programs Revisited
- Pascal Hitzler,Anthony Karel Seda
Acceptable logic programs have been studied extensively in the context of proving
termination of Prolog programs. It is difficult, however, to establish acceptability
from the definition since this depends on finding a suitable model, which need not
be a Herbrand model in general, together with a suitable level mapping that one
can use to check the conditions which characterize acceptability. In this paper, we
will see that when working over a fixed but arbitrary preinterpretation, a method
can be provided for obtaining both a suitable model and a canonical level mapping
which are sufficient for this purpose. Furthermore, the canonical model and level
mapping obtained will turn out...
A Semantic Model of Types and Machine Instructions for Proof-Carrying Code
- Amy P. Felty
Proof-carrying code is a framework for proving the safety of machine-language programs with a machinecheckable proof. Such proofs have previously defined type-checking rules as part of the logic. We show a universal type framework for proof-carrying code that will allow a code producer to choose a programming language, prove the type rules for that language as lemmas in higher-order logic, then use those lemmas to prove the safety of a particular program. We show how to handle traversal, allocation, and initialization of values in a wide variety of types, including functions, records, unions, existentials, and covariant recursive types.
The Design and Evaluation of an Asynchronous Microprocessor
- S. B. Furber,P. Day,J. D. Garside,N. C. Paver,S. Temple,J. V. Woods
AMULET1 is a fully asynchronous implementation of the ARM microprocessor which was designed at Manchester University between 1991 and 1993. First silicon arrived in April 1994 and was found to be functional, demonstrating that asynchronous design of complex circuits is feasible with present day CAD tools. This paper presents the motivation for the work, some of the design choices which were made, the problems which were encountered during the development of the design and the characteristics of the device itself. The future potential for asynchronous circuits is also discussed. 1: Introduction The growth in demand for high performance portable computing...
- Research Report,Thomas Eiter,Georg Gottlob,Yuri Gurevich
. Existential second-order logic (ESO) and monadic second-order logic (MSO) have attracted
much interest in logic and computer science. ESO is a much more expressive logic over word
structures than MSO. However, little was known about the relationship between MSO and syntactic
fragments of ESO. We shed light on this issue by completely characterizing this relationship for the
prefix classes of ESO over strings, (i.e., finite word structures). Moreover, we determine the complexity
of model checking over strings, for all ESO-prefix classes. Let ESO(Q) denote the prefix
class containing all sentences of the shape 9RQ' where R is a list of predicate variables, Q is a
What Is A Skeptical Proof?
- Michael Thielscher
. We investigate the task of skeptically reasoning in extensionbased,
nonmonotonic logics by concentrating on general argumentation
theories. The restricted applicability of Dung's notion of skeptical provability
in his well-known argumentation framework is illustrated, and a
new approach based on the notion of a claim associated with each argument
is proposed. We provide a formal definition of a skeptical proof
in our framework. As a concrete formalism, default logic in case of normal
default theories is embedded in the general framework. We prove a
formal correspondence between the two notions of skeptical provability,
which enables us to adopt the general concept of a skeptical proof into
clp(B): Combining Simplicity and Efficiency in Boolean Constraint Solving
- Daniel Diaz
. We present the design and the implementation of clp(B): a
boolean constraint solver in the Constraint Logic Programming paradigm.
This solver is based on local propagation methods and follows the "glassbox
" approach of compiling high-level constraints into primitive low-level
ones. We detail its integration into the WAM showing that the necessary
extension is truly minimal since only four new instructions are added.
The resulting solver is around an order of magnitude faster than other
existing boolean solvers.
Constraint Logic Programming (CLP) combines both the declarativity of Logic
Programming and the ability to reason and compute with partial information
(constraints) on specific domains, thus opening up a wide...
Quantitative Disjunctive Logic Programming: Semantics and Computation
- Cristinel Mateis
this paper are given in
Type Inference with Constrained Types
- Martin Odersky,Martin Wehr
this paper we present a general
framework HM(X) for Hindley/Milner style type systems
with constraints, analogous to the CLP(X) framework
in constraint logic programming [JM94]. Particular
type systems can be obtained by instantiating the
parameter X to a specific constraint system. The Hindley
/Milner system itself is obtained by instantiating X
to the standard Herbrand constraint system.
Handling Preferences in Negotiation Dialogue Frames
- Aspassia Daskalopulu,Chris Reed
. Complex argumentation-based interaction can be characterised by a
rich model of inter-agent communication based upon the construct of a dialogue
frame. This approach is shown to have computational benefits and can be easily
extended to include models of agents' preferences. The process of negotiation is
founded upon the notion of compromise and this comes about as a result of agents'
preferences: an agent may be willing to make concessions if in so doing, preferred
states of affairs obtain. This paper explores a formal approach to representing such
preference criteria, and the means by which evaluation of potential contracts can be
carried out. The resulting system supports sophisticated...
rd. International Conference on Fuzzy Logic, Neural Nets and Soft Computing (IIZUKA'94), pp. 651-652, Iizuka - Japan, August 1-7, 1994.
- C. J. Jimnez,A. Barriga,S. Snchez Solano
.-- A classification of inference systems based
on approximate reasoning techniques is proposed. An
alternative realization method is described for the
particular SISC case, which enables reducing the silicon
area and increasing the operation speed, making
it especially appropriate for real time control applications.
Fuzzy logic provides a conceptual and mathematical
frame for those problems where the imprecise definition
of variables and vague resolution strategies
applied require the use of approximate reasoning techniques.
This has led to the development of new processing
structures which allow hardware implementations
of fuzzy inference mechanisms .
Distinct taxonomies can be established for fuzzy
inference systems according to different criteria. However,
in order to compare their hardware realizations, it
How to Normalize the Jay
- Dieter Probst,Thomas Studer
In this note we give an elementary proof of the strong normalization property
of the J combinator in combinatory logic by providing an explicit bound for
the maximal length of the reduction path of a term.
The combinators I and J with their reduction rules Ia#a and Jabcd#ab(adc) were
introduced by Rosser  in 1935. These two combinators are of particular interest
since together they form a basis for the #I-calculus (cf. e.g. Barendregt ).
In combinatory logic, it is natural to ask whether a certain system is strongly normalizing,
i.e. whether there does not exist a term with an infinite reduction path.
Most standard combinators such...
Goals, Desires, Utilities and Preferences
- Leendert W. N,Torre E. Weydert
. In this paper we study the logic of goals, which
are formalized as desires with an utilitarian semantics. In our
framework goals have a dual character, because they are constraints
on utility functions as well as constructors of these
utility functions. The non-monotonic reasoning related to the
constructors reflects that goals are used as heuristic approximations
of preferences in decision making and planning. Moreover,
our framework is based on bipolar additive preferences,
where bipolarity means that goals can either result in a gain
of utility if achieved, or a loss of utility if not achieved. The
framework is used to illustrate different types of contextdependence
and conflicts of goals.
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...
A Semantics for Evaluation Logic (Extended Version)
- Eugenio Moggi
This paper proposes an internal semantics for the modalities and evaluation predicate of Pitts'
Evaluation Logic, and introduces several predicate calculi (ranging from Horn sequents to Higher
Order Logic), which are sound and complete w.r.t. natural classes of models. It is shown (by examples)
that many computational monads satisfy the additional properties required by the proposed semantics.
Evaluation logic EL T is a typed predicate logic (see [CP92, Pit91]) based on the metalanguage for
computational monads ML T (a typed calculus introduced in [Mog91]), which permits statements
about the evaluation of programs to values by the use of evaluation modalities. In particular, EL T
might be used...
Logic Program Transformation through Generalization Schemata
- Pierre Flener,Yves Deville
In program synthesis, program transformation can be done on the fly, based on information generated and exploited
during the program construction process. For instance, some logic program generalization techniques
can be pre-compiled at the logic program schema level, yielding transformation schemata that give rise to
elimination of the eureka discovery, full automation of the transformation process itself, and even the prediction
whether and which optimizations will be achieved.
Programs can be classified according to their construction methodologies, such as divide-and-conquer, generate
-and-test, top-down decomposition, global search, and so on, or any composition thereof. Informally,
a program schema is a template program with a fixed control and...
Plugging Data Constructs into Paradigm-Specific Languages: towards an Application to UML
- Egidio Astesiano,Maura Cerioli,Gianna Reggio
. We are interested in the composition of languages, in particular
a data description language and a paradigm-specific language,
from a pragmatic point of view. Roughly speaking our goal is the description
of languages in a component-based style, focussing on the data
definition component. The proposed approach is to substitute the constructs
dealing with data from the "data" language for the constructs
describing data that are not specific to the particular paradigm of the
"paradigm-specific" language in a way that syntax, semantics as well as
methodologies of the two components are preserved.
We illustrate our proposal on a toy example: using the algebraic specification
language Casl, as data language, and...
Coalgebras and Modal Logic
- Martin Roiger
Coalgebras are of growing importance in theoretical
computer science. To develop languages for them is significant
for the specification and verification of systems modelled
with them. Modal logic has proved to be suitable
for this purpose. So far, most approaches have presented
a language to describe only deterministic coalgebras. The
present paper introduces a generalization that also covers
non-deterministic systems. As a special case, we obtain the
"usual" modal logic for Kripke-structures. Models for our
modal language L
are F-coalgebras where the functor F is
inductively constructed from constant sets and the identity
functor using product, coproduct, exponentiation, and the
power set functor. We define a language L
and show that
it embeds into L
Modularity in Lambda Calculus
- Antonino Salibra
The variety (equational class) of lambda abstraction algebras was introduced to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order predicate logic. In this paper a proof is given that the variety of lambda abstraction algebras is not congruence modular. Some simple applications of this result to lambda calculus are also obtained.
Context Adaptation in Fuzzy Processing
- Ricardo R. Gudwin,Fernando A. C. Gomide
: This paper deals with the
influence of the context in fuzzy rule base
systems. The linguistic variable definition of
Zadeh is modified to permit context
adaptation, and inference procedure is
modified to handle context adaptation when
evaluating fuzzy concepts. Procedures to
determine context in different situations are
provided. Context determination may be
viewed as a kind of learning. An application
example concerning supervisory control of
group of elevators is also considered.
A linguistic variable is a variable that assigns
as its values linguistic labels, which are mapped
onto the real world by a fuzzy set. A great
problem which comprises this definition is the
difficulty to fine tune membership functions,
which is actually one of...
Executable Temporal Logic for Distributed A.I.
- Michael Fisher,Michael Wooldridge
This paper describes Concurrent METATEM, a programming language based on temporal logic, and
applies it to the study of Distributed Artificial Intelligence (DAI). A Concurrent METATEM system
consists of a number of asynchronously executing objects, which are able to communicate through
broadcast message-passing. Each individual object directly executes a specification of its desired
behaviour. Such specifications are given using a set of temporal logic `rules', determining how the
object may generate `commitments', which it subsequently attempts to satisfy.
This language provides a novel and powerful approach to representing DAI systems, where
individual `agents' are specified in a natural way using temporal logic, while groups of agents