+612 9045 4394
Automated Reasoning : First International Joint Conference, Ijcar 2001 Siena, Italy, June 18-23, 2001 Proceedings - Rajeev Gore

Automated Reasoning

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

By: Rajeev Gore (Editor), Alexander Leitsch (Editor), Tobias Nipkow (Editor)


Published: 6th June 2001
Ships: 5 to 9 business days
5 to 9 business days
or 4 easy payments of $51.04 with Learn more
if ordered within

The last ten years have seen a gradual fragmentation of the Automated Reas- ing community into various disparate groups, each with its own conference: the Conference on Automated Reasoning (CADE), the International Workshop on First-Order Theorem Proving (FTP), and the International Conference on - tomated Reasoning with Analytic Tableau and Related Methods (TABLEAUX) to name three. During 1999, various members of these three communities d- cussed the idea of holding a joint conference in 2001 to bring our communities togetheragain.Theplanwastoholdaone-o?conferencefor2001, toberepeated ifitprovedasuccess.Thisvolumecontainsthepaperspresentedattheresulting event: the?rstInternationalJointConferenceonAutomatedReasoning(IJCAR 2001), held in Siena, Italy, from June 18-23, 2001. We received 88 research papers and 24 systems descriptions as submissions. Each submission was fully refereed by at least three peers who were asked to writeareportonthequalityofthesubmissions.Thesereportswereaccessibleto membersoftheprogrammecommitteeviaaweb-basedsystemspeciallydesigned for electronic discussions. As a result we accepted 37 research papers and 19 system descriptions, which make up these proceedings. In addition, this volume contains full papers or extended abstracts from the ?ve invited speakers. Tenone-dayworkshopsandfourtutorialswereheldduringIJCAR2001.The automatedtheoremprovingsystemcompetition(CASC)wasorganizedbyGeo? Sutcli?e to evaluate the performance of sound, fully automatic, classical, ?r- order automated theorem proving systems. The third Workshop on Inference in Computational Semantics (ICoS-3) and the 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS-2001) were co-located with IJCAR 2001, and held their own associated workshops and produced their own separate proceedings.

Invited Talks
Program Termination Analysis by Size-Change Graphsp. 1
SET Cardholder Registration: The Secrecy Proofsp. 5
Algorithms, Datastructures, and Other Issues in Efficient Automated Deductionp. 13
Description, Modal, and Temporal Logics
The Description Logic ALCNH(R)+ Extended with Concrete Domains: A Practically Motivated Approachp. 29
NExpTlME-Complete Description Logics with Concrete Domainsp. 45
Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logicsp. 61
The Hybrid -Calculusp. 76
The Inverse Method Implements the Automata Approach for Modal Satisfiabilityp. 92
Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTLp. 107
Tableaux for Temporal Description Logic with Constant Domainsp. 121
Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designationp. 137
Saturation Based Theorem Proving, Applications, and Data Structures
Instructing Equational Set-Reasoning with Otterp. 152
NP-Completeness of Refutability by Literal-Once Resolutionp. 168
Ordered Resolution vs. Connection Graph Resolutionp. 182
A Model-Based Completeness Proof of Extended Narrowing and Resolutionp. 195
A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equalityp. 211
Superposition and Chaining for Totally Ordered Divisible Abelian Groupsp. 226
Context Treesp. 242
On the Evaluation of Indexing Techniques for Theorem Provingp. 257
Logic Programming and Nonmonotonic Reasoning
Preferred Extensions of Argumentation Frameworks: Query, Answering, and Computationp. 272
Bunched Logic Programmingp. 289
A Top-Down Procedure for Disjunctive Well-Founded Semanticsp. 305
A Second-Order Theorem Prover Applied to Circumscriptionp. 318
NoMoRe: A System for Non-monotonic Reasoning with Logic Programs under Answer Set Semanticsp. 325
Propositional Satisfiability and Quantified Boolean Logic
Conditional Pure Literal Graphsp. 331
Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiabilityp. 347
Qube: A System for Deciding Quantified Boolean Formulas Satisfiabilityp. 364
System Abstract: E 0.61p. 370
Vampire 1.1 (System Description)p. 376
DCTP - A Disconnection Calculus Theorem Prover - System Abstractp. 381
Logical Frameworks, Higher-Order Logic, Interactive Theorem Proving
More on Implicit Syntaxp. 386
Termination and Reduction Checking for Higher-Order Logic Programsp. 401
P.rex: An Interactive Proof Explainerp. 416
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistantsp. 421
Semantic Guidance
The eXtended Least Number Heuristicp. 427
System Description: SCOTT-5p. 443
Combination of Distributed Search and Multi-search in Peers-mcd.d (System Description)p. 448
Lotrec: The Generic Tableau Prover for Modal and Description Logicsp. 453
The Modprof Theorem Proverp. 459
A New System and Methodology for Generating Random Modal Formulaep. 464
Equational Theorem Proving and Term Rewriting
Decidable Classes of Inductive Theoremsp. 469
Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systemsp. 485
Decidability and Complexity of Finitely Closable Linear Equational Theoriesp. 499
A New Meta-complexity Theorem for Bottom-Up Logic Programsp. 514
Tableau, Sequent, Natural Deduction Calculi, and Proof Theory
Canonical Propositional Gentzen-Type Systemsp. 529
Incremental Closure of Free Variable Tableauxp. 545
Deriving Modular Programs from Short Proofsp. 561
A General Method for Using Schematizations in Automated Deductionp. 578
Automata, Specification, Verification, and Logics of Programs
Approximating Dependency Graphs Using Tree Automata Techniquesp. 593
On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variablesp. 611
A Sequent Calculus for First-Order Dynamic Logic with Trace Modalitiesp. 626
Flaw Detection in Formal Specificationsp. 642
CCE: Testing Ground Joinabilityp. 658
System Description: RDL Rewrite and Decision Procedure Laboratoryp. 663
Nonclassical Logics
Lollicop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logicp. 670
Musoadet 2.3: A Knowledge-Based Theorem Prover Based on Natural Deductionp. 685
Hilberticus-AToolDeciding an Elementary Sublanguage of Set Theoryp. 690
STRIP: Structural Sharing for Efficient Proof-Searchp. 696
RACER System Descriptionp. 701
Author Indexp. 707
Table of Contents provided by Publisher. All Rights Reserved.

ISBN: 9783540422549
ISBN-10: 3540422544
Series: Lecture Notes in Computer Science
Audience: General
Format: Paperback
Language: English
Number Of Pages: 712
Published: 6th June 2001
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 3.68
Weight (kg): 1.0