Skip to main content
SpringerLink
Log in
Book cover

Automated Reasoning

First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-23, 2001 Proceedings

  • Conference proceedings
  • © 2001

Overview

Editors:
  1. Rajeev Goré

    1. Automated Reasoning Project and Department of Computer Science, Australian National University, Canberra, Australia

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Alexander Leitsch

    1. AG Theoretische Informatik und Logik, Institut für Computersprachen, Technische Universität Wien, Wien, Austria

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Tobias Nipkow

    1. Institut für Informatik, Technische Universität München, München, Germany

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 2083)

Part of the book sub series: Lecture Notes in Artificial Intelligence (LNAI)

Included in the following conference series:

Conference proceedings info: IJCAR 2001.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (59 papers)

  1. Front Matter

    Pages I-XIII
    Download chapter PDF

  3. SET Cardholder Registration: The Secrecy Proofs

    1. SET Cardholder Registration: The Secrecy Proofs

      • Lawrence C. Paulson
      Pages 5-12

  4. Algorithms, Datastructures, and other Issues in Efficient Automated Deduction

    1. Algorithms, Datastructures, and other Issues in Efficient Automated Deduction

      • Andrei Voronkov
      Pages 13-28

  5. Description, Modal and temporal Logics

    1. The Description Logic ALCNH R + Extended with Concrete Domains: A Practically Motivated Approach

      • Volker Haarslev, Ralf Möller, Michael Wessel
      Pages 29-44

    2. NExpTime-Complete Description Logics with Concrete Domains

      • Carsten Lutz
      Pages 45-60

  6. Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics

    1. Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics

      • Volker Haarslev, Ralf Möller, Anni-Yasmin Turhan
      Pages 61-75

  7. The Hybrid μ-Calculus

    1. The Hybrid μ-Calculus

      • Ulrike Sattler, Moshe Y. Vardi
      Pages 76-91

  8. The Inverse Method Implements the Automata Approach for Modal Satisfiability

    1. The Inverse Method Implements the Automata Approach for Modal Satisfiability

      • Franz Baader, Stephan Tobies
      Pages 92-106

  9. Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL

    1. Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL

      • Regimantas Pliuškevičius
      Pages 107-120

  10. Tableaux for Temporal Description Logic with Constant Domains

    1. Tableaux for Temporal Description Logic with Constant Domains

      • Carsten Lutz, Holger Sturm, Frank Wolter, Michael Zakharyaschev
      Pages 121-136

  11. Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation

    1. Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation

      • Serenella Cerrito, Marta Cialdea Mayer
      Pages 137-151

  12. Saturation Based Theorem Proving, Applications, and Data Structures

    1. Instructing Equational Set-Reasoning with Otter

      • Andrea Formisano, Eugenio G. Omodeo, Marco Temperini
      Pages 152-167

    2. NP-Completeness of Refutability by Literal-Once Resolution

      • Stefan Szeider
      Pages 168-181

    3. Ordered Resolution vs. Connection Graph resolution

      • Reiner Hähnle, Neil V. Murray, Erik Rosenthal
      Pages 182-194

  13. A Model-Based Completeness Proof of Extended Narrowing and Resolution

    1. A Model-Based Completeness Proof of Extended Narrowing and Resolution

      • Jürgen Stuber
      Pages 195-210

  14. A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality

    1. A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality

      • Hans de Nivelle, Ian Pratt-Hartmann
      Pages 211-225

  15. Superposition and Chaining for Totally Ordered Divisible Abelian Groups

    1. Superposition and Chaining for Totally Ordered Divisible Abelian Groups

      • Uwe Waldmann
      Pages 226-241

  16. Context Trees

    1. Context Trees

      • Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
      Pages 242-256

  17. On the Evaluation of Indexing Techniques for Theorem Proving

    1. On the Evaluation of Indexing Techniques for Theorem Proving

      • Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov
      Pages 257-271
Back to top

Other volumes

  1. Automated Reasoning

Keywords

Editors and Affiliations

  • Automated Reasoning Project and Department of Computer Science, Australian National University, Canberra, Australia

    Rajeev Goré

  • AG Theoretische Informatik und Logik, Institut für Computersprachen, Technische Universität Wien, Wien, Austria

    Alexander Leitsch

  • Institut für Informatik, Technische Universität München, München, Germany

    Tobias Nipkow

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation