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 BibTeX

Invited Talks

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

Proofs

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

Search

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

System Description 1

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

Higher-Order Logic

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

Proof Theory

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

System Description 2

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

Search

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

Proof Theory

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

Proof Checking

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

Combination

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

Decision Procedures

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
Electronic Edition (link) BibTeX
Amine Chaieb:
Verifying Mixed Real-Integer Quantifier Elimination. 528-540
Electronic Edition (link) BibTeX
Stéphane Demri, Denis Lugiez:
Presburger Modal Logic Is PSPACE-Complete. 541-556
Electronic Edition (link) BibTeX
Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron:
Tree Automata with Equality Constraints Modulo Equational Theories. 557-571
Electronic Edition (link) BibTeX

CASC-J3

Geoff Sutcliffe:
CASC-J3 - The 3rd IJCAR ATP System Competition. 572-573
Electronic Edition (link) BibTeX

Rewriting

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

Description Logic

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