Journal of Automated Reasoning (JAR), Volume 23

Volume 23, Number 1, July 1999

Geoff Sutcliffe, Christian B. Suttner: The CADE-15 ATP System Competition. 1-23 BibTeX
Masahito Kurihara, Hisashi Kondo: Completion for Multiple Reduction Orderings. 25-42 BibTeX
John D. Ramsdell: The Tail-Recursive SECD Machine. 43-62 BibTeX
Tomás Recio, M. P. Vélez: Automatic Discovery of Theorems in Elementary Geometry. 63-82 BibTeX
Alexander Brodsky, Catherine Lassez, Jean-Louis Lassez, Michael J. Maher: Separability of Polyhedra for Optimal Filtering of Spatial and Constraint Data. 83-104 BibTeX

Miki Hermann, Phokion G. Kolaitis: Computational Complexity of Simultaneous Elementary Matching Problems. 107-136 BibTeX
Allen Van Gelder: Autarky Pruning in Propositional Model Elimination Reduces Failure Redundancy. 137-193 BibTeX

Piotr Rudnicki, Andrzej Trybulec: On Equivalents of Well-Foundedness. 197-234 BibTeX
Florian Kammüller, Lawrence C. Paulson: A Formal Proof of Sylow's Theorem. 235-264 BibTeX
Ching-Tsun Chou, Doron Peled: Formal Verification of a Partial-Order Reduction Technique for Model Checking. 265-298 BibTeX
Wolfgang Naraschewski, Tobias Nipkow: Type Inference Verified: Algorithm W in Isabelle/HOL. 299-318 BibTeX
Catherine Dubois, Valérie Ménissier-Morain: Certification of a Type Inference Tool for ML: Damas-Milner within Coq. 319-346 BibTeX
Mathieu Jaume: A Full Formalization of SLD-Resolution in the Calculus of Inductive Constructions. 347-371 BibTeX
James McKinna, Robert Pollack: Some Lambda Calculus and Type Theory Formalized. 373-409 BibTeX
Bernhard Reus: Formalizing Synthetic Domain Theory. 411-444 BibTeX
David M. Goldschlag: A Mechanization of Unity in PC-NQTHM-92. 445-498 BibTeX