301.
Towards a Logic for Reasoning about Logic Programs Transformation
- Alberto Momigliano
We give a proof-theoretic analysis of logic programs transformations,
viewed as operations on proof trees in the sense of [3, 4, 9, 10].
We present a logic for reasoning about (equivalence preserving) transformations
of logic programs. Our main tool is the usage of inference rules;
the target program may be obtained as a set of clause introduction proofs
with axioms from the source program. The rules are admissible, that is
every proof according to the latter can be translated back in a derivation
of the same consequence built from the source program without those
rules. In this formal setting, we give a general schema for program transformation
analysis, which...
302.
A Combination of Interval Logic and Linear Temporal Logic
The super-dense computation model provides an abstraction of real-time behaviour of computing systems.
Logics to deal with this model are being studied. In the paper, we propose a combination of a linear
temporal logic and an interval logic, and demonstrate how this combination can be used to specify a
real-time semantics of an OCCAM-like programming language and its real-time properties, where the
super-dense computation model is adopted.
303.
Full Dynamic Plural Logic
- Martin Van Den Berg
this paper was sent to
the proceedings of the fourth Hungarian symposium
of logic and language.
The main change is that formulas are now consequently
written as infix relations. This made
some textual changes necessary. Also some typing
and stylistic errors have been corrected.
Full Dynamic Plural Logic
Martin van den Berg
Department of Computational Linguistics
Faculty of Arts, University of Amsterdam
vdberg@alf.let.uva.nl
304.
Dynamic Predicate Logic
- Jeroen Groenendijk,Martin Stokhof
This paper is devoted to the formulation and investigation of a dynamic semantic
interpretation of the language of first-order predicate logic. The resulting
system, which will be referred to as `dynamic predicate logic', is intended as
a first step towards a compositional, non-representational theory of discourse
semantics.
305.
Dynamic Predicate Logic
- Jeroen Groenendijk,Martin Stokhof
This paper is devoted to the formulation and investigation of a dynamic semantic
interpretation of the language of first-order predicate logic. The resulting
system, which will be referred to as `dynamic predicate logic', is intended as
a first step towards a compositional, non-representational theory of discourse
semantics.
306.
On Urquhart's C Logic
- Agata Ciabattoni
In this paper we investigate the basic many-valued logics
introduced by Urquhart in [15] and [16], here referred
to as C and Cnew , respectively. We define a cut-free hypersequent
calculus for Cnew and show the following results:
(1) C and Cnew are distinct versions of G odel logic without
contraction. (2) Cnew is decidable. (3) In Cnew the family
of axioms ((A
k
! C) ^ (B
k
! C)) ! ((A _ B)
k
! C),
with k 2, is in fact redundant.
1 Introduction
The logic C was introduced by Urquhart in the chapter
devoted to many-valued logic of the Handbook of Philosophical
Logic [15].
C turns out to be a basic many-valued logic being...
307.
Success of Default Logic
- Vladimir Lifschitz
Ray Reiter's Logic for Default Reasoning was published
almost twenty years ago, but it is widely used today by
researchers in knowledge representation, commonsense reasoning
and logic programming. This note is a collection of random
comments on aspects of this success story.
308.
Cell-Based Logic Optimization
- Giovanni De Micheli
This chapter surveys techniques for library binding in semicustom technologies.
Library binding is the back-end of logic synthesis, and constructs an interconnection
of cell instances from a given library, starting from a multi-level logic
network. Emphasis is placed on the algorithmic approach to library binding, with
particular reference to covering and matching techniques.
309.
Automata, Logic, and XML
- Frank Neven
We survey some recent developments in the broad area of
automata and logic which are motivated by the advent of XML. In particular,
we consider unranked tree automata, tree-walking automata, and
automata over infinite alphabets. We focus on their connection with logic
and on questions imposed by XML.
310.
A Logic Programming Language
- Stefania Costantini,Arianna Tocchio
This paper presents a new logic programming language for
modelling Agents and Multi-Agent systems in computational logic. The
basic objective of the specification of this new language has been the
identification and the formalization of what we consider to be the basic
patterns for reactivity, proactivity, internal "thinking", and "memory".
311.
Cell-Based Logic Optimization
- Giovanni De Micheli
This chapter surveys techniques for library binding in semicustom technologies.
Library binding is the back-end of logic synthesis, and constructs an interconnection
of cell instances from a given library, starting from a multi-level logic
network. Emphasis is placed on the algorithmic approach to library binding, with
particular reference to covering and matching techniques.
312.
Pruning in Logic Programming
- Lee Naish
The logic programming community has a love--hate relationship with operators for
pruning the search space of logic programs such as cut, commit, once, conditionals and
variations on these. Pruning operators typically are not declarative, result in incompleteness
and/or unsoundness, decrease readability and flexibility of code and make
program analysis and transformation more difficult. Despite this, nearly all non-trivial
Prolog programs contain cuts, nearly all more recent logic programming languages have
similar pruning operators and many languages insist on pruning operators in every
clause. In practice, logic programming is less logical than functional programming.
Why it this so? Do we really need pruning operators? Can we have sufficiently
powerful pruning...
313.
Fuzzy Logic and Probability
- Francesc Esteva
In this paper we deal with a new approach
to probabilistic reasoning in a logical framework.
Nearly almost all logics of probability
that have been proposed in the literature
are based on classical two-valued logic.
After making clear the differences between
fuzzy logic and probability theory, here we
propose a fuzzy logic of probability for which
completeness results (in a probabilistic sense)
are provided. The main idea behind this
approach is that probability values of crisp
propositions can be understood as truthvalues
of some suitable fuzzy propositions associated
to the crisp ones. Moreover, suggestions
and examples of how to extend the
formalism to cope with conditional probabilities
and with other uncertainty formalisms
are also provided.
1 Introduction
Discussions about...
314.
Pruning in Logic Programming
- Lee Naish
The logic programming community has a love--hate relationship with operators for
pruning the search space of logic programs such as cut, commit, once, conditionals and
variations on these. Pruning operators typically are not declarative, result in incompleteness
and/or unsoundness, decrease readability and flexibility of code and make
program analysis and transformation more difficult. Despite this, nearly all non-trivial
Prolog programs contain cuts, nearly all more recent logic programming languages have
similar pruning operators and many languages insist on pruning operators in every
clause. In practice, logic programming is less logical than functional programming.
Why it this so? Do we really need pruning operators? Can we have sufficiently
powerful pruning...
315.
Multi-Valued Autoepistemic Logic
- Robert F. Stark
We generalize Moore's autoepistemic logic to multi-valued autoepistemic logic,
where the set of truth-values can be any complete lattice. Multi-valued autoepistemic
extensions can be characterized by admissible belief interpretations which are
the concrete approximations of extensions and are appropriate to be computed and
manipulated. We prove that multi-valued autoepistemic extensions are exactly the
theories of maximal multi-valued Kripke models. The class of stratified theories is
investigated and it is shown that stratified theories have exactly one multi-valued
autoepistemic extension. Finally we present a sequent calculus for multi-valued
logic which serves as a tool for a decision procedure for multi-valued autoepistemic
logic.
1 Introduction
Autoepistemic logic was introduced by Moore [10] in...
316.
Multi-Agent VSK Logic
- Michael Wooldridge
We present a formalism for reasoning about the information properties of multi-agent systems. Multi-agent VSK logic allows us to represent what is objectively true of some environment, what is visible, or accessible of the environment to individual agents, what these agents actually perceive, and finally, what the agents actually know about the environment. The semantics of the logic are given in terms of a general model of multi-agent systems, closely related to the interpreted systems of epistemic logic. After introducing the logic and establishing its relationship to the formal model of multi-agent systems, we systematically investigate a number of possible...
317.
Observational Logic
- R. Hennicker,M. Bidoit,Rolf Hennicker,Michel Bidoit
. We present an institution of observational logic which generalizes earlier approaches to
observational systems specification in various ways. First, we introduce a notion of an observational
signature which incorporates the declaration of a distinguished set of observers. Then, we define
observational algebras whose operations are required to be compatible with the indistinguishability relation
determined by the observers of an observational signature. In particular, we introduce a homomorphism
concept for observational algebras which adequately expresses observational relationships between algebras.
Then we consider a flexible notion of observational signature morphism which guarantees the satisfaction
condition of institutions w.r.t. observational satisfaction for arbitrary first-order sentences.
From the proof theoretical point...
318.
Geometric Logic in Computer Science
- Steve Vickers
We present an introduction to geometric logic and the mathematical structures
associated with it, such as categorical logic and toposes. We also describe some
of its applications in computer science including its potential as a logic for specification
languages.
319.
HOLCF: Higher Order Logic of
- Franz Regensburger
This paper presents a survey of HOLCF, a higher order logic
of computable functions. The logic HOLCF is based on HOLC, a variant
of the well known higher order logic HOL, which offers the additional
concept of type classes.
320.
A Visual Syntax for Logic and Logic Programming
- Jaume Agust I,Jordi Puigsegur
It is commonly accepted that non-logicians have difficulty in expressing themselves
in first order logic. Part of the visual language community is concerned
with providing visual notations which use visual cues ("declarative diagrams")
to make the structuring of logical expressions more intuitive. One of the more
successful metaphors used in such diagrammatic languages is that of set inclusion,
making use of the graphical intuitions which most of us are taught at
school. Existing declarative diagrammatic languages do not make full use of
such set-based intuitions. We present a more uniform use of sets which allow
simple but highly expressive diagrams to be constructed from a small number
of primitive...
