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
Volume 23, Number 2, August 1999
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
Volume 23, Numbers 3-4, November 1999
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
Copyright ©
Sun May 17 00:06:23 2009 by
Michael Ley
(
ley@uni-trier.de
)