A Critical Examination of the Cohen-Levesque Theory of Intentions
- Munindar P. Singh
. We examine the formal theory of intentions recently proposed by Cohen & Levesque . We evaluate the assumptions made by this theory and their consequences relative to fairly general intuitions about intentions, especially as they are applied in AI domains. We show that the theory is conceptually problematic and that certain technical claims made by the authors are false or counterintuitive in most natural scenarios. Keywords: intentions, logic in AI. 1 Introduction It is of great use to a scientific discipline when its theories are critically examined and their unstated assumptions, and the unexpected consequences of their explicit assumptions,...
Specifying Performance Measures for PEPA
- Graham Clark; Stephen Gilmore; Jane Hillston
. Stochastic process algebras such as PEPA provide ample support for the component-based construction of models. Tools compute the numerical solution of these models; however, the stochastic process algebra methodology lacks support for the specification and calculation of complex performance measures. This paper addresses that problem by presenting a performance specification language which supports high level reasoning about PEPA models, allowing the description of equilibrium (steady-state) measures. The meaning of the specification language can be made formal by examining its foundations in a stochastic modal logic. A case-study is presented to illustrate the approach. 1 Introduction Performance Evaluation Process Algebra...
Beth Definability for the Guarded Fragment
- Eva Hoogland; Maarten Marx; Martin Otto
. The guarded fragment (GF) was introduced in [ABN98] as a fragment of first order logic which combines a great expressive power with nice modal behavior. It consists of relational first order formulas whose quantifiers are relativized by atoms in a certain way. While GF has been established as a particularly well-behaved fragment of first order logic in many respects, interpolation fails in restriction to GF, [HM99]. In this paper we consider the Beth property of first order logic and show that, despite the failure of interpolation, it is retained in restriction to GF. Being a closure property w.r.t. definability,...
An Empirical Evaluation of Optimization Strategies for ABox Reasoning in Expressive Description Logics
- Volker Haarslev; Ralf Möller
This paper presents an evaluation of a new description logic reasoner called RACE which implements TBox and ABox reasoning for the description logic ALCNH_R+ supporting number restrictions, role hierarchies, and transitively closed roles. Tests on benchmark ABoxes indicate a speedup of several orders of magnitude compared to previous systems.
Specifying and Enforcing Intertask Dependencies
- Paul Attie Munindar; Paul C. Attie; Munindar P. Singh; Amit Sheth; Marek Rusinkiewicz
Extensions of the traditional atomic transaction model are needed to support the development of multi-system applications or workflows that access heterogeneous databases and legacy application systems. Most extended transaction models use conditions involving events or dependencies between transactions. Intertask dependencies can serve as a uniform framework for defining extended transaction models. In this paper, we introduce event attributes needed to determine whether a dependency is enforceable and to properly schedule events in extended transaction models. Using these attributes and a formalization of a dependency into the temporal logic CTL, we can automatically synthesize an automaton that captures the computations that...
On Negation as Instantiation
- Alessandra Di Pierro; Wlodzimierz Drabent; Ra Di Pierro; S Linkoping
Given a logic program P and a goal G, we introduce a notion which states when an SLD-tree for P [ fGg instantiates a set of variables V with respect to another one, W . We call this notion weak instantiation, as it is a generalisation of the instantiation property introduced by Di Pierro, Martelli and Palamidessi. A negation rule based on instantiation, the so-called Negation As Instantiation rule (NAI), allows for inferring existentially closed negative queries, that is formulas of the form 9:Q, from logic programs. We show that, by using the new notion, we can infer a larger...
On the Completeness of Propositional Hoare Logic
- Dexter Kozen; Jerzy Tiuryn
. We investigate the completeness of Hoare logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness result for propositional Hoare logic (PHL): all relationally valid rules fb1g p1 fc1g; : : : ; fbng pn fcng fbg p fcg are derivable in PHL, provided the propositional expressiveness conditions are met. Moreover, if the programs p i in the premises are atomic, no expressiveness assumptions are needed. 1 Introduction As shown by Cook , Hoare logic is relatively complete for partial correctness assertions (PCAs) over while programs whenever the underlying...
Exploiting Modal Logic to Express Performance Measures
- Graham Clark; Stephen Gilmore; Jane Hillston; Marina Ribaudo
Stochastic process algebras such as PEPA provide ample support for the component-based construction of models. Tools compute the numerical solution of these models; however, the stochastic process algebra methodology has lacked support for the specification and calculation of complex performance measures. In this paper we present a stochastic modal logic which can aid the construction of a reward structure over the model. We discuss its relationship to the underlying theory of PEPA. We also present a performance specification language which supports high level reasoning about PEPA models, and allows queries about the equilibrium behaviour. The meaning of the specification language...
A PSpace-algorithm for ALCQI-satisfiability
- Stephan Tobies
The description logic ALCQI extends the "standard" description logic ALC by qualifying number restrictions and converse roles. We show that concept satisfiability for this DL is still decidable in polynomial space. The presented algorithm combines techniques from [Tob99] to deal with qualifying number restrictions and from [HST99] to deal with converse roles.
A Description Logic with Transitive and Converse Roles, Role Hierarchies and Qualifying Number Restrictions
- Ian Horrocks; Ulrike Sattler; Stephan Tobies
From Fuzzy Values to Intuitionistic Fuzzy Values to Intuitionistic Fuzzy Intervals etc.: Can We Get an Arbitrary Ordering?
- Vladik Kreinovich; Masao Mukaidono; Krassimir Atanassov
Traditional fuzzy logic uses real numbers as truth values. This description is not always adequate, so in intuitionistic fuzzy logic, we use pairs of real numbers to describe a truth value. Such pairs can be described either as pairs (t; f) for which t + f 1, or, alternatively, as pairs (t; 1 \Gamma f) for which t 1 \Gamma f . To make this description even more adequate, instead of using real numbers to described each value t and f , we can use intervals, and thus get interval-valued intuitionistic fuzzy values which can be described by 4 real...
ILP with Noise and Fixed Example Size: A Bayesian Approach
- Eric Mccreath; Arun Sharma
Current inductive logic programming systems are limited in their handling of noise, as they employ a greedy covering approach to constructing the hypothesis one clause at a time. This approach also causes difficulty in learning recursive predicates. Additionally, many current systems have an implicit expectation that the cardinality of the positive and negative examples reflect the "proportion" of the concept to the instance space. A framework for learning from noisy data and fixed example size is presented. A Bayesian heuristic for finding the most probable hypothesis in this general framework is derived. This approach evaluates a hypothesis as a whole...
Planning for Temporally Extended Goals
- Fahiem Bacchus; Froduald Kabanza
In planning, goals have been traditionally been viewed as specifying a set of desirable final states. Any plan that transforms the current state to one of these desirable states is viewed to be correct. Goals of this form are limited as they do not allow us to constrain the manner in which the plan achieves its objectives. We propose viewing goals as specifying desirable sequences of states, and a plan to be correct if its execution yields one of these desirable sequences. We present a logical language, a temporal logic, for specifying goals with this semantics. Our language is rich...
Proofs as Discourse: An Empirical Study
- Jon Oberlander; Richard Cox; Keith Stenning
Computer-based logic proofs are a form of `unnatural' language discourse, but the structure and process of proof can be observed in considerable detail, and analysis is leading to a number of general insights. We have been studying how students respond to multimodal logic teaching. First, psychological measures indicate that students' pre-existing cognitive styles have a significant impact on teaching outcome. Secondly, a large corpus of proofs has been gathered via automatic logging of proof development. Frequency analysis and cluster analysis of this corpus indicate that students' cognitive styles influence the structure of their logical discourse. Our current objective is to...
Phonological Analysis in Typed Feature Systems
- Steven Bird; Ewan Klein
this paper we suggest some strategies for reuniting phonology and the rest of grammar in the context of a uniform constraint formalism. We explain why this is a desirable goal, and we present some conservative extensions to current practice in computational linguistics and in non-linear phonology which we believe are necessary and sufficient for achieving this goal. We begin by exploring the application of typed feature logic to phonology and propose a system of prosodic types. Next, taking HPSG as an exemplar of the grammar frameworks we have in mind, we show how the phonology attribute can be enriched, so...
The Use of Static Constructs in A Modal Process Logic
- Hans Hüttel; Kim G. Larsen
this paper we want to demonstrate that --- from a practical
A PSPACE-algorithm for deciding ALCNI_R+-satisfiability
- Ian Horrocks; Ulrike Sattler; Stephan Tobies
ALCNI R +---ALCNaugmented with transitive and inverse roles---is an expressive Description Logic which is especially well-suited for the representation of complex, aggregated objects. Despite its expressiveness, it has been conjectured that concept satisfiability for this logic could be decided in a comparatively efficient way. In this paper we prove the correctness of this conjecture by presenting a PSPACE algorithm for deciding satisfiability and subsumption of ALCNI R +-concepts. The space-efficiency of this tableaubased algorithm is due to a sophisticated guidance of the search for a solution. Moreover, this space-efficiency is not paid for with time-consumption; on the contrary, the guidance...
Safety for Bisimulation in Monadic Second-Order Logic
- Marco Hollenberg
We characterize those formulas of MSO (monadic second-order logic) that are safe for bisimulation: formulas defining binary relations such that any bisimulation is also a bisimulation with respect to these defined relations. Every such formula is equivalent to one constructed from ¯- calculus tests, atomic actions and the regular operations. The proof uses a characterization of completely additive ¯-calculus formulas: formulas OE(p) that distribute over arbitrary unions. It turns out that complete additivity is equivalent to distributivity over countable unions. For FOL (first-order logic) a similar theorem is shown (giving an alternative proof to the original of ). Here though...
A Description Logic with Transitive and Converse Roles and Role Hierarchies
- Ian Horrocks; Ulrike Sattler
Expressive ABox Reasoning with Number Restrictions, Role Hierarchies, and Transitively Closed Roles
- Volker Haarslev; Volker Haarslev; Rolf Möller; Ralf Moller
We present a new tableaux calculus deciding the ABox consistency problem for the expressive description logic ALCNH R + . Prominent language features of ALCNH R + are number restrictions, role hierarchies, transitively closed roles, and generalized concept inclusions.