601.
On the Relationship between \omega-Automata and Temporal Logic Normal Forms
- Alexander Bolotov; Michael Fisher; Clare Dixon
We consider the relationship between omega-automata and a specific logical formulation based on a normal form for temporal logic formulae. While this normal form was developed for use with execution and clausal resolution in temporal logics, we here show how it can represent, syntactically, omega-automata in a high-level way. Technical proofs of the correctness of this representation are given.
602.
Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications
- Wiebe van der Hoek; Michael Wooldridge
Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic ctl, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in ctl. Recently, ctl was generalised by Alur, Henzinger, and Kupferman in a logic known as "Alternating-time Temporal Logic" (atl). The key insight in atl is that the path quantifiers of ctl could be replaced by "cooperation modalities", of the form where...
603.
An Analysis of U.S. Patent #5,243,538 “Comparison and Verification System for Logic Circuits and Method Thereof,”
- Randal E. Bryant
On Sept. 7, 1993, U. S. Patent Number 5,243,538 was awarded to four Hitachi employees for a technique for comparing logic circuits using Binary Decision Diagrams (BDDs). Although the U. S. patent application was filed on Aug. 7, 1990, they had filed for a patent in Japan on Aug. 9, 1989, and hence this earlier date should be used in determining the prior art. The key property exploited by the patentees is that by generating the BDDs for the two logic circuits according to a unique ordering of the variables, the task of comparing the BDDs is greatly simplified. The...
604.
Challenge Problems for the Integration of Logic and Connectionist Systems (Extended Abstract)
There have been many results on such a combination which involves propositional logic (c.f. [27, 32]). In [18] we have shown that a three-layered feed forward network of binary threshold units can be used to compute the meaning function of a propositional logic program. The input and output layer of such a network consists of a vector of units, each representing a propositional letter. The activation pattern of these layers represent an interpretation I with the understanding that the unit representing the propositional letter p is active iff p is true under I. For certain classes of logic programs it...
605.
Logic Synthesis for Asynchronous Circuits Based on Petri Net Unfoldings and Incremental SAT
- Victor Khomenko; Maciej Koutny; Alex Yakovlev
The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is deriving equations for logic gates implementing each output signal of the circuit. This is usually done using reachability graphs.
606.
On Analysis of Boundness Property for ECATNets by Using Rewriting Logic
Abstract—To analyze the behavior of Petri nets, the accessibility graph and Model Checking are widely used. However, if the analyzed Petri net is unbounded then the accessibility graph becomes infinite and Model Checking can not be used even for small Petri nets. ECATNets [2] are a category of algebraic Petri nets. The main feature of ECATNets is their sound and complete semantics based on rewriting logic [8] and its language Maude [9]. ECATNets analysis may be done by using techniques of accessibility analysis and Model Checking defined in Maude. But, these two techniques supported by Maude do not work also...
607.
Logic Synthesis for Asynchronous Circuits Based on Petri Net Unfoldings and Incremental SAT
- Victor Khomenko; Maciej Koutny; Alex Yakovlev
The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is deriving equations for logic gates implementing each output signal of the circuit. This is usually done using reachability graphs.
608.
Two-phase Exception Logic
- Yao-hua Tan
In this paper we propose an exception logic -- formalizing
reasoning about exceptions. We use this logic to
defend two claims. First, we argue that default logic
-- formalizing reasoning about default assumptions -- is
an extension of exception logic. A deconstruction argument
shows that reasoning about exceptions is one
of the first principles of reasoning about default assumptions.
Second, we argue that two phases have to
be distinguished in reasoning about exceptions, and
therefore also in reasoning about default assumptions.
We identify two causes of the distinction between two
phases, the disjunction rule or and right weakening
rw. This sheds some new light on these `standard'
(according to the Kraus-Lehmann-Magidor paradigm)
properties of...
609.
Timed Possibilistic Logic
- Didier Dubois,Henri Prade
. This paper is an attempt to cast both uncertainty and time in a logical
framework. It generalizes possibilistic logic, previously developed by the authors,
where each classical formula is associated with a weight which obeys the laws of
possibility theory. In the possibilistic temporal logic we present here, each formula
is associated with a time set (a fuzzy set in the more general case) which represents
the set of instants where the formula is certainly true (more or less certainly true in
the general case). When a particular instant is fixed we recover possibilistic logic.
Timed possibilistic logic generalizes possibilistic logic also in the sense that...
610.
Higher-order Computational Logic
- J. W. Lloyd
. This paper presents the case for the use of higher-order logic
as a foundation for computational logic. A suitable polymorphicallytyped,
higher-order logic is introduced and its syntax and proof theory
briefly described. In addition, a metric space of closed terms suitable for
knowledge representation purposes is presented. The approach to representing
individuals is illustrated with some examples, as is the technique
of programming with abstractions. The paper concludes by placing the
results in the wider context of previous and current research in the use
of higher-order logic in computational logic.
1 Introduction
In 1974, Robert Kowalski published the seminal idea that predicate logic could
be used as a programming language...
611.
The New Logic
- Dov Gabbay Department
The purpose of this paper is to communicate some developments in what we call the new logic. In a nutshell the new logic is a model of the behaviour of a logical agent. By these lights, logical theory has two principal tasks. The rst is an account of what a logical agent is. The second is a description of how this behaviour is to be modelled. Before getting on with these tasks we oer a disclaimer and a warning. The disclaimer is that although the new logic is signi cantly dierent from it, we have no inclination to see the...
612.
Constraint Logic Programming
- Francois Fages,Le Chesnay Cedex
this article appeared in the Proc. of Logic in Computer
Science LICS'98, pp.141-152, IEEE Computer Society, Indianapolis, (1998).
613.
On a Logic of Induction
- Diderik Batens
In this paper, I present a simple and straightforward logic of induction:
a consequence relation characterized by a proof theory and a semantics.
614.
A Constraint Functional Logic
- Antonio J. Fern'andez
We present CFLP(FD), a constraint functional logic programming approachover
finite domains (FD) for solving typical combinatorial problems.
615.
Embedding Defeasible Logic into Logic Programs G. Antoniou
- G. Antoniou
Defeasible reasoning is a simple but efficient approach to
nonmonotonic reasoning that has recently attracted considerable interest
and that has found various applications. Defeasible logic and its variants
are an important family of defeasible reasoning methods. So far no relationship
has been established between defeasible logic and mainstream
nonmonotonic reasoning approaches.
616.
APV logic simulations
- N. Marinelli
The amount of data in the CMS inner tracker system at the LHC interaction rate is so large that it
cannot be read out at each bunch crossing. A pipeline memory is then needed to store the data at
the front--end level until a Level 1 Trigger accept signal marks the interesting data which will then be
read out. Due to the random arrival of triggers with a maximum average rate of 100kHz a queue may
develop in the pipeline which in the end can become full and cause errors. Some triggers must then
be vetoed.
In the present version of the chip to be used...
617.
Epistemic Logic: A Survey
- Rineke Verbrugge
Introduction
Epistemic logic is the logic of knowledge: how do you reason about the question
whether your silent admirer knows that you know that (s)he sent you an anonymous
Valentine card? Is it harmful if, at a literature-exam you don't know the
contents of a chapter? No, as long as you know that the examiner does not
know that you do not know it. Knowing whether your neighbor knows that
he regularly plays his radio so loudly that you wake up during the night, may
help you to solve the problem in an appropriate way. In negotiations, it will
harm you to let the other party know your...
618.
Probabilistic Neighbourhood Logic
- Dimitar P. Guelev
This paper presents a probabilistic extension of Neighbourhood Logic (NL,[ZH96, RZ97, BZ97, BRZ00]). The study of such an extension is motivated by the need to supply the Probabilistic Duration Calculus (PDC, [LRSZ92, DZ94]) with a proof system. The relation between the new logic and PDC is similar to that between DC [ZHR91] and ITL [Mos85, Dut95]. We present a complete proof system for the new logic.
619.
On Role Logic
- Viktor Kuncak,Martin Rinard
We present role logic, a notation for describing properties
of relational structures in shape analysis, databases, and
knowledge bases. We construct role logic using the ideas
of de Bruijn's notation for lambda calculus, an encoding of
first-order logic in lambda calculus, and a simple rule for
implicit arguments of unary and binary predicates.
620.
On Role Logic
- Viktor Kuncak,Martin Rinard
We present role logic, a notation for describing properties
of relational structures in shape analysis, databases, and
knowledge bases. We construct role logic using the ideas
of de Bruijn's notation for lambda calculus, an encoding of
first-order logic in lambda calculus, and a simple rule for
implicit arguments of unary and binary predicates.
