On Statman's Finite Completeness Theorem
Logic in Computer Science
2023-09-08 v1
Abstract
We give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the -definability conjecture implies the higher-order matching conjecture.
Keywords
Cite
@article{arxiv.2309.03602,
title = {On Statman's Finite Completeness Theorem},
author = {Richard Statman and Gilles Dowek},
journal= {arXiv preprint arXiv:2309.03602},
year = {2023}
}