281.
Nonmonotonic Logic
- John F. Horty
Introduction
The goal of a logic is to dene a consequence relation between a set of formulas
and, in most cases, an individual formula A. This denition generally takes one of
two forms. From a proof theoretic standpoint A is said to be a consequence of
whenever there is a deduction of A from the set , viewed as a set of premises; from
a model theoretic standpoint, A is said to be a consequence of whenever A holds
in every model that satises each formula in .
Although the detailed inferences sanctioned by particular logics vary widely
depending on the connectives present and the properties attributed to...
282.
Modelización mediante lógica difusa del mecanismo biológico regulador de la glucemia
- Sánchez Romero, José Luis; Ruiz Fernández, Daniel; Ferrández Pastor, Francisco Javier; García Chamizo, Juan Manuel; Soriano Payá, Antonio
La diabetes mellitus es una patología relacionada con
una deficiente regulación de la glucemia. El sistema
biológico encargado de controlar la glucosa en sangre es
de gran complejidad, y su modelización basada tanto en
esquemas clásicos como en redes neuronales y
algoritmos genéticos presenta serios inconvenientes. En
este trabajo se presenta una modelización del sistema
biológico regulador basada en lógica difusa. El modelo
desarrollado está compuesto por diferentes módulos,
cada uno de ellos encargado del seguimiento de un tipo
de sustancia implicada en el control glucémico y
diseñado mediante estructuras de control difuso. Los
resultados obtenidos ponen de manifiesto que el modelo
desarrollado proporciona buenos resultados para los
diferentes estados metabólicos estudiados. Este trabajo
sirve...
283.
Visualization Designs for Constraint Logic Programming
- Manuel Carro; Manuel Hermenegildo
We address the design and implementation of visual paradigms for observing the execution of constraint logic programs, aiming at debugging, tuning and optimization, and teaching. We focus on the display of data in CLP executions, where representation for constrained variables and for the constrains themselves are seeked. Two tools, VIFID and TRIFID, exemplifying the devised depictions, have been implemented, and are used to showcase the usefulness of the visualizations developed.
284.
Logical consecutions in discrete linear temporal logic
- Rybakov, V. V.
We investigate logical consequence in temporal logics in terms of logical consecutions, i.e., inference rules. First, we discuss the question: what does it mean for a logical consecution to be correct in a propositional logic. We consider both valid and admissible consecutions in linear temporal logics and discuss the distinction between these two notions. The linear temporal logic LDTL, consisting of all formulas valid in the frame ? ??, ?, ? ? of all integer numbers, is the prime object of our investigation. We describe consecutions admissible in LDTL in a semantic wayvia consecutions valid in special temporal Kripke/Hintikka models....
285.
Rough Logic Control
The traditional approach to automatic control is based on the assumption that an analytical model
of the controlled process is available. A rule based control system does not require a classical
mathematical description of the process, but consist of a set of If-Then rules as an experienced
human operator might formulate his knowledge of the process in question. Thus we obtain not only
a separation between the controller and a mathematical process model in the classical sense, but
are also able to formulate the control algorithm in a more humanlike way. The If-Then rules also
form a kind of mathematical description of the controlled process, but...
286.
Tableaus for Logic Programming
We present a logic programming language, which we call Proflog, with an operational semantics
based on tableaus, and a denotational semantics based on supervaluations. We show
the two agree. Negation is well-behaved, and semantic non-computability issues do not arise.
This is accomplished essentially by dropping a domain closure requirement. The cost is that
intuitions developed through the use of classical logic may need modification, though the system
is still classical at a level once removed. Implementation problems are discussed very briefly ---
the thrust of the paper is primarily theoretical.
1 Introduction
Life would be almost perfect if we had a logic programming language that was e#cient, treated
negation...
287.
A Temporal Logic of Actions
In 1977, Pnueli introduced to computer scientists a temporal logic for reasoning
about concurrent programs. His logic was simple and elegant, based
on the single temporal modality "forever", but it was not expressive enough
to completely describe programs. Since then, a plethora of more expressive
logics have been proposed, all with additional temporal modalities such as
"next", "until", and "since". Here, a temporal logic is introduced based
only on Pnueli's original modality "forever", but with predicates (assertions
about a single state) generalized to actions---assertions about pairs of states.
This logic has all the expressive power needed to describe and reason about
concurrent programs. Much of the temporal reasoning required...
288.
Mathematics and Logic
eep impact on the development of logic as well as on the science of computing.
It was the problem that led to Turing's world-famous paper that is generally recognised
as laying the basis for the development of computing machinery. (In his paper Turing
developed a mathematical model of a computer"; the paper was published in 1936 well
before any (electronic) computer existed.) Hilbert wanted to construct a complete and
consistent axiomatisation of logic. Godel showed that this was impossible, and Turing
1
showed that not everything is computable. But, in spite of these two negative results (or
perhaps because of them), interest in formalising logic has continued unabated.
Undoubtedly,...
289.
Logic Based Distributed Decision
- System For Multi-Robot; Miguel Arroz; Vasco Pires; Luis Custódio
In this paper a decision system for a team, constituted by several robots is described. The system is distributed and uses logic to choose the most suitable action in order to accomplish a pre-determined goal. It also supports cooperation and machine learning.
290.
Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic
- Baaz, Matthias; Zach, Richard
Takeuti and Titani have introduced and investigated a logic they called
intuitionistic fuzzy logic. This logic is characterized as the first-order
Goedel logic based on the truth value set [0,1]. The logic is known to be
axiomatizable, but no deduction system amenable to proof-theoretic, and hence,
computational treatment, has been known. Such a system is presented here, based
on previous work on hypersequent calculi for propositional Goedel logics by
Avron. It is shown that the system is sound and complete, and allows
cut-elimination. A question by Takano regarding the eliminability of the
Takeuti-Titani density rule is answered affirmatively.
291.
ABSTRACT A COMPILER SYSTEM OF A LINEAR LOGIC PROGRAMMING LANGUAGE
Linear logic developed by J.-Y. Girard can be described as a logic of resources. There have been several proposals for logic programming language based on linear logic: LO, LinLog, ACL, Lolli, Lygon, and Forum. Lolli and Lygon are implemented as interpreter systems (on SML and λProlog for Lolli, on Prolog for Lygon). But, none of them have been implemented as a compiler system. This paper describes a compiler system of a linear logic programming language called LLP. New features of LLP with various example programs are also shown. LLP is a superset of Prolog and a subset of Lolli. LLP...
292.
Decidability of quantified propositional intuitionistic logic and S4 on
trees
- Zach, Richard
Quantified propositional intuitionistic logic is obtained from propositional
intuitionistic logic by adding quantifiers \forall p, \exists p over
propositions. In the context of Kripke semantics, a proposition is a subset of
the worlds in a model structure which is upward closed. Kremer (1997) has shown
that the quantified propositional intuitionistic logic H\pi+ based on the class
of all partial orders is recursively isomorphic to full second-order logic. He
raised the question of whether the logic resulting from restriction to trees is
axiomatizable. It is shown that it is, in fact, decidable. The methods used can
also be used to establish the decidability of modal S4 with propositional
quantification on...
293.
Concurrent Logic Programming in Linear Logic
- Jir Zlatuska
. A proof-theoretic semantics based on linear logic is developed
for committed-choice logic languages, represented here by
Flat Concurrent Prolog. Several fragments of linear logic are used in
order to provide for a suitable translation of guarded clauses clauses,
with the committed-choiceconcurrency featurescaptured by the properties
of linear logic provability rather than by some additional mechanism
and without the need of using interleaving approach for de#ning
concurrent behaviour. Linear logic operations from different fragments
correspond in quite a natural way to the need for speci#c features
of the translation. Two different translations are proposed here,
one of them corresponding to the backward-chaining execution, and
the other one to a process-related interpretation...
294.
Possibilistic Logic as an Annotated Logic
- Peter Kullmann
In this paper we study how to transform possibilistic logic
extended with fuzzy constants and fuzzy quantifiers into the
generalized annotated logic system proposed by Kifer and
Subrahmanian in 1992. Specifically, the valuation in a possibilistic
clause generates the annotation which will be attached
to the head of the annotated clause. We also show how the inference
rules of possibilistic logic extended with fuzzy constants
can be translated in terms of the mechanisms provided
by this annotated logic.
295.
Non-Orthomodular Models for Both Standard Quantum Logic and Standard Classical Logic: Repercussions for Quantum Computers
- Mladen Pavičić; Norman D. Megill
Abstract. It is shown that propositional calculuses of both quantum and classical logics are noncategorical. We find that quantum logic is in addition to an orthomodular lattice also modeled by a weakly orthomodular lattice and that classical logic is in addition to a Boolean algebra also modeled by a weakly distributive lattice. Both new models turn out to be non-orthomodular. We prove the soundness and completeness of the calculuses for the models. We also prove that all the operations in an orthomodular lattice are five-fold defined. In the end we discuss possible repercussions of our results to quantum computations and...
296.
A Calculus of Inconsistency I: Sentential Logic
- Seabold, Dan; Waner, Stefan; Warner, Steve
We describe a graph-theoretic syntax for self-referential formulas as well as
a four-valued logic to include contradictory and independent formulas. We then
explore the degree to which generalized truth tables can be realized in our
theory, and go on to describe a model theory for sentential calculus, wherein
models are allowed to include contradictions (such as the ``Liar'') and
formulas that result from them as an integral part of their structure. This
sets the groundwork for a sequel in which we construct models of set theory
that include contradictions.
297.
Efficient Pattern Mapping for Deterministic Logic BIST
- Hans-joachim Wunderlich
Deterministic logic BIST (DLBIST) is an attractive test strategy, since it combines advantages of deterministic external testing and pseudo-random LBIST. Unfortunately, previously published DLBIST methods are unsuited for large ICs, since computing time and memory consumption of the DLBIST synthesis algorithms increase exponentially, or at least cubically, with the circuit size. In this paper, we propose a novel DLBIST synthesis procedure that has nearly linear complexity in terms of both computing time and memory consumption. The new algorithms are based on binary decision diagrams (BDDs). We demonstrate the efficiency of the new algorithms for industrial designs up to 2M gates.
298.
Unique Supported-Model Classes of Logic Programs
- Pascal Hitzler; Anthony Karel Seda
We study classes of programs, herein called unique supported-model classes, with the property that each program in the class has a unique supported model. Elsewhere, the authors examined these classes from the point of view of operators dened relative to certain three-valued logics. In this paper, we complement our earlier results by considering how unique supported-model classes t into the framework given by various classes of programs in several well-known approaches to semantics. Keywords: logic programming, denotational semantics, supported-model semantics 1
299.
Efficient Pattern Mapping for Deterministic Logic BIST
- Hans-joachim Wunderlich
Deterministic logic BIST (DLBIST) is an attractive test strategy, since it combines advantages of deterministic external testing and pseudo-random LBIST. Unfortunately, previously published DLBIST methods are unsuited for large ICs, since computing time and memory consumption of the DLBIST synthesis algorithms increase exponentially, or at least cubically, with the circuit size. In this paper, we propose a novel DLBIST synthesis procedure that has nearly linear complexity in terms of both computing time and memory consumption. The new algorithms are based on binary decision diagrams (BDDs). We demonstrate the efficiency of the new algorithms for industrial designs up to 2M gates.
300.
Cactus: A branching-time logic programming language
- P. Rondogiannis; M. Gergatsoulis; T. Panayiotopoulos
Abstract. Temporal programming languages are recognized as natural and expressive formalisms for describing dynamic systems. However, most such languages are based on linear ow of time, a fact that makes them unsuitable for certain types of applications. 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 has a tree-like structure. As a result, Cactus appears to be especially appropriate for expressing non-deterministic computations or generally algorithms that involve the manipulation of tree data...
