default search action
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. Pilar 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 A. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.