3. IJCAR (CADE, FroCoS, FTP, TABLEAUX, TPHOLs) 2006: Seattle, WA, USA

Ulrich Furbach, Natarajan Shankar (Eds.): Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings. Lecture Notes in Computer Science 4130 Springer 2006, ISBN 3-540-37187-7

Invited Talks

Bruno Buchberger:
Mathematical Theory Exploration. 1-2
Adnan Darwiche:
Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation. 3
Dale Miller:
Representing and Reasoning with Operational Semantics. 4-20

Tobias Nipkow, Gertrud Bauer, Paula Schultz:
Flyspeck I: Tame Graphs. 21-35
Volker Sorge, Andreas Meier, Roy L. McCasland, Simon Colton:
Automatic Construction and Verification of Isotopy Invariants. 36-51
Sylvie Boldo:
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. 52-66
Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Allen Van Gelder:
Using the TPTP Language for Writing Derivations and Finite Interpretations. 67-81

Jordi Levy, Manfred Schmidt-Schauß, Mateu Villaret:
Stratified Context Unification Is NP-Complete. 82-96
Kaustuv Chaudhuri, Frank Pfenning, Greg Price:
A Logical Characterization of Forward and Backward Chaining in the Inverse Method. 97-111
Andrey Paskevich:
Connection Tableaux with Lazy Paramodulation. 112-124
Peter Baumgartner, Renate A. Schmidt:
Blocking and Other Enhancements for Bottom-Up Model Generation Methods. 125-139

Jürgen Zimmer, Serge Autexier:
The MathServe System for Semantic Web Reasoning Services. 140-144
Predrag Janicic, Pedro Quaresma:
System Description: GCLCprover + GeoThms. 145-150
Joe Hendrix, José Meseguer, Hitoshi Ohsaki:
A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms. 151-155
Allen Van Gelder, Geoff Sutcliffe:
Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. 156-161

Robert L. Constable, Wojciech Moczydlowski:
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics. 162-176
John Harrison:
Towards Self-verification of HOL Light. 177-191
Sean McLaughlin:
An Interpretation of Isabelle/HOL in HOL Light. 192-204
Chad E. Brown:
Combining Type Theory and Untyped Set Theory. 205-219

Christoph Benzmüller, Chad E. Brown, Michael Kohlhase:
Cut-Simulation in Impredicative Logics. 220-234
Viorica Sofronie-Stokkermans:
Interpolation in Local Theory Extensions. 235-250
Anna Zamansky, Arnon Avron:
Canonical Gentzen-Type Calculi with (n, k)-ary Quantifiers. 251-265
Bernhard Beckert, André Platzer:
Dynamic Logic with Non-rigid Functions. 266-280

Jürgen Giesl, Peter Schneider-Kamp, René Thiemann:
Automatic Termination Proofs in the Dependency Pair Framework. 281-286
Franz Baader, Carsten Lutz, Boontawee Suntisrivaraporn:
CEL - A Polynomial-Time Reasoner for Life Science Ontologies. 287-291
Dmitry Tsarkov, Ian Horrocks:
Description Logic Reasoner: System Description. 292-297
Steven Obua, Sebastian Skalberg:
Importing HOL into Isabelle/HOL. 298-302

Hans de Nivelle, Jia Meng:
Geometric Resolution: A Proof Procedure Based on Finite Model Search. 303-317
Xiangxue Jia, Jian Zhang:
A Powerful Technique to Eliminate Isomorphism in Finite Model Search. 318-331
Adam Koprowski, Hans Zantema:
Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems. 332-346

Roy Dyckhoff, Delia Kesner, Stéphane Lengrand:
Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic. 347-361
Brigitte Pientka:
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. 362-376
Florian Rabe:
First-Order Logic with Dependent Types. 377-391

Dexter Kozen, Christoph Kreitz, Eva Richter:
Automating Proofs in Category Theory. 392-407
Roland Zumkeller:
Formal Global Optimisation with Taylor Models. 408-422
Benjamin Grégoire, Laurent Théry:
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. 423-437
Assia Mahboubi:
Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. 438-452

Erik Reeber, Warren A. Hunt Jr.:
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). 453-467
Shuvendu K. Lahiri, Madanlal Musuvathi:
Solving Sparse Linear Constraints. 468-482
Olga Grinchtein, Martin Leucker, Nir Piterman:
Inferring Network Invariants Automatically. 483-497
Christian Urban, Stefan Berghofer:
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. 498-512

Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli:
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures. 513-527
Amine Chaieb:
Verifying Mixed Real-Integer Quantifier Elimination. 528-540
Stéphane Demri, Denis Lugiez:
Presburger Modal Logic Is PSPACE-Complete. 541-556
Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron:
Tree Automata with Equality Constraints Modulo Equational Theories. 557-571

Jörg Endrullis, Johannes Waldmann, Hans Zantema:
Matrix Interpretations for Proving Termination of Term Rewriting. 574-588
Alexander Krauss:
Partial Recursive Functions in Higher-Order Logic. 589-603
Benjamin Werner:
On the Strength of Proof-Irrelevant Type Theories. 604-618
Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz:
Consistency and Completeness of Rewriting in the Calculus of Constructions. 619-631

Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi:
Specifying and Reasoning About Dynamic Access-Control Policies. 632-646
David Toman, Grant E. Weddell:
On Keys and Functional Dependencies as First-Class Citizens in Description Logics. 647-661
Yevgeny Kazakov, Boris Motik:
A Resolution-Based Decision Procedure for SHOIQ. 662-677