Executable Temporal Logic for Nonmonotonic Reasoning
- Joeri Engelfriet; Jan Treur
this paper we view nonmonotonic reasoning as a (special kind of) process. As temporal logic is a common formalism to specify and derive properties of processes, we introduce a variant of temporal logic as a general specification language for reasoning processes. We show that it is possible to execute finite specifications in this language, which leads to executability of a large class of finite nonmonotonic reasoning processes. 1. Introduction
A CMOS VLSI Implementation of an Asynchronous ALU
- J.D. Garside
A CMOS self-timed ALU has been developed as part of an asynchronous implementation of the ARM microprocessor. This unit exploits the data dependency inherent in many arithmetic operations to enable a small, simple ALU to deliver a mean performance comparable with that of a more sophisticated synchronous one with consequent reductions in both silicon area and electrical power consumption. The self-timed nature of the unit means that the majority of operations complete quickly whilst allowing rare `worst-case' operations to take longer, maintaining a high average throughput. This paper presents instruction usage statistics to justify the claimed performance and SPICE simulation...
"Almost always" and "definitely sometime" are not enough: Probabilistic quantifiers and Probabilistic model-checking
- Purush Iyer; Murali Narasimha
Specifications for probabilistic programs often use the notion of almost always and definitely sometime to capture the probabilistic information. But there are a number of instances (eg. network protocols) where probabilistic information needs to be explicitly specified. In this paper we present PCTL , a probabilistic version of the branching time logic CTL , where the quantifiers for universality (almost always) and existence (definitely sometime) are replaced by a single probabilistic quantifier. We argue that this logic is more general than previous logics. We show how to model-check probabilistic programs (given as markov chains) against specifications in PCTL . We...
- Johan Van Benthem; Jan van Eijck; Alla Frolova
Abstract This is an exploratory document for a new research line in logical semantics which is emerging from several current developments in computer science. Standard logic employs 'flat' unstructured sets of statements for its theories and unstructured classes of models for its semantic universes. Nowadays, however, there is an incipient literature on structured universes of models as well as structured theories, both employing 'preference relations' of some sort. The purpose of this brief report is (1) to propose a more systematic framework for this trend, while also connecting it up with some historical predecessors, (2) to design some new logical...
Programming Paradigms of the Andorra Kernel Language
- Sverker Janson; Seif Haridi
The Andorra Kernel Language (AKL) is introduced. It is shown how AKL provides the programming paradigms of both Prolog and GHC. This is the original goal of the design. However, it has also been possible to provide capabilities beyond that of Prolog and GHC. There are means to structure search, more powerful than plain backtracking. It is possible to encapsulate search in concurrent reactive processes. It is also possible to write a multi-way merger with constant delay. In these respects AKL is quite original. Although AKL is an instance of our previously introduced Kernel Andorra Prolog framework, this exposition contains...
Reasoning about knowledge of unawareness
- Joseph Y. Halpern; Leandro Chaves Rêgo
Awareness has been shown to be a useful addition to stan-dard epistemic logic for many applications. However, stan-dard propositional logics for knowledge and awareness can-not express the fact that an agent knows that there are facts of which he is unaware without there being an explicit fact that the agent knows he is unaware of. We propose a logic for reasoning about knowledge of unawareness, by extending Fagin and Halpern’s Logic of General Awareness. The logic allows quantification over variables, so that there is a formula in the language that can express the fact that “an agent explic-itly knows that...
Evaluation of a DPA-Resistant Prototype Chip
- Mario Kirschbaum
Abstract—The recently proposed masked logic style iMDPL seems to eradicate many of the latest points of criticism against masked logic styles in general. By means of a prototype chip containing different implementations we analyze the DPA resistance of iMDPL. Furthermore we compare the results with the logic styles ’ predecessor MDPL, which verifiably suffers from an effect called ”early propagation”. We also investigate iMDPL regarding an advanced attack approach that claims to be able to almost completely remove the effect of masking in masked logic styles.
Otter: The CADE-13 Competition Incarnations
- William Mccune; Larry Wos
. This article discusses the two incarnations of Otter entered in the CADE-13 Automated Theorem Proving Competition. Also presented are some historical background, a summary of applications that have led to new results in mathematics and logic, and a general discussion of Otter. Key words: Automated theorem proving, automated reasoning, equational deduction, Otter, paramodulation, resolution. 1. Introduction Otter [19, 21] is an automated deduction system for first-order logic with equality. Two versions of Otter were entered in the CADE-13 Automated Theorem Proving System Competition, and the main purpose of this article is to give a detailed presentation of our entries....
Complexity and Expressive Power of Logic Programming
- Evgeny Dantsin; Thomas Eiter; Georg Gottlob; Andrei Voronkov
This paper surveys various complexity and expressiveness results on different forms of logic programming. The main focus is on decidable forms of logic programming, in particular, propositional logic programming and datalog, but we also mention general logic programming with function symbols. Next to classical results on plain logic programming (pure Horn clause programs), more recent results on various important extensions of logic programming are surveyed. These include logic programming with different forms of negation, disjunctive logic programming, logic programming with equality, and constraint logic programming.
Using Prediction to Accelerate Coherence Protocols
- S.S. Mukherjee; Mark D. Hill
Most large shared-memory multiprocessors use directory protocols to keep per-processor caches coherent. Some memory references in such systems, however, suffer long latencies for misses to remotely-cached blocks. To ameliorate this latency, researchers have augmented standard coherence protocols with optimizations for specific sharing patterns, such as read-modify-write, producer-consumer, and migratory sharing. This paper seeks to replace these directed solutions with general prediction logic that monitors coherence activity and triggers appropriate coherence actions. This paper takes the first step toward using general prediction to accelerate coherence protocols by developing and evaluating the Cosmos coherence message predictor. Cosmos predicts the source and type...
Synthesis of the Hardware/Software Interface in Microcontroller-Based Systems
- Pai Chou; Ross Ortega; Gaetano Borriello
Microcontroller-based systems require the design of a hardware/software interface that enables software running on the microcontroller to control external devices. This interface consists of the sequential logic that physically connects the devices to the microcontroller and the software drivers that allow code to access the device functions. This paper presents a method for automatically synthesizing this hardware/software interface using a recursive algorithm. Practical examples are used to demonstrate the utility of the method and results indicate that the synthesized circuit and driver code are comparable to that generated by human designers. This new tool will be used by higher-level synthesis...
Intuitionistic Logic with a "Definitely" Operator
- Peter Mott
This paper introduces a logic ILED derived from standard intuitionistic sentence logic by adding two operators Dj for "Definitely j" and ~j for "Experience rejects j". A further negation j = def (j®^) Ú ~j , which we call real negation, is introduced. Real negation is like intuitionistic negation when there are no D-operators but deviates when there are. We see that Dj j is valid but Dj ® j is not and hence that contraposition fails for real negation. We give a semantics for this logic, axiomatise it and prove the axiomatisation complete. Finally we show that real negation...
Formalization of graphical schemas: General sketch-based logic vs heuristic pictures
- Zinovy Diskin
e lack of rigor in graph-based formalisms supporting schemas as such. Then there emerges the tempting problem of providing schemas with an appropriate graph-based logic so that graphical images themselves can be regarded as formal specifications. Indeed, several successful attempts are already known, e.g., proof trees in proof theory, parsing trees in grammar theory, and sketches in category theory. We suggest a general approach to the problem encompassing a wide variety of kinds of schemas. The approach aims at providing (in a uniform way) schemas with a corresponding logic so that any schema can be considered as a theory of...
A Logical Foundation for Logic Programming II: Semantics of General Logic Programs
- Alexander Bochman
We suggested in  a general logical formalism for Logic Programming based on a four-valued inference. In this paper we give a uniform representation of various semantics for logic programs based on this formalism. The main conclusion from this representation is that the distinction between these semantics can be largely attributed to the difference in their underlying (monotonic) logical systems. Moreover, in most cases the difference can even be reduced to that of the language, that is, to the difference in the logical connectives allowed for representing derivable information. Keywords. Foundations of logic programming, negation as failure, semantics for logic...
CHAPTER 1 Background
- D. Stott Parker; Jr.
Machine (WAM). In a similar approach Mellish [Mell 85] describes the compilation of Prolog into a procedural language with first-class continuations, called POPLOG. Mellish also argues that the majority of Prolog programs are directed and deterministic and can therefore be directly compiled into efficient code running on conventional machines. In [Bruy 86], Bruynooghe suggests compiling Prolog to Pascal in order to improve garbage-collection performance in Prolog. Although the main motivation of this paper is developing static garbage collection mechanisms for Prolog, his work provides interesting insights into how Prolog-like languages can be translated into procedural languages. Weiner and Ramakrishnan [Wein...
Extended Logic Programs as Autoepistemic Theories
- Vladimir Lifschitz; Grigori Schwarz
Recent research on applications of nonmonotonic reasoning to the semantics of logic programs demonstrates that some nonmonotonic formalisms are better suited for such use than others. Circumscription is applicable as long as the programs under consideration are stratified. To describe the semantics of general logic programs without the stratification assumption, one has to use autoepistemic logic or default logic. When Gelfond and Lifschitz extended this work to programs with classical negation, they used default logic, because it was not clear whether autoepistemic logic could be applied in that wider domain. In this paper we show that programs with classical negation...
Equivalence and Tractability Results for SAS+ Planning
- Christer Bäckström
We define the SAS + planning formalism, which generalizes the previously presented SAS formalism. The SAS + formalism is compared with some better-known propositionalplanning formalisms with respect to expressiveness. Contrary to intuition, all formalisms turn out to be equally expressive in a very strong sense. We further present the SAS + -PUS planning problem which generalizes the previously presented, tractable SASPUS problem. We prove that also the SAS + - PUS problem is tractable by devising a provably correct polynomial time algorithm for this problem. 1 Introduction Much effort has gone into finding more and more general formalisms, mainly logic-based,...
A Methodology for Proving Termination of General Logic Programs
- Elena Marchiori
This paper introduces a methodology for proving termination of general logic programs, when the Prolog selection rule is considered. This methodology combines the approaches by Apt and Bezem [ 1 ] and Apt and Pedreschi [ 2 ] , and provides a simple and flexible tool for proving termination. 1 Introduction General logic programs (glp's for short) provide formalizations and implementations for special forms of nonmonotonic reasoning. For example, the Prolog negation as finite failure operator has been used to implement a formulation as logic program of the temporal persistence problem in AI (see [ 9; 8; 1 ] )....
Expressing and Detecting Control Flow Properties of Distributed Computations
- Vijay K. Garg; Vijay K Garg; Alex Tomlinson; Alex Tomlinson; Eddy Fromentin; Eddy Fromentin; Michel Raynal; Michel Raynal; Projets Adp
: Properties of distributed computations can be either on their global states or on their control flows. This paper addresses control flow properties. It first presents a simple yet powerful logic for expressing general properties on control flows, seen as sequences of local states. Among other properties, we can express invariance, sequential properties (to satisfy such a property a control flow must match a pattern described as a word on some alphabet) and non-sequential properties (these properties are on several control flows at the same time). A decentralized detection algorithm for properties described by this logic is then presented. This...
Loose Semantics and Constraints for Graph Transformation Systems
- Reiko Heckel; Hartmut Ehrig; Uwe Wolter; Andrea Corradini
. The main aim of this paper is an extension of the theory of algebraic graph transformation systems by a loose semantics. For this purpose, graph transitions are introduced as a loose interpretation of graph productions. They are defined using a double pullback construction in contrast to classical graph derivations based on double-pushouts. Two characterisation results relate graph transitions to the classical double-pushout derivations and to amalgamated derivations, respectively. Moreover, a loose semantics for graph transformation systems is defined, which associates with each system a category of models (deterministic transition systems) defined as coalgebras over a suitable functor. Such category...