An Equational Axiomatization of Dynamic Negation and Relational Composition

We consider algebras on binary relations with two main operators: relational composition and dynamic negation. Relational composition has its standard interpretation, while dynamic negation is an operator familiar to students of Dynamic Predicate Logic (DPL) (Groenendijk and Stokhof, 1991): given a relation R its dynamic negation R is a test that contains precisely those pairs (s,s) for which s is not in the domain of R. These two operators comprise precisely the propositional part of DPL.This paper contains a finite equational axiomatization for these dynamic relation algebras. The completenessresult uses techniques from modal logic. We also lookat the variety generated by the class of dynamic relation algebras and note that there exist nonrepresentable algebras in this variety, ones which cannot be construedas spaces of relations. These results are also proved for an extension to a signature containing atomic tests and union.     

Temporalizing Epistemic Default Logic

We present an epistemic default logic, based on the metaphore of a meta-level architecture. Upward reflection is formalized by a nonmonotonic entailment relation, based on the objective facts that are either known or unknown at the object level. Then, the meta (monotonic) reasoning process generates a number of default-beliefs of object-level formulas. We extend this framework by proposing a mechanism to reflect these defaults down. Such a reflection is seen as essentially having a temporal flavour: defaults derived at the meta-level are projected as facts in a next object level state. In this way, we obtain temporal models for default reasoning in meta-level formalisms which can be conceived as labeled branching trees. Thus, descending the tree corresponds to shifts in time that model downward reflection, whereas the branching of the tree corresponds to ways of combining possible defaults. All together, this yields an operational or procedural semantics of reasoning by default, which admits one to reason about it by means of branching-time temporal logic. Finally, we define sceptical and credulous entailment relations based on these temporal models and we characterize Reiter extensions in our semantics.     

From event calculus to the scheduling problem. Semantics of action and temporal reasoning in aircraft maintenance

In this work we are interested in the logical and semantical aspects of reasoning about actions in a scheduling process. We present an adaptation of the event calculus of Kowalski and Sergot to the problem of determining the temporal structure of the operations that must be performed during the realization of some complex objectives. Our application domain is aircraft maintenance. We try to reason about the actions which are performed during an overhaul in order to help to schedule them. The original model reasons about changes, i.e. events which initiate or terminate propositions. The first step of this work was to improve the initial model by adding a temporal relation between events and propositions because in our field we also have to reason about events which only inform us about some propositions without affecting them. The second step of this work is to build a set of specific rules which temporally interpret the semantics of the usual specifications of the actions to be considered. This interpretation aims to associate each action with two events and some temporal relations which are usable by the general model. Temporal reasoning uses pertinent knowledge about the specific universe (here, the aircraft that we consider and the actions which may be performed on it). We outline a generative methodology to formalize this relevant knowledge efficiently. This cognitive approach brings more informational economy in temporal reasoning because only the relevant information is considered The temporal reasoning model and the methodology have been exemplified and tested on a complex part of an aircraft. In the future, adapted tools based on this approach will be developed, in order to solve several problems of aircraft maintenance scheduling.     

The Objective Conception of Context and Its Logic

In this paper, an objective conception of contexts based loosely upon situation theory is developed and formalized. Unlike subjective conceptions, which take contexts to be something like sets of beliefs, contexts on the objective conception are taken to be complex, structured pieces of the world that (in general) contain individuals, other contexts, and propositions about them. An extended first-order language for this account is developed. The language contains complex terms for propositions, and the standard predicate ist that expresses the relation that holds between a context and a proposition just in case the latter is true in the former. The logic for the objective conception features a global classical predicate calculus, a local logic for reasoning within contexts, and axioms for propositions. The specter of paradox is banished from the logic by allowing ist to be nonbivalent in problematic cases: it is not in general the case, for any context c and proposition p, that either ist(c,p) or ist(c, ¬ p). An important representational capability of the logic is illustrated by proving an appropriately modified version of an illustrative theorem from McCarthy's classic Blocks World example.     

The rest stays unchanged (concurrency and state-based specification)

Pre-/postconditions have been extensively used in program specification, e.g. Z [Spi89], VDM [Jon86], and proof, e.g. Hoare logic, Dijkstra's guarded commands [DiF88]. In [ScP86, SPB90] the authors introduced neutral and central relations to formalise the concept of the rest stays the same. In this paper we abstract away from the specific definition of neutral relation given in [SPB90], through the mechanism of relational boolean algebras. This leads to the definition of implicitly central relations which are easier for the user in practical examples and facilitate the use of pre-/postcondition reasoning about truly concurrent behaviour.     

On the complemented disk algebra

The importance of relational methods in temporal and spatial reasoning has been widely recognised in the last two decades. A quite large part of contemporary spatial reasoning is concerned with the research of relation algebras generated by the “part of” and “connection” relations in various domains. This paper is devoted to the study of one particular relation algebra appeared in the literature, viz. the complemented disk algebra. This algebra was first described by Düntsch [I. Düntsch, A tutorial on relation algebras and their application in spatial reasoning, Given at COSIT, August 1999, Available from: <http://www.cosc.brocku.ca/~duentsch/papers/relspat.html>] and then, Li et al. [Y. Li, S. Li, M. Ying, Relational reasoning in the Region Connection Calculus, Preprint, 2003, Available from: http://arxiv.org/abs/cs/0505041] showed that closed disks and their complements provides a representation. This set of regions is rather restrictive and, thus, of limited practical values. This paper will provide a general method for generating representations of this algebra in the framework of Region Connection Calculus. In particular, connected regions bounded by Jordan curves and their complements is also such a representation.     

Temporal relational data model

This paper incorporates a temporal dimension to nested relations. It combines research in temporal databases and nested relations for managing the temporal data in nontraditional database applications. A temporal data value is represented as a temporal atom; a temporal atom consists of two parts: a temporal set and a value. The temporal atom asserts that the value is valid over the time duration represented by its temporal set. The data model allows relations with arbitrary levels of nesting and can represent the histories of objects and their relationships. Temporal relational algebra and calculus languages are formulated and their equivalence is proved. Temporal relational algebra includes operations to manipulate temporal data and to restructure nested temporal relations. Additionally, we define operations to generate a power set of a relation, a set membership test, and a set inclusion test, which are all derived from the other operations of temporal relational algebra. To obtain a concise representation of temporal data (temporal reduction), collapsed versions of the set-theoretic operations are defined. Procedures to express collapsed operations by the regular operations of temporal relational algebra are included. The paper also develops procedures to completely flatten a nested temporal relation into an equivalent 1 NF relation and back to its original form, thus providing a basis for the semantics of the collapsed operations by the traditional operations on 1 NF relations     

Dual Grid: A New Approach for Robust Spatial Algebra Implementation

Systems of spatial data types and operations, or spatial algebras, are fundamental for the implementation of spatial database systems. Several designs of such algebras have been proposed in the last decade, and recently commercial DBMS offer such algebras in the form of extension packages (e.g., data blades). However, actual implementations are generally severely restricted when compared to designs in the literature. A main reason is that at the implementation level one cannot further ignore the problems of robustness and topological correctness arising from the discrete number representations used in computers. Therefore, implemented packages either avoid problematic operations, or accept inconsistencies and topological errors in the answers of queries due to rounding effects.The ROSE algebra [12], proposed and implemented earlier, goes a long way towards avoiding such problems, since it was defined from scratch with robustness problems in mind. It is founded on a discrete geometric basis called a realm. The ROSE algebra guarantees a correct behavior of operations and has an entirely robust implementation. Unfortunately, the realm concept and its interaction with DBMS are difficult to implement, and certain kinds of topological problems still remain.In this paper we introduce the concept of dual grid, which provides a new approach for the representation of spatial information that avoids any robustness and topological correctness problem and allows a less restrictive implementation of spatial algebras. As an example, we show how can it be used for implementing the ROSE algebra without realms, and show that such an implementation does not suffer from the side effects and disadvantages of the original realm-based one.     

Modal nonmonotonic logics demodalized

The study of the relation between default logic and modal nonmonotonic logics has been mostly concerned with the task of translating default logic to autoepistemic or some other modal nonmonotonic logic. Here, we discuss the reverse problem, that is, the possibility of translating modal nonmonotonic logics into default-type systems formulated in the language without modal operators. To this end, we first consider a reformulation of both formalisms in terms of what we call default consequence relations. These consequence relations turn out to be especially suitable for studying default and modal nonmonotonic reasoning. We show, in particular, that different kinds of such reasoning naturally correspond to different structural rules imposed on default consequence relations. Our main results also demonstrate that all modal nonmonotonic objects considered have exact nonmodal counterparts. As an immediate consequence of these results, we obtain a method of reducing common types of modal nonmonotonic reasoning to nonmodal default reasoning.     

Real-time model based geometric reasoning for vision-guided navigation

This paper describes results of a real-time model based geometric reasoning module for autonomous vision-guided road following. Vision-guided road following requires extracting road boundaries from images in real time to guide the navigation of autonomous vehicles on a roadway. The detected road region boundary is error prone due to imperfect image segmentation. To achieve robust system performance, a geometric reasoning module that uses spatial and temporal constraints to perform model based reasoning is used. Local geometric supports for each road edge segment are collected and recorded and a global consistency checking is performed to obtain a consistent interpretation of the raw data. Cases involving incomplete sensor data, curved roads where only one side of the road is visible, and incorrect segmentation due to shadows, road patches, or unusual road conditions, can usually be detected and corrected. The image segmentation results are what the vision system sees. The geometric reasoning results are what the vision system perceives. This reasoning module has been integrated into a road following system which is capable of supporting autonomous robot road following at 24 km/hr.     

Resource-Bounded Paraconsistent Inference

In this paper, a new framework for reasoning from inconsistent propositional belief bases is presented. A family of resource-bounded paraconsistent inference relations is introduced. Such inference relations are based on S-3 entailment, an inference relation logically weaker than the classical one and parametrized by a set S of propositional variables. The computational complexity of our relations is identified, and their logical properties are analyzed. Among the strong features of our framework is the fact that tractability is ensured each time |S| is bounded and a limited amount of knowledge is taken into account within the belief base. Furthermore, binary connectives , behave in a classical manner. Finally, our framework is general enough to encompass several paraconsistent multi-valued logics (including S-3, J ₃ and its restrictions), the standard coherence-based approach to inconsistency handling (based on the selection of consistent subbases) and some signed systems for paraconsistent reasoning as specific cases.     

VVSL: A language for structured VDM specifications

VVSL is a VDM specification language of the British School with modularisation constructs allowing sharing of hidden state variables and parameterisation constructs for structuring specifications, and with constructs for expressing temporal aspects of the concurrent execution of operations which interfere via state variables. The modularisation and parameterisation constructs have been inspired by the kernel design language COLD-K from the ESPRIT project 432: METEOR, and the constructs for expressing temporal aspects by various temporal logics based on linear and discrete time. VVSL is provided with a well-defined semantics by defining a translation to COLD-K extended with constructs which are required for translation of the VVSL constructs for expressing temporal aspects.In this paper, the syntax for the modularisation and parameterisation constructs of VVSL is outlined. Their meaning is informally described by giving an intuitive explanation and by outlining the translation to COLD-K. It is explained in some detail how sharing of hidden state variables is modelled. Examples of the use of the modularisation and parameterisation constructs are also given. These examples are based on a formal definition of the relational data model. With respect to the constructs for expressing temporal aspects, the ideas underlying the use of temporal formulae in VVSL are briefly outlined and a simple example is given.     

Reasoning about networks of temporal relations and its applications to problem solving

An interval algebra (IA) has been proposed as a model for representing and reasoning about qualitative temporal relations between time intervals. Unfortunately, reasoning tasks with IA that involve deciding the satisfiability of the temporal constraints, or providing all the satisfying instances of the temporal constraints, areNP-complete. That is, solving these problems are computationally exponential in the worst case. However, several directions in improving their computational performance are still possible. This paper presents a new backtracking algorithm for finding a solution called consistent scenario. This algorithm has anO(n ³) best-case complexity, compared toO(n ⁴) of previous known backtrack algorithms, wheren denotes the number of intervals. By computational experiments, we tested the performance of different backtrack algorithms on a set of randomly generated networks with the results favoring our proposal. In this paper, we also present a new path consistency algorithm, which has been used for finding approximate solutions towards the minimal labeling networks. The worst-case complexity of the proposed algorithm is stillO(n ³); however, we are able to improve its performance by eliminating the unnecessary duplicate computation as presented in Allen's original algorithm, and by employing a most-constrained first principle, which ensures a faster convergence. The performance of the proposed scheme is evaluated through a large set of experimental data.     

Priority as extremal probability

We extend the stratified model of probabilistic processes to obtain a very general notion ofprocess priority. The main idea is to allow probability guards of value 0 to be associated with alternatives of a probabilistic summation expression. Such alternatives can be chosen only if the non-zero alternatives are precluded by contextual constraints. We refer to this model as one of extremal probability and to its signature asPCCS . We providePCCS with a structural operational semantics and a notionof probabilistic bisimulation, which is shown to be a congruence. Of particular interest is the abstractionPCCS ofPCCS in which all non-zero probability guards are identified.PCCS represents a customized framework for reasoning about priority, and covers all features of process algebras proposed for reasoning about priority that we know of.A preliminary version of this paper appeared inProceedings of CONCUR '90 — First International Conference on Concurrency Theory, Vol. 458 of the Springer-Verlag seriesLecture Notes in Computer Science, pp. 456–466, Aug. 1990. The research of Scott Smolka was supported in part by NSF Grants CCR-9120995, CCR-9208585 and CCR-9505562; and AFOSR Grants F49620-93-1-0250, F49620-95-1-0508 and F49620-96-1-0087.     

A treatment of plurals and plural quantifications based on a theory of collections

Collective entities and collective relations play an important role in natural language. In order to capture the full meaning of sentences like The Beatles sing Yesterday, a knowledge representation language should be able to express and reason about plural entities — like the Beatles — and their relationships — like sing — with any possible reading (cumulative, distributive or collective).In this paper a way of including collections and collective relations within a concept language, chosen as the formalism for representing the semantics of sentences, is presented. A twofold extension of theA–C concept language is investigated: (1) special relations introduce collective entities either out of their components or out of other collective entities, (2) plural quantifiers on collective relations specify their possible reading. The formal syntax and semantics of the concept language is given, together with a sound and complete algorithm to compute satisfiability and subsumption of concepts, and to compute recognition of individuals.An advantage of this formalism is the possibility of reasoning and stepwise refining in the presence of scoping ambiguities. Moreover, many phenomena covered by the Generalized Quantifiers Theory are easily captured within this framework. In the final part a way to include a theory of parts (mereology) is suggested, allowing for a lattice-theoretical approach to the treatment of plurals.     

Qualitative Spatial Reasoning with Conceptual Neighborhoods for Agent Control

Research on qualitative spatial reasoning has produced a variety of calculi for reasoning about orientation or direction relations. Such qualitative abstractions are very helpful for agent control and communication between robots and humans. Conceptual neighborhood has been introduced as a means of describing possible changes of spatial relations which e.g. allows action planning at a high level of abstraction. We discuss how the concrete neighborhood structure depends on application-specific parameters and derive corresponding neighborhood structures for the calculus. We demonstrate that conceptual neighborhoods allow resolution of conflicting information by model-based relaxation of spatial constraints. In addition, we address the problem of automatically deriving neighborhood structures and show how this can be achieved if the relations of a calculus can be modeled in another calculus for which the neighborhood structure is known.     

Mathematical modelling of processes in mechanics

Mathematical modelling processes are computed by the path following method from the literature. A new approximation is presented using parametrical optimization. The problems are solved as nonlinear programming problems by converting the problem from the function space into the ² space.     

Computable processes and bisimulation equivalence

A process is calledcomputable if it can be modelled by a transition system that has a recursive structure—implying finite branching. The equivalence relation between transition systems considered is strong bisimulation equivalence. The transition systems studied in this paper can be associated to processes specified in common specification languages such as CCS, LOTOS, ACP and PSF. As a means for defining transition systems up to bisimulation equivalence, the specification languageCRL is used. Two simple fragments of,CRL are singled out, yielding universal expressivity with respect to recursive and primitive recursive transition systems. For both these domains the following properties are classified in the arithmetical hierarchy:bisimilarity, perpetuity (both ₁ ⁰ ),regularity (having a bisimilar, finite representation, ₂ ⁰ ),acyclic regularity ( ₁ ⁰ ), anddeadlock freedom (distinguishing deadlock from successful termination, ₁ ⁰ ). Finally, it is shown that in the domain of primitive recursive transition systems over a fixed, finite label set, a genuine hierarchy in bisimilarity can be defined by the complexity of the witnessing relations, which extends r.e. bisimilarity. Hence, primitive recursive transition systems already form an interesting class.     

A model for pattern perception with musical applications part II: The information content of pitch structures

This is the second paper of a series which begins by treating the perception of pitch relations in musical contexts and the perception of timbre and speech. The first paper discusses in some detail those properties of musical scales required in order for them to function as reference frames which provide for the measurement of intervals such that ([1], p. 270),Every melodic phrase, every chord, which can be executed at any pitch, can be also executed at any other pitch in such a way that we immediately perceive the characteristic marks of their similarity. Here we continue this discussion by developing quantitative measures of the degree to which different scales possess the above properties. Then that property of musical scales which permits a listener to code the pitches of which it is constituted into degrees is examined and a corresponding quantitative measure developed. Musical scales are shown to be optimal choices with respect to both the former and latter measures, and a theory limiting those scales which are musically useful to a small fraction of possible sets of pitches is proposed. Existing scales which have been examined fall within the theory, which links the techniques of composition which may be used (i.e., those which produce perceptible relations between musical segments) to the above properties of the scale structures. This paper is not self-contained—reading of the previous paper in this series is required.This research was supported in part by grants and contracts AF-AFOSR 881-65, AF 49(638)-1738 and AF-AFOSR 68-1596.     

A graphical approach to relational reasoning

Relational reasoning is concerned with relations over an unspecified domain of discourse. Two limitations to which it is customarily subject are: only dyadic relations are taken into account; all formulas are equations, having the same expressive power as first-order sentences in three variables. The relational formalism inherits from the Peirce-Schröder tradition, through contributions of Tarski and many others.Algebraic manipulation of relational expressions (equations in particular) is much less natural than developing inferences in first-order logic; it may in fact appear to be overly machine-oriented for direct hand-based exploitation.The situation radically changes when one resorts to a convenient representation of relations based on labeled graphs. The paper provides details of this representation, which abstracts w.r.t. inessential features of expressions.Formal techniques illustrating three uses of the graph representation of relations are discussed: one technique deals with translating first-order specifications into the calculus of relations; another one, with inferring equalities within this calculus with the aid of convenient diagram-rewriting rules; a third one with checking, in the specialized framework of set theory, the definability of particular set operations. Examples of use of these techniques are produced; moreover, a promising approach to mechanization of graphical relational reasoning is outlined.