Refine
Year of publication
- 1999 (1)
Document Type
- Article (1) (remove)
Language
- English (1)
Has Fulltext
- yes (1)
Keywords
- second order logic (1) (remove)
Faculty / Organisational entity
In this paper we are interested in using a firstorder theorem prover to prove theorems thatare formulated in some higher order logic. Tothis end we present translations of higher or-der logics into first order logic with flat sortsand equality and give a sufficient criterion forthe soundness of these translations. In addi-tion translations are introduced that are soundand complete with respect to L. Henkin's gen-eral model semantics. Our higher order logicsare based on a restricted type structure in thesense of A. Church, they have typed functionsymbols and predicate symbols, but no sorts.