This book constitutes the refereed proceedings of the First International Joint Conference on Automated Reasoning, IJCAR 2001, held in Siena, Italy, in June 2001. The 37 research papers and 19 system descriptions presented together with three invited contributions were carefully reviewed and selected from a total of 112 submissions. The book offers topical sections on description, modal, and temporal logics; saturation based theorem proving, applications, and data structures; logic programming and nonmonotonic reasoning; propositional satisfiability and quantified Boolean logic; logical frameworks, higher-order logic, and interactive theorem proving; equational theorem proving and term rewriting; tableau, sequent, and natural deduction calculi and proof theory; automata, specification, verification, and logics of programs; and nonclassical logics.
Author(s): Neil D. Jones (auth.), Rajeev Goré, Alexander Leitsch, Tobias Nipkow (eds.)
Series: Lecture Notes in Computer Science 2083 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2001
Language: English
Pages: 708
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Software Engineering; Mathematical Logic and Foundations
Program Termination Analysis by Size-Change Graphs (Abstract)....Pages 1-4
SET Cardholder Registration: The Secrecy Proofs....Pages 5-12
Algorithms, Datastructures, and other Issues in Efficient Automated Deduction....Pages 13-28
The Description Logic ALCNH R + Extended with Concrete Domains: A Practically Motivated Approach....Pages 29-44
NExpTime-Complete Description Logics with Concrete Domains....Pages 45-60
Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics....Pages 61-75
The Hybrid μ-Calculus....Pages 76-91
The Inverse Method Implements the Automata Approach for Modal Satisfiability....Pages 92-106
Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL....Pages 107-120
Tableaux for Temporal Description Logic with Constant Domains....Pages 121-136
Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation....Pages 137-151
Instructing Equational Set-Reasoning with Otter....Pages 152-167
NP-Completeness of Refutability by Literal-Once Resolution....Pages 168-181
Ordered Resolution vs. Connection Graph resolution....Pages 182-194
A Model-Based Completeness Proof of Extended Narrowing and Resolution....Pages 195-210
A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality....Pages 211-225
Superposition and Chaining for Totally Ordered Divisible Abelian Groups....Pages 226-241
Context Trees....Pages 242-256
On the Evaluation of Indexing Techniques for Theorem Proving....Pages 257-271
Preferred Extensions of Argumentation Frameworks: Query, Answering, and Computation....Pages 272-288
Bunched Logic Programming....Pages 289-304
A Top-Down Procedure for Disjunctive Well-Founded Semantics....Pages 305-317
A Second-Order Theorem Prover Applied to Circumscription....Pages 318-324
NoMoRe: A System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics....Pages 325-330
Conditional Pure Literal Graphs....Pages 331-346
Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability....Pages 347-363
QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability....Pages 364-369
System Abstract: E 0.61....Pages 370-375
Vampire 1.1....Pages 376-380
DCTP - A Disconnection Calculus Theorem Prover - System Abstract....Pages 381-385
More On Implicit Syntax....Pages 386-400
Termination and Reduction Checking for Higher-Order Logic Programs....Pages 401-415
P.rex : An Interactive Proof Explainer....Pages 416-420
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants....Pages 421-426
The eXtended Least Number Heuristic....Pages 427-442
System Description: SCOTT-5....Pages 443-447
Combination of Distributed Search and Multi-Search in Peers-mcd.d....Pages 448-452
Lotrec: The Generic Tableau Prover for Modal and Description Logics....Pages 453-458
The modprof Theorem Prover....Pages 459-463
A New System and Methodology for Generating Random Modal Formulae....Pages 464-468
Decidable Classes of Inductive Theorems....Pages 469-484
Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems....Pages 485-498
Decidability and Complexity of Finitely Closable Linear Equational Theories....Pages 499-513
A New Meta-Complexity Theorem for Bottom-Up Logic Programs....Pages 514-528
Canonical Propositional Gentzen-Type Systems....Pages 529-544
Incremental Closure of Free Variable Tableaux....Pages 545-560
Deriving Modular Programs from Short Proofs....Pages 561-577
A General Method for Using Schematizations in Automated Deduction....Pages 578-592
Approximating Dependency Graphs Using Tree Automata Techniques....Pages 593-610
On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables....Pages 611-625
A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities....Pages 626-641
Flaw Detection in Formal Specifications....Pages 642-657
CCE: Testing Ground Joinability....Pages 658-662
System Description: RDL Rewrite and Decision Procedure Laboratory....Pages 663-669
lolliCoP — A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic....Pages 670-684
Muscadet 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction....Pages 685-689
Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory....Pages 690-695
STRIP: Structural Sharing for Efficient Proof-Search....Pages 696-700
RACER System Description....Pages 701-705
