nach oben

2005 | Buch

Kapitel lesen Erstes Kapitel lesen

Automated Reasoning with Analytic Tableaux and Related Methods

14th International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005. Proceedings

herausgegeben von: Bernhard Beckert

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Inhaltsverzeichnis

Frontmatter

Invited Talks

Query Processing in Peer-to-Peer Systems: An Epistemic Logic Approach

Abstract

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.

Diego Calvanese

Description Logics in Ontology Applications

Abstract

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.

Ian Horrocks

Automated Reasoning in the Context of the Semantic Web

Abstract

“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.

Hans Jürgen Ohlbach

Formal Versus Rigorous Mathematics: How to Get Your Papers Published

Abstract

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.

Erik Rosenthal

Research Papers

Consistency of Variable Splitting in Free Variable Systems of First-Order Logic

Abstract

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.

Roger Antonsen, Arild Waaler

On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic

Abstract

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.

Serge Autexier

A Tableau-Based Decision Procedure for Right Propositional Neighborhood Logic

Abstract

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 genuinely 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.

Davide Bresolin, Angelo Montanari

Cyclic Proofs for First-Order Logic with Inductive Definitions

Abstract

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 traces 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.

James Brotherston

A Tableau-Based Decision Procedure for a Fragment of Graph Theory Involving Reachability and Acyclicity

Abstract

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

We prove that the language DGRA is decidable, and that its decidability problem is NP-complete. We do so by showing that the language enjoys a small model property: 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 DGRA.

Domenico Cantone, Calogero G. Zarba

Embedding Static Analysis into Tableaux and Sequent Based Frameworks

Abstract

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.

Tobias Gedell

A Calculus for Type Predicates and Type Coercion

Abstract

We extend classical first-order logic with subtyping by type predicates and type coercion. Type predicates assert that the value of a term belongs to a more special type than the signature guarantees, while type coercion allows using terms of a more general type where the signature calls for a more special one. These operations are important e.g. in the specification and verification of object-oriented programs. We present a tableau calculus for this logic and prove its completeness.

Martin Giese

A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics

Abstract

We present a sound and complete tableau calculus for the class of regular grammar logics. Our tableau rules use a special feature called automaton-labelled formulae, which are similar to formulae of automaton propositional dynamic logic. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. We show that the known EXPTIME upper bound for regular grammar logics can be obtained using our tableau calculus. We also give an effective Craig interpolation lemma for regular grammar logics using our calculus.

Rajeev Goré, Linh Anh Nguyen

Comparing Instance Generation Methods for Automated Reasoning

Abstract

The clause linking technique of Lee and Plaisted proves the unsatisfiability of a set of first-order clauses by generating a sufficiently large set of instances of these clauses that can be shown to be propositionally unsatisfiable. In recent years, this approach has been refined in several directions, leading to both tableau-based methods, such as the Disconnection Tableau Calculus, and saturation-based methods, such as Primal Partial Instantiation and Resolution-based Instance Generation. We investigate the relationship between these calculi and answer the question to what extent refutation or consistency proofs in one calculus can be simulated in another one.

Swen Jacobs, Uwe Waldmann

An Order-Sorted Quantified Modal Logic for Meta-ontology

Abstract

The notions of meta-ontology enhance the ability to process knowledge in information systems; in particular, ontological property classification deals with the kinds of properties in taxonomic knowledge based on a philosophical analysis. The goal of this paper is to devise a reasoning mechanism to check the ontological and logical consistency of knowledge bases, which is important for reasoning services on taxonomic knowledge. We first consider an ontological property classification that is extended to capture individual existence and time and situation dependencies. To incorporate the notion into logical reasoning, we formalize an order-sorted modal logic that involves rigidity, sortality, and three kinds of modal operators (temporal/situational/any world). The sorted expressions and modalities establish axioms with respect to properties, implying the truth of properties in different kinds of possible worlds and in varying domains in Kripke semantics. We provide a prefixed tableau calculus to test the satisfiability of such sorted modal formulas, which validates the ontological axioms of properties.

Ken Kaneiwa, Riichiro Mizoguchi

A Redundancy Analysis of Sequent Proofs

Abstract

Proof search often involves a choice between alternatives which may result in redundant information once the search is complete. This behavior can manifest itself in proof search for sequent systems by the presence of redundant formulae or subformulae in a sequent for which a proof has been found. In this paper we investigate the detection and elimination of redundant parts of a provable sequent by using labels and Boolean constraints to keep track of usage information. We illustrate our ideas in propositional linear logic, but we believe the general approach is applicable to a variety of sequent systems, including other resource-sensitive logics.

Tatjana Lutovac, James Harland

A Tableau Algorithm for Description Logics with Concrete Domains and GCIs

Abstract

In description logics (DLs), concrete domains are used for defining concepts based on concrete qualities of their instances such as the weight, age, duration, and spatial extension. So-called general concept inclusions (GCIs) play an important role for capturing background knowledge. It is well-known that, when combining concrete domains with GCIs, reasoning easily becomes undecidable. In this paper, we identify a general property of concrete domains that is sufficient for proving decidability of DLs with both concrete domains and GCIs. We exhibit some useful concrete domains, most notably a spatial one based on the RCC-8 relations, which have this property. Then, we present a tableau algorithm for reasoning in DLs equipped with concrete domains and GCIs.

Carsten Lutz, Maja Miličić

The Space Efficiency of OSHL

Abstract

Ordered semantic hyper-linking (OSHL) is a first-order theorem prover that tries to take advantage of the speed of propositional theorem proving techniques. It instantiates first-order clauses to ground clauses, and applies propositional techniques to these ground clauses. OSHL-U extends OSHL with rules for unit clauses to speed up the instantiation strategy. OSHL-U obtains many of the same proofs as Otter does. This shows that many first-order theorems can be obtained without true unification, so techniques used to speed up propositional provers may be applicable to them. OSHL-U, in finding proofs, also generates and stores significantly fewer clauses than resolution prover Otter on many TPTP problems. On some TPTP groups, OSHL-U finds more proofs than Otter, despite a slower inference rate.

Swaha Miller, David A. Plaisted

Efficient Query Processing with Compiled Knowledge Bases

Abstract

The goal of knowledge compilation is to enable fast queries. Prior approaches had the goal of small (i.e., polynomial in the size of the initial knowledge bases) compiled knowledge bases. Typically, query-response time is linear, so that the efficiency of querying the compiled knowledge base depends on its size. In this paper, a target for knowledge compilation called the ri-trie is introduced; it has the property that even if they are large they nevertheless admit fast queries. Specifically, a query can be processed in time linear in the size of the query regardless of the size of the compiled knowledge base.

Neil V. Murray, Erik Rosenthal

Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic

Abstract

We present a clausal connection calculus for first-order intuitionistic logic. It extends the classical connection calculus by adding prefixes that encode the characteristics of intuitionistic logic. Our calculus is based on a clausal matrix characterisation for intuitionistic logic, which we prove correct and complete. The calculus was implemented by extending the classical prover leanCoP. We present some details of the implementation, called ileanCoP, and experimental results.

Jens Otten

Automatic ‘Descente Infinie’ Induction Reasoning

Abstract

We present a framework and a methodology to build and analyse automatic provers using the ’Descente Infinie’ induction principle. A stronger connection between different proof techniques like those based on implicit induction and saturation is established by uniformly and explicitly representing them as applications of this principle. The framework offers a clear separation between logic and computation, by the means of i) an abstract inference system that defines the maximal sets of induction hypotheses available at every step of a proof, and ii) reasoning modules that perform the computation and allow for modular design of the concrete inference rules. The methodology is applied to define a concrete implicit induction prover and analyse an existing saturation-based inference system.

Sorin Stratulat

A Decision Procedure for the Alternation-Free Two-Way Modal μ-Calculus

Abstract

The satisfiability checking problem is known to be decidable for a variety of modal/temporal logics such as the modal μ-calculus, but effective implementation has not necessarily been developed for all such logics. In this paper, we propose a decision procedure using the tableau method for the alternation-free two-way modal μ-calculus. Although the size of the tableau set maintained in the method might be large for complex formulas, the set and the operations on it can be expressed using BDD and therefore we can implement the method in an effective way.

Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, Masami Hagiya

On the Partial Respects in Which a Real Valued Arithmetic System Can Verify Its Tableaux Consistency

Abstract

Gödel’s Second Incompleteness Theorem states axiom systems of sufficient strength are unable to verify their own consistency. We will show this theorem does not preclude axiomizations for a computer’s floating point arithmetic from recognizing their own consistency, in certain well defined partial respects.

Dan E. Willard

System Descriptions

Pdk: The System and Its Language

Abstract

This paper presents the planning system Pdk (Planning with Domain Knowledge), based on the translation of planning problems into Linear Time Logic theories, in such a way that finding solution plans is reduced to model search. The model search mechanism is based on temporal tableaux. The planning language accepted by the system allows one to specify extra problem dependent information, that can be of help both in reducing the search space and finding plans of better quality.

Marta Cialdea Mayer, Carla Limongelli, Andrea Orlandini, Valentina Poggioni

Proof Output and Transformation for Disconnection Tableaux

Abstract

For applications of first-order automated theorem provers in a wider verification context it is essential to provide a means of presenting and checking automatically found proofs. In this paper we present a new method of transforming disconnection tableau proofs found by the prover system DCTP into a series of resolution inferences representing a resolution refutation of the proof problem.

Philipp Correll, Gernot Stenz

LoTREC: Logical Tableaux Research Engineering Companion

Abstract

In this paper we describe a generic tableaux system for building models or counter-models and testing satisfiability of formulas in modal and description logics. This system is called LoTREC2.0. It is characterized by a high-level language for tableau rules and strategies. It aims at covering all Kripke-semantic based logics. It is implemented in Java and characterized by a user-friendly graphical interface. It can be used as a learning system for possible worlds semantics and tableaux based proof methods.

Olivier Gasquet, Andreas Herzig, Dominique Longin, Mohamad Sahade

A Tableau-Based Explainer for DL Subsumption

Abstract

This paper describes the implementation of a tableau-based reasoning component which is capable of providing quasi natural language explanations for subsumptions within \(\mathcal{ALEHF_R+}\) TBoxes.

Thorsten Liebig, Michael Halfmann

CondLean 3.0: Improving CondLean for Stronger Conditional Logics

Abstract

In this paper we present CondLean 3.0, a theorem prover for propositional conditional logics CK, CK+ID, CK+MP, CK+CS, CK+CEM and some of their combinations. CondLean 3.0 implements sequent calculi for these logics. CondLean 3.0 improves CondLean and is developed following the methodology of leanTAP. It is implemented in SICStus Prolog and also comprises a graphical user interface implemented in JAVA. CondLean 3.0 can be downloaded at www.di.unito.it/~pozzato/condlean3/

Nicola Olivetti, Gian Luca Pozzato

The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic

Abstract

The Intuitionistic Logic Theorem Proving (ILTP) Library provides a platfom for testing and benchmarking theorem provers for first-order intuitionistic logic. It includes a collection of benchmark problems in a standardised syntax and performance results obtained by a comprehensive test of currently available intuitionistic theorem proving systems. These results are used to provide information about the status and the difficulty rating of the benchmark problems.

Thomas Raths, Jens Otten, Christoph Kreitz

Unit Propagation in a Tableau Framework

Abstract

Unit propagation is one of the most important techniques of efficient SAT solvers. Unfortunately, this technique is not directly applicable to first-order clausal tableaux. We show a way of integrating a variant of unit propagation into the disconnection calculus and present some results obtained with an implementation of unit propagation in the DCTP theorem prover that show the usefulness of our new method.

Gernot Stenz

Backmatter

Titel: Automated Reasoning with Analytic Tableaux and Related Methods
herausgegeben von: Bernhard Beckert
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-540-31822-4
Print ISBN: 978-3-540-28931-9
DOI: https://doi.org/10.1007/11554554

Springer Professional

Inhaltsverzeichnis

Frontmatter

Invited Talks

Query Processing in Peer-to-Peer Systems: An Epistemic Logic Approach

Description Logics in Ontology Applications

Automated Reasoning in the Context of the Semantic Web

Formal Versus Rigorous Mathematics: How to Get Your Papers Published

Research Papers

Consistency of Variable Splitting in Free Variable Systems of First-Order Logic

On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic

A Tableau-Based Decision Procedure for Right Propositional Neighborhood Logic

Cyclic Proofs for First-Order Logic with Inductive Definitions

A Tableau-Based Decision Procedure for a Fragment of Graph Theory Involving Reachability and Acyclicity

Embedding Static Analysis into Tableaux and Sequent Based Frameworks

A Calculus for Type Predicates and Type Coercion

A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics

Comparing Instance Generation Methods for Automated Reasoning

An Order-Sorted Quantified Modal Logic for Meta-ontology

A Redundancy Analysis of Sequent Proofs

A Tableau Algorithm for Description Logics with Concrete Domains and GCIs

The Space Efficiency of OSHL

Efficient Query Processing with Compiled Knowledge Bases

Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic

Automatic ‘Descente Infinie’ Induction Reasoning

A Decision Procedure for the Alternation-Free Two-Way Modal μ-Calculus

On the Partial Respects in Which a Real Valued Arithmetic System Can Verify Its Tableaux Consistency

System Descriptions

Pdk: The System and Its Language

Proof Output and Transformation for Disconnection Tableaux

LoTREC: Logical Tableaux Research Engineering Companion

A Tableau-Based Explainer for DL Subsumption

CondLean 3.0: Improving CondLean for Stronger Conditional Logics

The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic

Unit Propagation in a Tableau Framework

Backmatter

Premium Partner