Journal of Automated Reasoning (JAR), Volume 29

Volume 29, Number 1, 2002

William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, Larry Wos: Short Single Axioms for Boolean Algebra. 1-16 BibTeX
Adnan H. Yahya, David A. Plaisted: Ordered Semantic Hyper Tableaux. 17-57 BibTeX
John K. Slaney: More Proofs of an Axiom of Lukasiewicz. 59-66 BibTeX
Ruediger Thiele, Larry Wos: Hilbert's Twenty-Fourth Problem. 67-89 BibTeX
Vivek S. Borkar, Vijay Chandru, Sanjoy K. Mitter: Mathematical Programming Embeddings of Logic. 91-106 BibTeX

Larry Wos, Dolph Ulrich, Branden Fitelson: Vanquishing the XCB Question: The Methodological Discovery of the Last Shortest Single Axiom for the Equivalential Calculus. 107-124 BibTeX
Leila Amgoud, Claudette Cayrol: Inferring from Inconsistency in Preference-Based Argumentation Frameworks. 125-169 BibTeX
G. Mashevitzky: Unification Types of Completely Regular Semigroups. 171-182 BibTeX

Fairouz Kamareddine: Special Issue Mechanizing and Automating Mathematics: In honour of N.G. de Bruijn - Preface. 183-188 BibTeX
Grzegorz Bancerek, Piotr Rudnicki: A Compendium of Continuous Lattices in MIZAR. 189-224 BibTeX
Yves Bertot, Nicolas Magaud, Paul Zimmermann: A Proof of GMP Square Root. 225-252 BibTeX
Marc Bezem, Dimitri Hendriks, Hans de Nivelle: Automated Proof Construction in Type Theory Using Resolution. 253-275 BibTeX
Dimitri Hendriks: Proof Reflection in Coq. 277-307 BibTeX
Quang Huy Nguyen, Claude Kirchner, Hélène Kirchner: External Rewriting for Skeptical Proof Assistants. 309-336 BibTeX
Virgile Prevosto, Damien Doligez: Algorithms and Proofs Inheritancey in the FOC Language. 337-363 BibTeX
Freek Wiedijk: A New Implementation of Automath. 365-387 BibTeX
Markus Wenzel, Freek Wiedijk: A Comparison of Mizar and Isar. 389-411 BibTeX