How to Prove Higher Order Theorems in First Order Logic

Kerber, Manfred

How to Prove Higher Order Theorems in First Order Logic

Download BibTeX Cite

Proceedings of the Twelfth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 137-141.

Abstract

In this paper we are interested in using a first order theorem prover to prove theorems that are formulated in some higher order logic. To this end we present translations of higher order logics into first order logic with fiat sorts and equality and give a sufficient criterion for the soundness of these translations. In addition translations are introduced that are sound and complete with respect to L. Henkin's general model semantics. Our higher order logics are based on a restricted type structure in the sense of A. Church, they have typed function symbols and predicate symbols, but no sorts.

Manfred Kerber. 1991. How to Prove Higher Order Theorems in First Order Logic. In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91. IJCAI, 137–141. https://ijcai.org/proceedings/1991/21

@inproceedings{ijcai1991p21,
  title     = {How to Prove Higher Order Theorems in First Order Logic},
  author    = {Kerber, Manfred},
  booktitle = {Proceedings of the Twelfth International Joint Conference on
               Artificial Intelligence, {IJCAI-91}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {John Mylopoulos and Ray Reiter},
  pages     = {137--141},
  year      = {1991},
  month     = {8},
  note      = {Automated Reasoning},
  url       = {https://ijcai.org/proceedings/1991/21},
}

TY  - CPAPER
TI  - How to Prove Higher Order Theorems in First Order Logic
AU  - Kerber, Manfred
T2  - Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1991
SP  - 137
EP  - 141
UR  - https://ijcai.org/proceedings/1991/21
ER  -