Journal of Automated Reasoning (JAR), Volume 39

Volume 39, Number 1, July 2007

• Alberto Ciaffaglione, Luigi Liquori, Marino Miculan:
  Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts. 1-47
  
• Hans Kleine Büning, K. Subramani, Xishun Zhao:
  Boolean Functions as Models for Quantified Boolean Formulas. 49-75
  
• Barbara Morawska:
  General E -unification with Eager Variable Elimination and a Nice Cycle Rule. 77-106
  

Volume 39, Number 2, August 2007

• David Aspinall, Christoph Lüth:
  Special Issue on User Interfaces in Theorem Proving: Preface. 107-108
  
• Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli:
  User Interaction with the Matita Proof Assistant. 109-139
  
• Paul A. Cairns, Jeremy Gow:
  Integrating Searching and Authoring in Mizar. 141-160
  
• Julien Narboux:
  A Graphical User Interface for Formal Proofs in Geometry. 161-180
  
• William Billingsley, Peter Robinson:
  Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book. 181-218
  
• Carsten Sinz:
  Visualizing SAT Instances and Runs of the DPLL Algorithm. 219-243
  

Volume 39, Number 3, October 2007

• Franz Baader:
  Preface to Special Issue on Reasoning in Description Logics. 245-247
  
• Ian Horrocks, Ulrike Sattler:
  A Tableau Decision Procedure for SHOIQ. 249-276
  
• Dmitry Tsarkov, Ian Horrocks, Peter F. Patel-Schneider:
  Optimizing Terminological Reasoning for Expressive Description Logics. 277-316
  
• Stefan Schlobach, Zhisheng Huang, Ronald Cornet, Frank van Harmelen:
  Debugging Incoherent Terminologies. 317-349
  
• Ullrich Hustadt, Boris Motik, Ulrike Sattler:
  Reasoning in Description Logics by a Reduction to Disjunctive Datalog. 351-384
  
• Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, Riccardo Rosati:
  Tractable Reasoning and Efficient Query Answering in Description Logics: The DL-Lite Family. 385-429
  

Volume 39, Number 4, December 2007

• Gem Stapleton, Judith Masthoff, Jean Flower, Andrew Fish, Jane Southern:
  Automated Theorem Proving in Euler Diagram Systems. 431-470
  
• Daniel R. Brooks, Esra Erdem, Selim T. Erdogan, James W. Minett, Donald Ringe:
  Inferring Phylogenetic Trees Using Answer Set Programming. 471-511
  
• Julien Forest, Delia Kesner:
  Expression Reduction Systems with Patterns. 513-541