Automated Reasoning: Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (Lecture Notes in Computer Science, 4130)

This book constitutes the refereed proceedings of the Third International Joint Conference on Automated Reasoning, IJCAR 2006, held in Seattle, WA, USA in August 2006 as part of the 4th Federated Logic Conference, FLoC 2006. IJCAR 2006 is a merger of CADE, FroCoS, FTP, TABLEAUX, and TPHOLs. The 41 revised full research papers and 8 revised system descriptions presented together with 3 invited papers and a summary of a systems competition were carefully reviewed and selected from a total of 152 submissions. The papers address the entire spectrum of research in automated reasoning including formalization of mathematics, proof theory, proof search, description logics, interactive proof checking, higher-order logic, combination methods, satisfiability procedures, and rewriting. The papers are organized in topical sections on proofs, search, higher-order logic, proof theory, search, proof checking, combination, decision procedures, CASC-J3, rewriting, and description logic. Front Matter....Pages - Mathematical Theory Exploration....Pages 1-2 Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation....Pages 3-3 Representing and Reasoning with Operational Semantics....Pages 4-20 Flyspeck I: Tame Graphs....Pages 21-35 Automatic Construction and Verification of Isotopy Invariants....Pages 36-51 Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms....Pages 52-66 Using the TPTP Language for Writing Derivations and Finite Interpretations....Pages 67-81 Stratified Context Unification Is NP-Complete....Pages 82-96 A Logical Characterization of Forward and Backward Chaining in the Inverse Method....Pages 97-111 Connection Tableaux with Lazy Paramodulation....Pages 112-124 Blocking and Other Enhancements for Bottom-Up Model Generation Methods....Pages 125-139 The MathServe System for Semantic Web Reasoning Services....Pages 140-144 System Description: GCLCprover + GeoThms....Pages 145-150 A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms....Pages 151-155 Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation....Pages 156-161 Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics....Pages 162-176 Towards Self-verification of HOL Light....Pages 177-191 An Interpretation of Isabelle/HOL in HOL Light....Pages 192-204 Combining Type Theory and Untyped Set Theory....Pages 205-219 Cut-Simulation in Impredicative Logics....Pages 220-234 Interpolation in Local Theory Extensions....Pages 235-250 Canonical Gentzen-Type Calculi with (n,k)-ary Quantifiers....Pages 251-265 Dynamic Logic with Non-rigid Functions....Pages 266-280 AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework....Pages 281-286 CEL — A Polynomial-Time Reasoner for Life Science Ontologies....Pages 287-291 FaCT++ Description Logic Reasoner: System Description....Pages 292-297 Importing HOL into Isabelle/HOL....Pages 298-302 Geometric Resolution: A Proof Procedure Based on Finite Model Search....Pages 303-317 A Powerful Technique to Eliminate Isomorphism in Finite Model Search....Pages 318-331 Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems....Pages 332-346 Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic....Pages 347-361 Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach....Pages 362-376 First-Order Logic with Dependent Types....Pages 377-391 Automating Proofs in Category Theory....Pages 392-407 Formal Global Optimisation with Taylor Models....Pages 408-422 A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers....Pages 423-437 Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials....Pages 438-452 A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)....Pages 453-467 Solving Sparse Linear Constraints....Pages 468-482 Inferring Network Invariants Automatically....Pages 483-497 A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL....Pages 498-512 Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures....Pages 513-527 Verifying Mixed Real-Integer Quantifier Elimination....Pages 528-540 Presburger Modal Logic Is PSPACE-Complete....Pages 541-556 Tree Automata with Equality Constraints Modulo Equational Theories....Pages 557-571 CASC-J3 The 3rd IJCAR ATP System Competition....Pages 572-573 Matrix Interpretations for Proving Termination of Term Rewriting....Pages 574-588 Partial Recursive Functions in Higher-Order Logic....Pages 589-603 On the Strength of Proof-Irrelevant Type Theories....Pages 604-618 Consistency and Completeness of Rewriting in the Calculus of Constructions....Pages 619-631 Specifying and Reasoning About Dynamic Access-Control Policies....Pages 632-646 On Keys and Functional Dependencies as First-Class Citizens in Description Logics....Pages 647-661 A Resolution-Based Decision Procedure for $\mathcal{SHOIQ}$ ....Pages 662-677 Back Matter....Pages - Annotation Here are the proceedings of the Third International Joint Conference on Automated Reasoning, IJCAR 2006, held in Seattle, Washington, USA, August 2006. The book presents 41 revised full research papers and 8 revised system descriptions, with 3 invited papers and a summary of a systems competition. The papers are organized in topical sections on proofs, search, higher-order logic, proof theory, proof checking, combination, decision procedures, CASC-J3, rewriting, and description logic Ulrich Furbach, Natarajan Shankar (eds.). Includes Bibliographical References And Index. Also Issued Online.