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
  
• Jia Meng, Lawrence C. Paulson:
  Translating Higher-Order Clauses to First-Order Clauses. 35-60
  
• Marc Bezem, Dimitri Hendriks:
  On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic. 61-85
  

Volume 40, Numbers 2-3, March 2008

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

Volume 40, Number 4, May 2008

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