Journal of Automated Reasoning (JAR), Volume 27

Volume 27, Number 1, July 2001

David A. Basin, Amy P. Felty: Current Trends in Logical Frameworks and Metalanguages. 1-2 BibTeX
Paul Callaghan, Zhaohui Luo: An Implementation of LF with Coercive Subtyping & Universes. 3-27 BibTeX
Mirna Bognar, Roel C. de Vrijer: A Calculus of Lambda Calculus Contexts. 29-59 BibTeX
Paula Severi, Nora Szasz: Studies of a Theory of Specifications with Built-in Program Extraction. 61-87 BibTeX

Larry Wos: A Milestone Reached and a Secret Revealed. 89-95 BibTeX
Dolph Ulrich: A Legacy Recalled and a Tradition Continued. 97-122 BibTeX
Robert Veroff: Finding Shortest Proofs: An Application of Linked Inference Rules. 123-139 BibTeX
Kenneth Harris, Branden Fitelson: Distributivity in [Lstrok][aleph]0 and Other Sentential Logics. 141-156 BibTeX
Robert Veroff: Solving Open Questions and Other Challenge Problems Using Proof Sketches. 157-174 BibTeX
Larry Wos: Conquering the Meredith Single Axiom. 175-199 BibTeX
Branden Fitelson, Larry Wos: Missing Proofs Found. 201-225 BibTeX

Geoff Sutcliffe: The CADE-17 ATP System Competition. 227-250 BibTeX
Michael L. Littman, Stephen M. Majercik, Toniann Pitassi: Stochastic Boolean Satisfiability. 251-296 BibTeX
Guido Fiorino: An O(nlog n)-SPACE Decision Procedure for the Propositional Dummett Logic. 297-311 BibTeX
Lifeng He: I-SATCHMO: An Improvement of SATCHMO. 313-322 BibTeX

Ruben Gamboa, Matt Kaufmann: Nonstandard Analysis in ACL2. 323-351 BibTeX
Guilherme Bittencourt, Isabel Tonin: An Algorithm for Dual Transformation in First-Order Logic. 353-389 BibTeX
Piero A. Bonatti: Resolution for Skeptical Stable Model Semantics. 391-421 BibTeX