ALLPAD: Approximate learning of logic programs with annotated disjunctions (Tech. Rep
- Fabrizio Riguzzi
Abstract. Logic Programs with Annotated Disjunctions (LPADs) provide a simple and elegant framework for representing probabilistic knowledge in logic programming. In this paper I consider the problem of learning ground LPADs starting from a set of interpretations annotated with their probability. I present the system ALLPAD for solving this problem. ALLPAD modifies the previous system LLPAD in order to tackle real world learning problems more effectively. This is achieved by looking for an approximate solution rather than a perfect one. ALLPAD has been tested on the problem of classifying proteins according to their tertiary structures and the results compare favorably...
A physical notice board with digital logic and display
- Nicolas Villar; Kristof Van Laerhoven; Hans Gellersen
A physical notice board is augmented with digital capabilities to provide additional functionality. The notice board retains its form factor, and when used with interactive pins with controllable lights it can be used to signal to the user information about the state of documents posted on the board. Both board and augmented pins are easy to deploy and cheap to produce.
Mechanizing Coinduction and Corecursion in Higher-order Logic
- Lawrence C. Paulson
A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least fixedpoints express inductive data types such as strict lists; greatest fixedpoints express coinductive data types, such as lazy lists. Wellfounded recursion expresses recursive functions over inductive data types; corecursion expresses functions that yield elements of coinductive data types. The theory rests on a traditional formalization of infinite trees. The theory is intended for use in specification and verification. It supports reasoning about a wide range of computable functions, but it does not formalize their operational semantics and can express noncomputable functions...
Weakly complete axiomatization of exogenous quantum propositional logic
- P. Mateus; A. Sernadas
A finitary axiomatization for EQPL (exogenous quantum propositional logic) is presented. The axiomatization is shown to be weakly complete relative to an oracle for analytical reasoning. The proof is carried out using a non trivial extension of the Fagin-Halpern-Megiddo technique together with three Henkin style completions. 1
Miss Scarlett in the Ballroom with the Lead Piping
- Clare Dixon
Abstract. Temporal logics of knowledge are useful for reasoningabout situations where the knowledge of an agent or component is important, and where change in this knowledge may occur over time.Here we use temporal logics of knowledge to reason about the game Cluedo. We show how to specify Cluedo using temporal logics ofknowledge and prove statements about the knowledge of the players using a clausal resolution calculus for this logic.
A complete and decidable logic for resource-bounded agents
- Natasha Alechina; Brian Logan; Mark Whitsey
We propose a context-logic style formalism, Timed Reasoning Logics (TRL), to describe resource-bounded reasoners who take time to derive consequences of their knowledge. The semantics of TRL is grounded in the agent’s computation, allowing an unambiguous ascription of the set of formulas which the agent actually knows at time t. We show that TRL can capture various rule application and conflict resolution strategies that a rule-based agent may employ, and analyse two examples in detail: TRL(STEP) which models an all rules at each cycle strategy similar to that assumed in step logic , and TRL(CLIPS) which models a single rule...
Overload Protection for CORBA Systems with Time Constraints
- Niklas Widell; Christian Nyberg; Maria Kihl
Scalable and reliable distributed object-oriented computing (DOC) middleware systems is an important technology in, for example, telecommunications service logic and distributed web servers. The Common Object Request Broker Architecture (CORBA), developed by the Object Management Group (OMG) is a specification of a common platform for DOC systems. CORBA acts as middleware, by inserting itself between the Operating System (OS) layer and the Application layer on a host. CORBA provides support for transparent interaction of objects situated on different nodes. The original CORBA specifications had no support for timing constraints in applications and very little support in the terms of performance...
Galois Connections in Categorial Type Logic Carlos Areces a;1;2 Raffaella Bernardi b;3 Michael Moortgat b;4
Abstract The introduction of unary connectives has proved to be an important addition to the categorial vocabulary. The connectives considered so far are order-preserving; in this paper instead, we consider the addition of order-reversing, Galois connected operators. In x2 we do the basic model-theoretic and proof-theoretic groundwork. In x3 we use the expressive power of the Galois connected operators to restrict the scopal possibilities of generalized quantifier expressions, and to describe a typology of polarity items. 1 Introduction Categorial type logic provides a vocabulary of logical constants for the assembly of form and meaning in natural language. The binary product...
Sufficient Conditions for Cut Elimination with Complexity Analysis
- João Rasga
Sufficient conditions for first order based sequent calculi to admit cut elimination by a Schütte-Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related with the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic modal logic S4, and classical and intuitionistic linear logic and some of its fragments. Moreover the conditions are...
1 Modal Change Logic (MCL): Specifying the Reasoning of Knowledge-based Systems
- Dieter Fensel; Rix Groenboom; G. R. Renardel De Lavalette
We investigate the formal specification of the reasoning process ofknowledge-based systems in this paper. We analyze the corresponding parts of the KADS specification languages KARL and (ML) 2 and deduce some generalrequirements. The essence of these languages is that they integrate a declarative specification of inferences with control information. The languages differ in theway they achieve this integration and each of them has shortcomings. We propose a unifying semantical framework that integrates the core of the different solutionsand overcomes their problems. We define a semantics and axiomatization with the
Translating Higher-Order Clauses to First-Order Clauses
- Jia Meng; Lawrence C. Paulson
Abstract. Interactive provers typically use higher-order logic, while automatic provers typically use first-order logic. In order to integrate interactive provers with automatic ones, it is necessary to translate higher-order formulae to first-order form. The translation should ideally be both sound and practical. We have investigated several methods of translating function applications, types and λ-abstractions. Omitting some type information improves the success rate, but can be unsound, so the interactive prover must verify the proofs. This paper presents experimental data that compares the translations in respect of their success rates for three automatic provers. 1.
CONGESTION CONTROL ACROSS A VIDEO-DOMINATED INTERNET TIGHT LINK
- E. A. Jammeh; M. Fleury; M. Ghanbari
Abstract: Existing congestion controllers have been designed with TCP traffic in mind. Changing traffic patterns on the Internet imply that on some tight links all UDP video streams will occur. Three different congestion controllers (RAP, TFRC, and fuzzy-logic based), already successful in avoiding instability in current TCPdominated internets, were tested across a tight link in which video traffic dominated. Congestion control is either achieved by modulating the sending rate in response to feedback of packet loss rates and/or round-trip delays (RAP/TFRC) or a congestion level based on packet dispersion across a network path (fuzzy controller). The controllers were found to...
Fundamenta Informaticae AAA 1–35 1 IOS Press Agents that Know How to Play
- Wojciech Jamroga; Wiebe Van Der Hoek
Abstract. We look at ways to enrich Alternating-time Temporal Logic (ATL) – a logic for specification and verification of multi-agent systems – with a notion of knowledge. Starting point of our study is a recent proposal for a system called Alternating-time Temporal Epistemic Logic (ATEL). We show that, assuming that agents act under uncertainty in some states of the system, the notion of allowable strategy should be defined with some caution. Moreover, we demonstrate a subtle difference between an agent knowing that he has a suitable strategy and knowing the strategy itself. We also point out that the agents should...
An observationally complete program logic for imperative higher-order functions
- Kohei Honda; Nobuko Yoshida; Martin Berger
Abstract. We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A systematic use of names and operations on them allows precise and general description of complex higher-order imperative behaviour. The proof rules of the logic exactly follow the syntax of the language and can cleanly embed, justify and extend the standard proof rules for total correctness of Hoare logic. The logic offers a foundation for general treatment of aliasing and local state on its basis, with minimal extensions. After establishing...
Algebraic theories for contextual pre-nets ⋆
- Roberto Bruni; José Meseguer; Ugo Montanari; Vladimiro Sassone
Abstract. The algebraic models of computation for contextual nets that have been proposed in the literature either rely on a non-free monoid of objects, or introduce too many fictitious behaviors that must be somewhat filtered out. In this paper, we exploit partial membership equational logic to define a suitable theory of models, where the meaningful concurrent computations can be selected by means of membership predicates. 1
Bistructures, bidomains and linear logic
- Pierre-louis Curien
Bistructures are a generalisation of event structures which allow a representation of spaces of functions at higher types in an orderextensional setting. The partial order of causal dependency is replaced by two orders, one associated with input and the other with output in the behaviour of functions. Bistructures form a categorical model of Girard’s classical linear logic in which the involution of linear logic is modelled, roughly speaking, by a reversal of the roles of input and output. The comonad of the model has an associated co-Kleisli category which is closely related to that of Berry’s bidomains (both have equivalent...
Reasoning about action and cooperation
- Luigi Sauro; Jelle Gerbrandy
We present a logic for reasoning both about the ability of agents to cooperate to execute complex actions, and how this relates to their ability to reach certain states of affairs. We show how the logic can be obtained in a modularised way, by combining a model for reasoning about actions and their effects with a model that describes what actions an agent can perform. More precisely, we show how one can combine an action logic which resembles Propositional Dynamic Logic with a cooperation logic which resembles Coalition Logic. We give a sound and complete axiomatisation for the logic, illustrate...
A logic of authentication
- Michael Burrows; Mart Abadi; Roger Needham
Questions of belief are essential in analyzing protocols for the authentication of principals in distributed computing systems. In this paper we motivate, set out, and exemplify a logic speci cally designed for this analysis; we show howvarious protocols di er subtly with respect to the required initial assumptions of the participants and their nal beliefs. Our formalism has enabled us to isolate and express these di erences with a precision that was not previously possible. It has drawn attention to features of protocols of which we and their authors were previously unaware, and allowed us to suggest improvements to the...
Rethinking Semantics of Dynamic Logic Programming
A dynamic logic program represents an evolving knowledge base. Research in the field is dominated by the causal rejection principle: the conflicting rule from the less preferred program is rejected in the case of conflict. Some drawbacks of the causal rejection principle (irrelevant updates, inconsistencies which cannot be solved according to the causal rejection principle, disagreement with other fields relevant for updates of nonmonotonic knowledge bases such as belief revision or preferences handling) are identified and discussed in the paper. The discussion of those drawbacks pointed out the role of assumptions and dependencies on assumptions for a careful attitude to...
Compositionality of Hennessy-Milner logic through structural operational semantics
- Wan Fokkink; Rob Van Glabbeek; Paulien De Wind
Abstract. This paper presents a method for the decomposition of HML formulae. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulae, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is that an earlier decomposition method from Larsen  for the De Simone format is extended to the more general ntyft/ntyxt format without lookahead. 1