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
  

Volume 23, Number 2, August 1999

• 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
  

Volume 23, Numbers 3-4, November 1999

• 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
  

Last update Sat May 18 20:39:05 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page