Abstract Context Logic as Modal Logic: Completeness and Parametric Inexpressivity Separation Logic, Ambient Logic and Context Logic are based on a
similar style of reasoning about structured data. They each consist of a structural (separating) composition for reasoning about disjoint subdata, and corresponding structural adjoint(s) for reasoning hypothetically about data. We show how to interpret these structural connectives as modalities in Modal Logic and prove completeness results. The structural connectives are essential for describing properties of the underlying data, such as weakest preconditions for Hoare reasoning for Separation and Context Logic, and security properties for Ambient Logic. In fact, we introduced Context Logic to reason about tree update, precisely because the structural connectives of the Ambient Logic did not have enough...
Abstract. This paper presents an expressive language for representing knowledge about vague con-cepts. It is based on the rough set formalism and it caters for implicit definition of rough relations by combining different regions (e.g. upper approximation, lower approximation, boundary) of otherrough relations. The semantics of the proposed language is obtained by translating it to the language of extended logic programs whose meaning is captured by paraconsistent stable models. A querylanguage is also discussed to retrieve information about the defined rough relations. Motivating examples illustrating the use of the language are described.
Ordered programs as abductive systems
- Davy Van Nieuwenborgh; Dirk Vermeir
Abstract. In ordered logic programs, i.e. partially ordered sets of clauses where smaller rules carry more preference, inconsistencies, which appear as conflicts between applicable rules, are handled by satisfying more preferred rules, at the expense of defeating lesser rules. We show that this formalism can be exploited to obtain a simple implementation of abductive systems, where abducibles are assumed false by default, but weaker rules can be used to introduce them, if necessary. Moreover, the approach can be extended, without leaving the ordered programming framework, to support abductive systems involving preference, either on the set of abducibles or on the...
PIECEWISE LINERIZATION OF LOGIC FUNCTIONS *
- Ilya Levin; Osnat Keren; George Kolotov; Mark Karpovsky
The paper deals with a problem of linearization of multi-output logic functions. Specifically, the case is discussed, when the functions have a large number of variables and cannot be efficiently linearized by using known techniques. For solution of the problem a socalled piecewise linearization is proposed. The piecewise linearization comprises decomposition of an initial multi-output function into a network of components, followed by independent linearization of the components. The decomposition is based on the theory of D-polynomials described in the paper. The resulting piecewise linearized network is directly mapable onto a special type of a binary graph called Parallel Multi...
Translating PLTL into WS1S: Application Description
Abstract This paper introduces a technique for translating propositional linear time logic PLTL into the weak second-order logic of one successor WS1S. Using the Mona tool, a decision procedure for WS1S, we obtain a decision procedure for PLTL. We demonstrate the viability of this approach by an empirical comparison with STeP, SMV, and the Logics Workbench on a class of semi-randomly generated PLTL-formulae.
Extraction of Temporal Information from Texts in Swedish
- Anders Berglund; Richard Johansson; Pierre Nugues
This paper describes the implementation and evaluation of a generic component to extract temporal information from texts in Swedish. It proceeds in two steps. The first step extracts time expressions and events, and generates a feature vector for each element it identifies. Using the vectors, the second step determines the temporal relations, possibly none, between the extracted events and orders them in time. We used a machine learning approach to find the relations between events. To run the learning algorithm, we collected a corpus of road accident reports from newspapers websites that we manually annotated. It enabled us to train...
Converting Inference Rules into Conditional Effects
- M. Garagnani
Given a planning domain, if the language adopted for the state representation is sophisticated enough to allow an accurate, simple and natural description of a problem, it is likely to contain `redundancies', i.e. expressions whose validity (or truth) can be deduced from that of other expressions currently present in the state. The relations expressing these redundancies are normally identi ed, in planning, as `domain axioms', but correspond to what in logic is usually called inference rules (I.R.). The problem of integrating a set of I.R. into a given planner which does not support domain axioms can be solved either by...
Inductive invariants for nested recursion
- Sava Krstić; John Matthews
Abstract. We show that certain input-output relations, termed inductive invariants are of central importance for termination proofs of algorithms defined by nested recursion. Inductive invariants can be used to enhance recursive function definition packages in higher-order logic mechanizations. We demonstrate the usefulness of inductive invariants on a large example of the BDD algorithm Apply. Finally, we introduce a related concept of inductive fixpoints with the property that for every functional in higher-order logic there exists a largest partial function that is such a fixpoint. 1
Sequential, Parallel, and Quantified Updates of First-Order Structures
Abstract. We present a datastructure for storing memory contents of imperative programs during symbolic execution—a technique frequently used for program verification and testing. The concept, called updates, can be integrated in dynamic logic as runtime infrastructure and models both stack and heap. Here, updates are systematically developed as an imperative programming language that provides the following constructs: assignments, guards, sequential composition and bounded as well as unbounded parallel composition. The language is equipped both with a denotational semantics and a correct rewriting system for execution, whereby the latter is a generalisation of the syntactic application of substitutions. The normalisation of...
Exogenous semantics approach to enriching logics
- Paulo Mateus; Amílcar Sernadas; Cristina Sernadas
Abstract. The exogenous semantics approach to enriching a logic consists in defining each model in the enrichment as a set of models in the original logic plus some relevant structure. We illustrate the approach by probabilizing classical propositional logic, including a novel global propositional logic. A model of the probability logic is a probability space where the outcomes are classical valuations. A model of the global propositional logic is simply a set of classical valuations. Syntactically, probabilities appear as constructors of new terms from classical formulas. Soundness and completeness results are proved for the calculi of both logics. A simple...
1 Background Combining logic systems: Why, how, what for?
- A. Sernadas; C. Sernadas
The practical significance of the problem of combining logics is widely recognized, namely in knowledge representation (within artificial intelligence) and in formal specification and verification of algorithms and protocols (within software engineering and security). In these fields, the need for working with several calculi at the same time is the rule rather than the exception. For instance, in a knowledge representation problem it may be necessary to work with temporal, spatial, deontic and probabilistic aspects (e.g., for reasoning with mixed assertions like “with probability greater than 0.99, sometime in the future smoking will be forbidden everywhere”). And in a software...
Precise and expressive mode systems for typed logic programming languages
- David Overton
Abstract In this thesis we look at mode analysis of logic programs. Being based on the mathematical formalism of predicate logic, logic programs have no a priori notion of data flow-- a single logic program may run in multiple modes where each mode describes, or prescribes, a pattern of data flow.
Model revision from temporal logic properties in computational systems biology
- François Fages; Sylvain Soliman
Systems biologists build models of bio-molecular processes from knowledge acquired both at the gene and protein levels, and at the phenotype level through experiments done in wild-life and mutated organisms. In this chapter, we present qualitative and quantitative logic learning tools, and illustrate how they can be useful to the modeler. We focus on biochemical reaction models written in the Systems Biology Machine BIOCHAM. We first present a model revision algorithm for inferring reaction rules from biological properties expressed in temporal logic. Then we discuss the representations of kinetic models with ordinary differential equations (ODEs) and with stochastic logic programs...
Modular verification of a non-blocking stack
- Matthew Parkinson; Richard Bornat; Peter O’Hearn
This paper contributes to the development of techniques for the modular proof of programs that include concurrent algorithms. We present a proof of a non-blocking concurrent algorithm, which provides a shared stack. The inter-thread interference, which is essential to the algorithm, is confined in the proof and the specification to the modular operations, which perform push and pop on the stack. This is achieved by the mechanisms of separation logic. The effect is that inter-thread interference does not pollute specification or verification of clients of the stack.
Doctoral Dissertation Temporal Linear Logic and Its Applications
- Takaharu Hirai
Linear logic, introduced by Girard in 1987, has been called a resource conscious logic. In order to express a dynamic change in process environment, it is useful to consider a concept of resource such as data consumption. The expressive power of linear logic is evidenced by some very natural encodings of computational models such as Petri nets, counter machines, Turing machines, and others. For example, in Petri nets, tokens are considered as resources that are consumed and transitions are considered as reusable resources. It is well known that the reachability problem for ordinary Petri nets is equivalent to the provability...
This paper presents a new method for modeling and solving high-level synthesis problem. In our approach, finite domain constraints and related constraints solving techniques offered by constrained logic programming are used. They make it possible to define basic constraints on operations and registers and provide a way to find optimal or suboptimal solutions to the data-path synthesis problem. Different design styles, such as multicycling, chaining, pipelined components and algorithmic pipelining can be modeled in this framework. The proposed formulation combines different constraints in one representation and thus the optimization can find a better solution. The prototype system has been implemented...
Interoperable transactions in business models -- a structured approach
- H. Weigand; E. Verharen; F. Dignum
Recent database research has given much attention to the specification of "flexible" transactions that can be used in interoperable systems. Starting from a quite different angle, Business Process Modelling has approached the area of communication modelling as well (the Language/Action perspective). The main goal of this paper is to provide some useful structuring mechanisms for interoperable transactions based on the Language/Action perspective. The paper thus tries to build a bridge between two rather separated worlds: the research on interoperable transactions on the one hand, and the research on business process models on the other. Extended deontic logic provides the material...
Kernels on Prolog Proof Trees: Statistical Learning in the ILP Setting
- A. Passerini Passerini A○dsi·unifi·it; P. Frasconi P-f A○dsi·unifi·it; L. De Raedt Deraedt A○informatik·uni-freiburg·de
We develop kernels for measuring the similarity between relational instances using background knowledge expressed in first-order logic. The method allows us to bridge the gap between traditional inductive logic programming representations and statistical approaches to supervised learning. Logic programs will be used to generate proofs of given visitor programs which exploit the available background knowledge, while kernel machines will be employed to learn from such proofs. We report positive empirical results on Bongard-like and M-of-N problems that are difficult or impossible to solve with traditional ILP techniques, as well as on a real data set. 1.
Complexity-Effective Superscalar Embedded Processors Using Instruction-Level Distributed Processing
- Ian Caulfield
Modern trends in mobile and embedded devices require ever increasing levels of performance, while maintaining low power consumption and silicon area usage. This thesis presents a new architecture for a high-performance embedded processor, based upon the instruction-level distributed processing (ILDP) methodology. A qualitative analysis of the complexity of an ILDP implementation as compared to both a typical scalar RISC CPU and a superscalar design is provided, which shows that the ILDP architecture eliminates or greatly reduces the size of a number of structures present in a superscalar architecture, allowing its complexity and power consumption to compare favourably with a simple...
Executable Temporal Logic for Distributed A.I
- Michael Fisher; Michael Wooldridge
DAI’93 Themes: societies and organisations of agents; modeling through communication in adversarial and cooperative systems This paper describes Concurrent METATEM, a programming language based on temporal logic, and applies it to the study of Distributed Artificial Intelligence (DAI). A Concurrent METATEM system consists of a number of asynchronously executing objects, which are able to communicate through broadcast message-passing. Each individual object directly executes a specification of its desired behaviour. Such specifications are given using a set of temporal logic ‘rules’, determining how the object may generate ‘commitments’, which it subsequently attempts to satisfy. This language provides a novel and powerful...