Journal of Automated Reasoning (JAR), Volume 40

Volume 40, Number 1, January 2008

Mark H. Liffiton, Karem A. Sakallah:
Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. 1-33
Electronic Edition (link) BibTeX
Jia Meng, Lawrence C. Paulson:
Translating Higher-Order Clauses to First-Order Clauses. 35-60
Electronic Edition (link) BibTeX
Marc Bezem, Dimitri Hendriks:
On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic. 61-85
Electronic Edition (link) BibTeX

Selected Papers from the 3rd International Joint Conference on Automated Reasoning

Ulrich Furbach:
IJCAR Preface. 87-88
Electronic Edition (link) BibTeX
Yevgeny Kazakov, Boris Motik:
A Resolution-Based Decision Procedure for SHOIQ. 89-116
Electronic Edition (link) BibTeX
David Toman, Grant E. Weddell:
On Keys and Functional Dependencies as First-Class Citizens in Description Logics. 117-132
Electronic Edition (link) BibTeX
Kaustuv Chaudhuri, Frank Pfenning, Greg Price:
A Logical Characterization of Forward and Backward Chaining in the Inverse Method. 133-177
Electronic Edition (link) BibTeX
Andrey Paskevich:
Connection Tableaux with Lazy Paramodulation. 179-194
Electronic Edition (link) BibTeX
Jörg Endrullis, Johannes Waldmann, Hans Zantema:
Matrix Interpretations for Proving Termination of Term Rewriting. 195-220
Electronic Edition (link) BibTeX
Volker Sorge, Andreas Meier, Roy L. McCasland, Simon Colton:
Automatic Construction and Verification of Isotopy Invariants. 221-243
Electronic Edition (link) BibTeX

Sandip Ray, Warren A. Hunt Jr., John Matthews, J. Strother Moore:
A Mechanical Analysis of Program Verification Strategies. 245-269
Electronic Edition (link) BibTeX
Jesús Aransay, Clemens Ballarin, Julio Rubio:
A Mechanized Proof of the Basic Perturbation Lemma. 271-292
Electronic Edition (link) BibTeX
Bishop Brock, Matt Kaufmann, J. Strother Moore:
Rewriting with Equivalence Relations in ACL2. 293-306
Electronic Edition (link) BibTeX
Laurence Rideau, Bernard P. Serpette, Xavier Leroy:
Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves. 307-326
Electronic Edition (link) BibTeX
Christian Urban:
Nominal Techniques in Isabelle/HOL. 327-356
Electronic Edition (link) BibTeX
Yevgeny Kazakov, Boris Motik:
A Resolution-Based Decision Procedure for SHOIQ. 357
Electronic Edition (link) BibTeX