A Mechanization of Type Theory
Abstract
A refutational system of logic for a language of order w ia presented. This langage is a slight modification of Church's \\-calculus with types. The system is complete, in the sense that a refutation of a set of sentences exists if and only if this set does not possess a general Henkin model. The main rule of inference is a generalization of Robinson's resolution to type theory, which allows us to get rid of the substitution rule.
Cite
Text
Huet. "A Mechanization of Type Theory." International Joint Conference on Artificial Intelligence, 1973.Markdown
[Huet. "A Mechanization of Type Theory." International Joint Conference on Artificial Intelligence, 1973.](https://mlanthology.org/ijcai/1973/huet1973ijcai-mechanization/)BibTeX
@inproceedings{huet1973ijcai-mechanization,
title = {{A Mechanization of Type Theory}},
author = {Huet, Gérard P.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1973},
pages = {139-146},
url = {https://mlanthology.org/ijcai/1973/huet1973ijcai-mechanization/}
}