461.
Linear, Branching Time and Joint Closure Semantics for Temporal Logic
- Joeri Engelfriet; Jan Treur
Temporal logic can be used to describe processes: their behaviour is characterized by a set of temporal models axiomatized by a temporal theory. Two types of models are most often used for this purpose: linear and branching time models. In this paper a third approach, based on socalled joint closure models, is studied using models which incorporate all possible behaviour in one model. Relations between this approach and the other two are studied. In order to define constructions needed to relate branching time models, appropriate algebraic notions are defined (in a category theoretical manner) and exploited. In particular, the notion...
462.
Calculi for Disjunctive Logic Programming
- Peter Baumgartner; Ulrich Furbach; Peter Baumgartner \delta Ulrich Furbach
We introduce a bottom-up and a top-down calculus for disjunctive logic programming (DLP). The bottom-up calculus, hyper tableaux, is depicted in its ground version and its relation to fixed point approaches from the literature is investigated. The top-down calculus, restart model elimination (RME), is presented as a sound and complete answer-computing mechanism for DLPs, and its relation to hyper tableaux is discussed. In two aspect this represents an extension of SLD-resolution for Horn clause logic programming: RME is SLD-resolution when restricted to Horn clauses, and it has a direct counterpart to the immediate consequence operator for Horn clauses. Furthermore we...
463.
Decision Diagrams And
- Pass Transistor Logic; V. Bertacco; V. Bertacco; V. Bertacco; S. Minato; S. Minato; S. Minato; P. Verplaetse; P. Verplaetse; P. Verplaetse; L. Benini; L. Benini; L. Benini; G. De Micheli; G. De Micheli; G. De Micheli
Since the relative importance of interconnections increases as feature size decreases, standardcell based synthesis becomes less e#ective when deep-submicron technologies become available. Intra-cell connectivity can be decreased by the use of macro-cells. In this work we present methods for the automatic generation of macro-cells using pass transistors and domino logic. The synthesis of these cells is based on BDD and ZBDD representations of the logic functions. We address speci #c problems associated with the BDD approach #level degradation, long paths# and the ZBDD approach #sneak paths, charge sharing, long paths#. We compare performance of the macro-cells approachversus the conventional standard-cell...
464.
The finite model property for knotted extensions of propositional linear logic
- van Alten, C. J.
The logics considered here are the propositional Linear Logic and
propositional Intuitionistic Linear Logic extended by a knotted
structural rule: ?, x
n ? y / ?, x
m
? y. It is proved that the class of algebraic models for
such a logic has the finite embeddability property, meaning
that every finite partial subalgebra of an algebra in the class can be
embedded into a finite full algebra in the class. It follows that
each such logic has the finite model property with respect to its
algebraic semantics and hence that the logic is decidable.
465.
Incompleteness of a First-order Gödel Logic and some Temporal Logics of Programs
- Matthias Baaz A; Er Leitsch B; Richard Zach B
Abstract. It is shown that the infinite-valued first-order Gödel logic G 0 based on the set of truth values {1/k: k ∈ ω \ {0}} ∪ {0} is not r.e. The logic G 0 is the same as that obtained from the Kripke semantics for first-order intuitionistic logic with constant domains and where the order structure of the model is linear. From this, the unaxiomatizability of Kröger’s temporal logic of programs (even of the fragment without the nexttime operator ○) and of the authors ’ temporal logic of linear discrete time with gaps follows.
466.
Beyond Tamaki-Sato Style Unfold/Fold Transformations for Normal Logic Programs
- Abhik Roychoudhury; K. Narayan Kumar; C. R. Ramakrishnan; I. V. Ramakrishnan
Unfold/fold transformation systems for logic programs have been extensively investigated. Existing unfold/fold transformation systems for normal logic programs typically fold using using a single, non-recursive clause i.e. the folding transformation is very restricted. In this paper we present a transformation system that permits folding in the presence of recursion, disjunction, as well as negation. We show that the transformations are correct with respect to various model theoretic semantics of normal logic programs including the well-founded model and stable model semantics. Keywords: Logic Programming, Program Transformations, Unfold/Fold Transformations, Normal Logic Programs. 1.
467.
Fundamenta Informaticae XXX-(2004) 1–25 1 IOS Press Quasi-possibilistic logic and its measures of information and conflict
- Didier Dubois; Sébastien Konieczny; Henri Prade
Abstract. Possibilistic logic and quasi-classical logic are two logics that were developed in artificial intelligence for coping with inconsistency in different ways, yet preserving the main features of classical logic. This paper presents a new logic, called quasi-possibilistic logic, that encompasses possibilistic logic and quasi-classical logic, and preserves the merits of both logics. Indeed, it can handle plain conflicts taking place at the same level of certainty (as in quasi-classical logic), and take advantage of the stratification of the knowledge base into certainty layers for introducing gradedness in conflict analysis (as in possibilistic logic). When querying knowledge bases, it may...
468.
Concurrency and Plan Generation in a Logic Programming Language With a Sequential Operator
- Alessio Guglielmi
In this paper we define a logic programming language, called SMR, whose main computational mechanism is multiset rewriting. It features a guarded choice capability and, above all, a sequential andlike operator. The language is defined starting from a core language, LM, a subset of Andreoli and Pareschi's LO, which is directly derived from linear logic. LM is minimal in a certain sense we will specify. The language SMR admits a translation into LM through a uniform "continuation" mechanism. We show how SMR could be interesting in two diverse areas, viz. concurrency and plan generation. Keywords Logic programming, linear logic, concurrency,...
469.
An Efficient Unification Algorithm for a Logic Database Language for Nested Relations
- Yiu-kai Ng; Qing Chang
Although efficient unification algorithms exist for logic database queries for flat relations, no efficient unification algorithm has been proposed for logic database queries for nested relations. As a result, the required time to process logic database queries for nested relations is often less than ideal. To overcome this shortcoming, we propose here a linear time unification algorithm for a large class of logic database queries for nested relations. The algorithm provides an efficient evaluation technique for many common nested relational queries. Our paper includes a characterization of the class of nested relational queries that can be handled by our proposed...
470.
Fast prototyping of computing-oriented fuzzy-logic systems
- Martínez Torre, J. I.; Deschamps, Jean Pierre; Fernández Centeno, M.
In this paper we propose to explore different dedicated hardware solutions in terms of area-speed trade-offs for computing-oriented fuzzy logic systems in the algorithmic abstraction level that fulfil the application requirements applying high level synthesis techniques. The main benefits of this proposal are the capability of selecting the best implementation for any application not being tied down to a predefined architecture, the use of the required number of hardware units and the reduction of the design cycle time. The results obtained in the control of a maximum power point of a photovoltaic plant are presented as an example.
471.
A neural implementation of multi-adjoint logic programs via sf-homogenization
- Medina, J.; Mérida Casermeiro, Enrique; Ojeda Aciego, Manuel
A generalization of the homogenization process needed for the neural implementation of multi-adjoint logic programming (a unifying theory to deal with uncertainty, imprecise data or incomplete information) is presented here. The idea is to allow to represent a more general family of adjoint pairs, but maintaining the advantage of the existing implementation recently introduced in [6]. The soundness of the transformation is proved and its complexity is analysed. In addition, the corresponding generalization of the neural-like implementation of the fixed point semantics of multi-adjoint is presented.
472.
Branching-Time Logic Programming: The Language Cactus and its Applications
- P. Rondogiannis; M. Gergatsoulis; T. Panayiotopoulos
Temporal programming languages provide a powerful means for the description and implementation of dynamic systems. However, most temporal languages are based on linear time, a fact that renders them unsuitable for certain types of applications (such as expressing properties of nondeterministic programs). In this paper we introduce the new temporal logic programming language Cactus, which is based on a branching notion of time. In Cactus, the truth value of a predicate depends on a hidden time parameter which varies over a tree-like structure. As a result, Cactus can be used to express in a natural way non-deterministic computations or generally...
473.
Logic BIST technology evaluation: an industrial case study
- Chris Feige; M. J. Geuzebroek
This paper presents an industrial case study on Built-In Self-Test for random logic (LBIST). The Self-testing Using MISR and Parallel SRSG (STUMPS) approach combined with multi-phase test point insertion (MTPI) has been evaluated on twenty-two industrial proven cores. The whole LBIST flow, including making cores LBIST ready and insertion of test points, has been investigated. The consequences with respect to fault coverage, MTPI parameter selection and area overhead are discussed. The case study results show that LBIST combined with MTPI can achieve comparable stuck-at fault coverages as Automatic Test Pattern Generation (ATPG) by acceptable area overhead.
474.
Compliance verification of agent interaction: a logic-based tool
- Marco Alberti; Marco Alberti; Federico Chesani; Federico Chesani; Marco Gavanelli; Marco Gavanelli; Evelina Lamma; Evelina Lamma; Paola Mello; Paola Mello; Paolo Torroni; Paolo Torroni
Abstract. In open societies of agents, where agents are autonomous and heterogeneous, it is not realistic to assume that agents will always act so as to comply to interaction protocols. Thus, the need arises for a formalism to specify constraints on agent interaction, and for a tool able to observe and check for agent compliance to interaction protocols. In this paper we present a Java-Prolog software component built on logic programming technology, which can be used to verify compliance of agent interaction to protocols, and that has been integrated with PROSOCS [Stathis et al., 2004]. ∗
475.
A Proof System and a Decision Procedure for Equality Logic
- Olga Tveretina; Hans Zantema
Abstract. We give an approach for deciding satisfiability of equality logic formulas (E-SAT) in conjunctive normal form. Central in our approach is a single proof rule called equality resolution (ER). For this single rule we prove soundness and completeness. Based on this rule we propose a complete procedure for E-SAT and prove its correctness. Applying our procedure on a variation of the pigeon hole formula yields a polynomial complexity contrary to earlier approaches to E-SAT. Parts of the theory we developed for proving completeness of the proof rule and the algorithm are of interest in itself: we give techniques for...
476.
Ordered Linear Logic and Applications
- Jeff Polakow; Harper John Reynolds
This work is dedicated to my parents. Acknowledgments Firstly, and foremost, I would like to thank my principal advisor, Frank Pfenning, for his patience with me, and for teaching me most of what I know about logic and type theory. I would also like to acknowledge some useful discussions with Kevin Watkins which led me to simplify some of this work. Finally, I would like to thank my other advisor, John Reynolds, for all his kindness and support over the last five years. Abstract This thesis introduces a new logical system, ordered linear logic, which combines reasoning with unrestricted, linear,...
477.
Backward Logic Tactics
- Alessandro Armando
Introduction
The notion of logic tactic has been introduced in [GT94] to express and
execute control strategies within a declarative metatheory. In this note we
adapt and extend the notion of logic tactic by (i) providing a formalization
of the backward primitive inference rules (let MT be the corresponding
metatheory), (ii) introducing the -abstraction operator and (iii) providing
the formalization of backward tacticals (let MT tac be the resulting metatheory)
. We argue that the -abstraction operation is necessary to express non
trivial control strategies). Finally we prove that MT tac is a conservative
extension of MT .
2 Backward logic tactics
Object level rules are modelled as partial functions ae...
478.
Linear, Branching Time and Joint Closure Semantics for Temporal Logic *
- Joeri Engelfriet; Jan Treur
Abstract. Temporal logic can be used to describe processes: their behaviour is characterized by a set of temporal models axiomatized by a temporal theory. Two types of models are most often used for this purpose: linear and branching time models. In this paper a third approach, based on socalled joint closure models, is studied using models which incorporate all possible behaviour in one model. Relations between this approach and the other two are studied. In order to define constructions needed to relate branching time models, appropriate algebraic notions are defined (in a category theoretical manner) and exploited. In particular, the...
479.
FLOW PREDICTION MODEL WITH FUZZY LOGIC APPROACHES: DIM STREAM
- M. Erol Keski̇n; Emine Dilek Taylan; A. Gökhan Yilmaz
In planning of the water structures, it is need some information about flow values. The identification of suitable generation models for future streamflows is an important precondition for successful planning and management of water resources, operation of flood control reservoirs, determination of flow potential in stream, forecasting of electric generation in hydroelectric power plants in drought periods, distribution of domestic and irrigation water and navigation in rivers. Flow prediction methods are countable as rainfall-runoff models or flood routing models for short periods; indis variable models, water budget models, rainfall-runoff models and time series models, respectively. In time series models, future...
480.
Block Cartesian Abstraction of a Geometric Model Using Fuzzy Logic
- Y. Su; A. Senthil Kumar
In this work, a fuzzy logic approach is proposed to transform a geometric model of arbitrary shape to its block Cartesian abstraction. This abstraction is topologically similar to the original model and it contains geometric sub-entities which are all aligned in the Cartesian directions. This is achieved by calculating the modifications made to the face normals as a result of the influences of the adjacent faces. A fuzzy logic inference engine is developed by combining heuristics to emulate the local changes in face normals with respect to the changes in the global space. A three-dimensional field morphing algorithm is used...
