On the finite and general implication problems of independence atoms and keys

We investigate implication problems for keys and independence atoms in relational databases. For keys and unary independence atoms we show that finite implication is not finitely axiomatizable, and establish a finite axiomatization for general implication. The same axiomatization is also sound and complete for finite and general implication of unary keys and independence atoms, which coincide. We show that the general implication of keys and unary independence atoms and of unary keys and general independence atoms is decidable in polynomial time. For these two classes we also show how to construct Armstrong relations. Finally, we establish tractable conditions that are sufficient for certain classes of keys and independence atoms not to interact.     

Axiomatizing the Logical Core of XPath 2.0

The first aim of this paper is to present the logical core of XPath 2.0: a logically clean, decidable fragment, which includes most navigational features of XPath 2.0 (complex counting conditions and data joins are not supported, as they lead to undecidability). The second aim is to provide a list of equations completely axiomatizing query equivalence in this language (i.e., all other query equivalences can be derived from these). A preliminary version of this paper was published in the proceedings of ICDT 2007. We would like to thank Jan Hidders for pointing us to the interesting question of stronger forms of completeness (cf. Sect. 4.3). We would also like to thank the anonymous reviewers for their extensive comments, which have greatly improved the quality of the paper. The first author is supported by NWO grant 639.021.508.     

XML数据库计划的公理化演进

数据库计划是由它的实体之间的模式关系构成, 该计划随着时间的改变被称为计划演进。XML 数据库计划的公理化演进指的是当该计划产生根本的变动时, XML 数据库能自动维持其数据的完整性。提出的公理化模式为XML 数据库演进的问题提供了一个一般的解决方案, 它能明确地决定计划的修改行为和自动维持其数据的完整性。     

A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle

We use the interactive theorem prover Isabelle to prove that the algebraic axiomatization of bisimulation equivalence in the pi-calculus is sound and complete. This is the first proof of its kind to be wholly machine checked. Although the result has been known for some time the proof had parts which needed careful attention to detail to become completely formal. It is not that the result was ever in doubt; rather, our contribution lies in the methodology to prove completeness and get absolute certainty that the proof is correct, while at the same time following the intuitive lines of reasoning of the original proof. Completeness of axiomatizations is relevant for many variants of the calculus, so our method has applications beyond this single result. We build on our previous effort of implementing a framework for the pi-calculus in Isabelle using the nominal data type package, and strengthen our claim that this framework is well suited to represent the theory of the pi-calculus, especially in the smooth treatment of bound names.     

Metrics for weighted transition systems: Axiomatization and complexity

Simulation distances are essentially approximations of simulation which provide a measure of the extent by which behaviors in systems are inequivalent. In this paper, we consider the general quantitative model of weighted transition systems, where transitions are labeled with elements of a finite metric space. We study the so-called point-wise and accumulating simulation distances which provide extensions to the well-known Boolean notion of simulation on labeled transition systems.We introduce weighted process algebras for finite and regular behavior and offer sound and (approximate) complete inference systems for the proposed simulation distances. We also settle the algorithmic complexity of computing the simulation distances.     

Verification of mobile ad hoc networks: An algebraic approach

We introduced Computed Network Process Theory to reason about protocols for mobile ad hoc networks (MANETs). Here we explore the applicability of our framework in two regards: model checking and equational reasoning. The operational semantics of our framework is based on constrained labeled transition systems (CLTSs), in which each transition label is parameterized with the set of topologies for which this transition is enabled. We illustrate how through model checking on CLTSs one can analyze mobility scenarios of MANET protocols. Furthermore, we show how by equational theory one can reason about MANETs consisting of a finite but unbounded set of nodes, in which all nodes deploy the same protocol. Model checking and equational reasoning together provide us with an appropriate framework to prove the correctness of MANETs. We demonstrate the applicability of our framework by a case study on a simple routing protocol.     

Three fundamental misconceptions of Artificial Intelligence

In discussions on the limitations of Artificial Intelligence (AI), there are three major misconceptions, identifying an AI system with an axiomatic system, a Turing machine, or a system with a model-theoretic semantics. Though these three notions can be used to describe a computer system for certain purposes, they are not always the proper theoretical notions when an AI system is under consideration. These misconceptions are not only the basis of many criticisms of AI from the outside, but also responsible for many problems within AI research. This paper analyses these misconceptions, and points out the common root of them: treating empirical reasoning as mathematical reasoning. Finally, an example intelligent system called NARS is introduced, which is neither an axiomatic system nor a Turing machine in its problem-solving process, and does not use model-theoretic semantics, but is still implementable in an ordinary computer.     

Ready to preorder: an algebraic and general proof

There have been quite a few proposals for behavioural equivalences for concurrent processes, and many of them are presented in Van Glabbeek’s linear time-branching time spectrum. Since their original definitions are based on rather different ideas, proving general properties of them all would seem to require a case-by-case study. However, the use of their axiomatizations allows a uniform treatment that might produce general proofs of those properties. Recently Aceto, Fokkink and Ingólfsdóttir have presented a very interesting result: for any process preorder coarser than the ready simulation in the linear time-branching time spectrum they show how to get an axiomatization of the induced equivalence. Unfortunately, their proof is not uniform and requires a case-by-case analysis. Following the algebraic approach suggested above, in this paper we present a much simpler proof of that result which, in addition, is more general and totally uniform, so that it does not need to consider one by one the different semantics in the spectrum.     

Reasoning about keys for XML

We study absolute and relative keys for XML, and investigate their associated decision problems. We argue that these keys are important to many forms of hierarchically structured data including XML documents. In contrast to other proposals of keys for XML, we show that these keys are always (finitely) satisfiable, and their (finite) implication problem is finitely axiomatizable. Furthermore, we provide a polynomial time algorithm for determining (finite) implication in the size of keys. Our results also demonstrate, among other things, that the analysis of XML keys is far more intricate than its relational counterpart.     

Axiomatizing functional dependencies in the Higher-Order Entity-Relationship Model

A finite axiomatization of functional dependencies on conceptual database schemata is presented which naturally generalizes the well-known Armstrong axioms. The underlying conceptual data model is the Higher-Order Entity-Relationship Model.