Catálogo de publicaciones - libros

In peer-to-peer (P2P) systems, each peer exports information in terms of its own schema, and interoperation is achieved by means of mappings among the peer schemas. Peers are autonomous systems and mappings are dynamically created and changed. One of the challenges in these systems is processing queries posed to one peer taking into account the mappings. Obviously, query processing strongly depends on the semantics of the overall system.

In this talk, we overview the various approaches that have been proposed for modeling P2P systems, considering several central properties of such systems, such as modularity, generality, and computational issues related to query processing. We argue that an approach based on epistemic logic is superior with respect to all the above properties to previously proposed approaches based on first-order logic. Specifically, the epistemic logic approach naturally captures the modular nature of P2P systems, and moreover query answering can be performed efficiently (i.e., polynomially) in the size of the data stored in the various peers. This holds independently of the topology of the mappings among peers, and hence respecting one of the fundamental assumptions in P2P systems: namely, that peers are autonomouns entities that can establish mappings to other peers without requiring the intervention of any centralized authority.

Description Logics (DLs) are a family of logic based knowledge representation formalisms. Although they have a range of applications (e.g., configuration and information integration), they are perhaps best known as the basis for widely used ontology languages such as OWL (now a W3C recommendation). This decision was motivated by a requirement that key inference problems be decidable, and that it should be possible to provide reasoning services to support ontology design and deployment. Such reasoning services are typically provided by highly optimised implementations of tableaux decision procedures; these have proved to be effective in applications in spite of the high worst case complexity of key inference problems. The increasing use of DL based ontologies in areas such as e-Science and the Semantic Web is, however, already stretching the capabilities of existing DL systems, and brings with it a range of research challenges.

“The Semantic Web is specifically a web of machine-readable information whose meaning is well-defined by standards” (Tim Berners-Lee in the foreword of the book “Spinning the Web”). This is a very simplified definition of the Semantic Web. The crucial part is the last word “standards”. Since machine readable information in the web can be almost anything, the standards must also be about almost anything. Taken to the extreme, it requires a standardised model of the whole world, physical as well as conceptual, against which the information is interpreted. The world model must contain concrete data, for example the location of my office in Munich, as well as abstract relationships, for example, that an office is a room.

This talk will consider rigorous mathematics and the nature of proof. It begins with an historical perspective and follows the development of formal mathematics. The talk will conclude with examples demonstrating that understanding the relationship between formal mathematics and rigorous proof can assist with both the discovery and the quality of real proofs of real results.

We prove consistency of a sequent calculus for classical logic with explicit splitting of free variables by means of a semantical soundness argument. The free variable system is a mature formulation of the system proposed at TABLEAUX 2003 [1]. We also identify some challenging and interesting open research problems.

A major source of the undecidability of a logic is the number of instances—the so-called multiplicities—of existentially quantified formulas that are required in a proof. We consider the problem in the context of matrix proof methods for classical higher-order logic and present a technique which improves the standard practice of iterative deepening over the multiplicities. We present a mechanism that allows to adjust multiplicities on demand during matrix-based proof search and not only preserves existing substitutions and connections, but additionally adapts them to the parts that result from the increase of the multiplicities.

Propositional interval temporal logics are quite expressive temporal logics that allow one to naturally express statements that refer to time intervals. Unfortunately, most such logics turned out to be (highly) undecidable. To get decidability, severe syntactic and/or semantic restrictions have been imposed to interval-based temporal logics that make it possible to reduce them to point-based ones. The problem of identifying expressive enough, yet decidable, new interval logics or fragments of existing ones which are interval-based is still largely unexplored. In this paper, we make one step in this direction by devising an original tableau-based decision procedure for the future fragment of Propositional Neighborhood Interval Temporal Logic, interpreted over natural numbers.

We consider a cyclic approach to inductive reasoning in the setting of first-order logic with inductive definitions. We present a proof system for this language in which proofs are represented as finite, locally sound derivation trees with a “repeat function” identifying cyclic proof sections. Soundness is guaranteed by a well-foundedness condition formulated globally in terms of over the proof tree, following an idea due to Sprenger and Dam. However, in contrast to their work, our proof system does not require an extension of logical syntax by ordinal variables.

A fundamental question in our setting is the strength of the cyclic proof system compared to the more familiar use of a non-cyclic proof system using explicit induction rules. We show that the cyclic proof system subsumes the use of explicit induction rules. In addition, we provide machinery for manipulating and analysing the structure of cyclic proofs, based primarily on viewing them as generating regular infinite trees, and also formulate a finitary trace condition sufficient (but not necessary) for soundness, that is computationally and combinatorially simpler than the general trace condition.

We study the decision problem for the language (), a quantifier-free fragment of graph theory involving the notions of reachability and acyclicity.

We prove that the language is decidable, and that its decidability problem is -complete. We do so by showing that the language enjoys a : If a formula is satisfiable, then it has a model whose cardinality is polynomial in the size of the formula.

Moreover, we show how the small model property can be used in order to devise a tableau-based decision procedure for .

In this paper we present a method for embedding static analysis into tableaux and sequent based frameworks. In these frameworks, the information flows from the root node to the leaf nodes. We show that the existence of free variables in such frameworks introduces a bi-directional flow, which can be used to collect and synthesize arbitrary information.

We use free variables to embed a static program analysis in a sequent style theorem prover used for verification of Java programs. The analysis we embed is a reaching definitions analysis, which is a common and well-known analysis that shows the potential of our method.

The achieved results are promising and open up for new areas of application of tableaux and sequent based theorem provers.