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
Masahito Kurihara, Hisashi Kondo: Completion for Multiple Reduction Orderings. 25-42
John D. Ramsdell: The Tail-Recursive SECD Machine. 43-62
Tomás Recio, M. P. Vélez: Automatic Discovery of Theorems in Elementary Geometry. 63-82
Alexander Brodsky, Catherine Lassez, Jean-Louis Lassez, Michael J. Maher: Separability of Polyhedra for Optimal Filtering of Spatial and Constraint Data. 83-104

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

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