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
Electronic Edition (link) BibTeX
Hans Kleine Büning, K. Subramani, Xishun Zhao:
Boolean Functions as Models for Quantified Boolean Formulas. 49-75
Electronic Edition (link) BibTeX
Barbara Morawska:
General E -unification with Eager Variable Elimination and a Nice Cycle Rule. 77-106
Electronic Edition (link) BibTeX

Special Issue on User Interfaces in Theorem Proving

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

Special Issue on Reasoning in Description Logics

Franz Baader:
Preface to Special Issue on Reasoning in Description Logics. 245-247
Electronic Edition (link) BibTeX
Ian Horrocks, Ulrike Sattler:
A Tableau Decision Procedure for SHOIQ. 249-276
Electronic Edition (link) BibTeX
Dmitry Tsarkov, Ian Horrocks, Peter F. Patel-Schneider:
Optimizing Terminological Reasoning for Expressive Description Logics. 277-316
Electronic Edition (link) BibTeX
Stefan Schlobach, Zhisheng Huang, Ronald Cornet, Frank van Harmelen:
Debugging Incoherent Terminologies. 317-349
Electronic Edition (link) BibTeX
Ullrich Hustadt, Boris Motik, Ulrike Sattler:
Reasoning in Description Logics by a Reduction to Disjunctive Datalog. 351-384
Electronic Edition (link) BibTeX
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
Electronic Edition (link) BibTeX

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