## Volume 232,
Numbers 1-2,
6 February 2000

- Didier Galmiche, David J. Pym:

**Proof-search in type-theoretic languages: an introduction.
**5-53

- James L. Caldwell, Ian P. Gent, Judith L. Underwood:

**Search algorithms in type theory.
**55-90

- Raymond McDowell, Dale Miller:

**Cut-elimination for a logic with definitions and induction.
**91-119

- Toshiyasu Arai, Grigori Mints:

**Extended normal form theorems for logical proofs from axioms.
**121-132

- Iliano Cervesato, Joshua S. Hodas, Frank Pfenning:

**Efficient resource management for linear logic proof search.
**133-163

- Martin W. Bunder:

**Proof finding algorithms for implicational logics.
**165-186

- Amy P. Felty:

**The calculus of constructions as a framework for proof search with set variable instantiation.
**187-229

- Didier Galmiche:

**Connection methods in linear logic and proof nets construction.
**231-272

- Gopalan Nadathur:

**Correspondences between classical, intuitionistic and uniform provability.
**273-298

- Eike Ritter, David J. Pym, Lincoln A. Wallen:

**On the intuitionistic force of classical search.
**299-333

Copyright © Fri Mar 12 17:33:09 2010
by Michael Ley (ley@uni-trier.de)