Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 8, Issue 6, pp. 713-744: Abstract.

Optimized encodings of fragments of type theory in first-order logic

T Tammet and JM Smith

Department of Computing Science, Chalmers University of Technology and Univ. of Goteborg, S-41296 Goteborg, Sweden, E-mail: {tammet, smith}@cs.chalmers.se

The paper presents sound and complete translations of several fragments of Martin-Löf's monomorphic type theory to first-order predicate calculus. The translations are optimized for the purpose of automated theorem proving in the mentioned fragments. The implementation of the theorem prover Gandalf and several experimental results are described.


[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 1998.