A Mechanization of Type Theory
Proceedings of the Third International Joint Conference on Artificial Intelligence. Theorem Proving and Logic: 2. Pages 139-145.
Abstract
A refutational system of lo gi c for a l a nguage of orde r w is presented . This langage :i.s a s li ght modif i ca t i on of Church 1 s A-calculus wi th types . The system i s comp lete , in the sense th at a refutation of a set of sentences exists i f and on l y if this set does not possess a general Henk in mode l . Th e main rul e of i nference is a generalizat ion of Robi nson ' s resol u t io n to typ e theo ry , which all ows us to get ri d of the substitut i on r ule.
Gérard P. Huet. 1973. A Mechanization of Type Theory. In Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73. IJCAI, 139–145. https://ijcai.org/proceedings/1973/19
Huet, G. P. (1973). A Mechanization of Type Theory. In Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73 (pp. 139–145). IJCAI. https://ijcai.org/proceedings/1973/19
@inproceedings{ijcai1973p19,
title = {A Mechanization of Type Theory},
author = {Huet, Gérard P.},
booktitle = {Proceedings of the Third International Joint Conference on
Artificial Intelligence, {IJCAI-73}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Nils J. Nilsson},
pages = {139--145},
year = {1973},
month = {8},
note = {Theorem Proving and Logic: 2},
url = {https://ijcai.org/proceedings/1973/19},
}
TY - CPAPER TI - A Mechanization of Type Theory AU - Huet, Gérard P. T2 - Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73 PB - International Joint Conferences on Artificial Intelligence PY - 1973 SP - 139 EP - 145 UR - https://ijcai.org/proceedings/1973/19 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
