Automated Reasoning: Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

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.

Author(s): Bruno Buchberger (auth.), Ulrich Furbach, Natarajan Shankar (eds.)
Series: Lecture Notes in Computer Science 4130 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2006

Language: English
Pages: 688
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Software Engineering

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 -