
561.
A Relational Model for Temporal Logic
We use Tarski's relational calculus to construct a model of linear temporal logic. Both discrete and
dense time are covered and we obtain denotational domains for a large variety of reactive systems.
Keywords : Relational algebra, reactive systems, temporal algebra, temporal logic.
1

562.
Predicate Logic with Definitions
- Makarov, Victor
Predicate Logic with Definitions (PLD or D-logic) is a modification of
first-order logic intended mostly for practical formalization of mathematics.
The main syntactic constructs of D-logic are terms, formulas and definitions. A
definition is a definition of variables, a definition of constants, or a
composite definition (D-logic has also abbreviation definitions called
abbreviations). Definitions can be used inside terms and formulas. This
possibility alleviates introducing new quantifier-like names. Composite
definitions allow constructing new definitions from existing ones.

563.
Nondeterministic Linear Logic
- Matsuoka, Satoshi
In this paper, we introduce Linear Logic with a nondeterministic facility,
which has a self-dual additive connective. In the system the proof net
technology is available in a natural way. The important point is that
nondeterminism in the system is expressed by the process of normalization, not
by proof search. Moreover we can incorporate the system into Light Linear Logic
and Elementary Linear Logic developed by J.-Y.Girard recently: Nondeterministic
Light Linear Logic and Nondeterministic Elementary Linear Logic are defined in
a very natural way.

564.
Trakhtenbrot Theorem and Fuzzy Logic
Trakhtenbrot theorem is shown to be valid for the three main fuzzy logics - Lukasiewicz, Gödel and product logic.

565.
Calendar Logic
- Hans Jurgen Ohlbach,Dov Gabbay
A propositional temporal logic is introduced whose operators quantify over intervals of a reference time line. The intervals are specified symbolically, for example `next week's weekend'. The specification language for the intervals takes into account all the features of real calendar systems. A simple statement which can be expressed in this language is for example: `yesterday I worked for eight hours with one hour lunch break at noon'. Calendar Logic can be translated into propositional logic. Satisfiability is therefore decidable. Since the translation is exponential, a tableau decision procedure for checking decidability is presented as an alternative.

566.
Linguistic Grammarasdynamic Logic
- Johan Van Benthem
Natural language is the primary vehicle of human communication. It involves
a series of interlocked processes at various levels of aggregation. Proof
theory and dynamic logic provide two paradigms for dealing with this variety.
This paper gives an analysis of some main issues that arise in merging the
two viewpoints towards this broader goal. Topics discussed include: proof
as discourse, interfacing low-level fast and high-level slow systems, merging
lambda dynamics and modal state dynamics, strategies that create feasible
proof calculi. Overall prospects for broad 'dynamic architectures' look good.
to appear in
M. Abrusci & C. Casadio, eds.,
Proceedings Third Workshop on Logic and Language, Roma
2
1 Connecting Proof and Communication
The programmatic...

567.
A Fuzzy Description Logic
- Umberto Straccia
Description Logics (DLs, for short) allow reasoning
about individuals and concepts, i.e. set of individuals
with common properties. Typically, DLs are limited to
dealing with crisp, well defined concepts. That is, concepts
for which the problem whether an individual is
an instance of it is a yes/no question. More often than
not, the concepts encountered in the real world do not
have a precisely defined criteria of membership: we
may say that an individual is an instance of a concept
only to a certain degree, depending on the individual's
properties. Concepts of this kind are rather vague than
precise. As fuzzy logic directly deals with the notion of
vagueness and imprecision, it...

568.
A Fuzzy Description Logic
- Umberto Straccia
Description Logics (DLs, for short) allow reasoning
about individuals and concepts, i.e. set of individuals
with common properties. Typically, DLs are limited to
dealing with crisp, well defined concepts. That is, concepts
for which the problem whether an individual is
an instance of it is a yes/no question. More often than
not, the concepts encountered in the real world do not
have a precisely defined criteria of membership: we
may say that an individual is an instance of a concept
only to a certain degree, depending on the individual's
properties. Concepts of this kind are rather vague than
precise. As fuzzy logic directly deals with the notion of
vagueness and imprecision, it...

569.
Prioritized Autoepistemic Logic
- Jussi Rintanen
An important problem in data and knowledge representation is the possibility of default rules that conflict. If the application of both of two default rules leads to a contradiction, they cannot both be applied. Systems that support the use of default rules may either remain indifferent or prioritize one rule over the other. In this paper a prioritized version of autoepistemic logic is presented. Priorities determine a subset of all stable expansions of a set, the preferred stable expansions. The priority notion is declarative, unlike e.g. some recent approaches to priorities in default logic that modify the semi-constructive denition of...

570.
Constraint Logic Programming
- Francesca Rossi
. Constraint logic programming (CLP) is a multidisciplinary
research area which can be located between Artificial Intelligence, Operation
Research, and Programming Languages, and has to do with modeling,
solving, and programming real-life problems which can be described
as a set of statements (the constraints) which pose some relationship
between the problem's variables. This survey paper gives a brief introduction
to CLP, presents the state of the art in CLP research and applications,
points out some promising directions for future applications,
and discusses about how to cope with current research challenges.
1 Introduction and Main Concepts
In the last 10-15 years, Constraint Logic Programming (CLP) has evolved from
a basic research idea...

571.
Prioritizing Default Logic
- Gerhard Brewka
INTRODUCTION
In nonmonotonic reasoning conflicts among defaults are ubiquitous. For instance,
more specific rules may be in conflict with more general ones, a problem which has
been studied intensively in the context of inheritance networks (Poole,1985; Touretzky,
1986; Touretzky et al., 1991). When defaults are used for representing design goals in
configuration tasks conflicts naturally arise. The same is true in model based diagnosis
where defaults are used to represent the assumption that components typically are ok.
In legal reasoning conflicts among rules are very common (Prakken, 1993) and keep
many lawyers busy (and rich).
The standard nonmontonicformalisms handle such conflicts by generating multiple
belief sets. In default logic (Reiter,...

572.
A Stratification Test for Temporal Logic Programs
- Christos Nomikos; Panos Rondogiannis; Manolis Gergatsoulis
In this paper, we propose a new stratification test for linear-time temporal logic programs. More specifically, we extend the cycle-sum test [Ron01] to take into account negatively signed edges in the cycle-sum graph. In this way we broaden the class of temporal logic programs which are acceptable by the test. Moreover, we demonstrate that the cycle-sum test can be used to decide local statification for a broad class of temporal logic programs.

573.
A Strati cation Test for Temporal Logic Programs
- Christos Nomikos Y; Panos Rondogiannis; Manolis Gergatsoulis
In this paper, we propose a new strati cation test for linear-time temporal logic programs. More speci cally, we extend the cycle-sum test [Ron01] to take into account negatively signed edges in the cycle-sum graph. In this way we broaden the class of temporal logic programs which are acceptable by the test. Moreover, we demonstrate that the cycle-sum test can be used to decide local stati cation for a broad class of temporal logic programs.

574.
11TH NMR WORKSHOP 2.13 On the Computation of Warranted Arguments within a Possibilistic Logic Framework with Fuzzy Unification On the Computation of Warranted Arguments within a Possibilistic Logic Framework with Fuzzy Unification ∗
- Teresa Alsinet; Carlos Chesñevar; Lluís Godo; Sandra Sandri
Possibilistic Defeasible Logic Programming (P-DeLP) is a logic programming language which combines features from argumentation theory and logic programming, incorporating the treatment of possibilistic uncertainty at object-language level. The aim of this paper is twofold: first to present an approach towards extending P-DeLP in order to incorporate fuzzy constants and fuzzy unification, and after to propose a way to handle conflicting arguments in the context of the extended framework.

575.
THE APPLICATION OF FUZZY LOGIC TO THE CONSTRUCTION OF THE RANKING FUNCTION OF INFORMATION RETRIEVAL SYSTEMS
- N. O. Rouben
Information systems The quality of the ranking function is an important factor that determines the quality of the Information Retrieval system. Each document is assigned a score by the ranking function; the score indicates the likelihood of relevance of the document given a query. In the vector space model, the ranking function is defined by a mathematic expression such as: score ( q, d) = ∑ tf(t in d) * idf(t) * getBoost(t.field in d) * lengthNorm(t.field in d) * overlap(q,d) * queryNorm(q) t∈q We propose a fuzzy logic (FL) approach to defining the ranking function. FL provides a convenient...

576.
Logic Programming
- Agostino Dovier,Andrea Formisano,Alberto Policriti
T -resolution parametrically generalizes standard resolution with respect to
a first-order theory T (the parameter). The inherent power of its derivation
rule, however, makes it difficult to develop efficient unrestricted T -resolution
based systems. CLP (X ) parametrically extends Horn clause logic programming
with respect to a domain of computation X . The theory T underlying
the domain X is fixed a-priori and can not be modified (extended) by the
user.
In this paper we present the parametric logic programming language
T logic programming (TLP) which extends the CLP -scheme by giving the
possibility of acting on the theory T . The scheme is embedded into (linear)
T -resolution; however,...

577.
IOS Press Executing Suspended Logic Programs
- Robert A. Kowalski; Francesca Toni; Gerhard Wetzel; R. A. Kowalski; F. Toni; G. Wetzel; Executing Slp
Abstract. We present an extension of Logic Programming (LP) which, in addition to ordinary LP clauses, also includes integrity constraints, explicit representation of disjunction in the bodies of clauses and in goals, and suspension of atoms as in concurrent logic languages. The resulting framework aims to unify Constraint Logic Programming (CLP), Abductive Logic Programming (ALP) and Semantic Query Optimisation (SQO) in deductive databases. We present a proof procedure for the new framework, simplifying and generalising previously proposed proof procedures for ALP. We discuss applications of the framework, formulating traditional problems from LP, ALP, CLP and SQO.

578.
Taming First-Order Logic
- Szabolcs Mikul
In this paper we define computationally well-behaved versions of classical first-order logic and prove
that the validity problem is decidable
1
.
Keywords: first-order logic, decidability, relativization, mosaic, polyadic and counting quantifiers.
1 Taming
In [5], we developed a strategy for taming logics. The idea of taming can be described
as follows. Let us assume that we have a well-investigated logic with some undesirable
metalogical properties. An example is the incompleteness and undecidability of the
finite variable fragment of classical first-order logic, FOL, with at least three variables,
cf. [4] 4.1.3 and 4.2.18 for the equivalent algebraic results. Taming a logic amounts to
finding a version of the logic such that...

579.
Deciding Provability of Linear Logic
Introduction
There are many interesting fragments of linear logic worthy of study in their
own right, most described by the connectives which they employ. Full linear
logic includes all the logical connectives, which come in three dual pairs: the
exponentials ! and ?, the additives & and Phi, and the
multiplicativesOmega
. . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ....

580.
Programming by Logic and Logic by Programming (Extended Abstract)
)
Paul J. Voda, J'an Komara
Institute of Informatics, Comenius University Bratislava,
Mlynsk'a dolina, 842 43 Bratislava, Slovakia.
Email: voda@fmph.uniba.sk, komara@fmph.uniba.sk
Abstract: This paper is an extended abstract of parts I and II of a monograph with the same title
being prepared by the authors. Logic was developed before the arrival of computers and
it can be presented without reference to them. The main idea of the monograph is to
stress the mutual links between logic and computer programming by taking those parts of
logic which deal with computability and finitary logic (proof theory) and presenting them
by employing the techniques of computer programming. The techniques involve the use
of a...