N-sorted logic for automatic theorem-proving in higher-order logic

Lawrence Joseph Henschen*

*Corresponding author for this work

Research output: Contribution to conferencePaperpeer-review

6 Scopus citations


This work demonstrates how a first-order logical system with more than one type of individual variable can be used to prove theorems in higher-order logic. Certain of the types are considered to be individuals while other types are treated as predicates and functions. For each pair of types i,j where type i objects are to be predicates over type j objects, a special 2-place predicate symbol P is included which acts as a graph, i.e. P(a,b) iff a(b). The lambda operator could be implemented as a set of comprehension axioms. However, since the axioms needed for a particular theorem are not generally known ahead of time and the inclusion of axioms in a theorem-proving program usually decreases efficiency, a new rule of inference, called naming, is proposed instead. Completeness of the resulting procedure is shown for a small class of higher-order problems. Some suggestions for computer implementation are given.

Original languageEnglish (US)
Number of pages11
StatePublished - Aug 1 1972
Event1972 ACM Annual Conference/Annual Meeting, ACM 1972 - Boston, United States
Duration: Aug 1 1972Aug 1 1972


Conference1972 ACM Annual Conference/Annual Meeting, ACM 1972
Country/TerritoryUnited States


  • Artificial intelligence
  • Higher-order logic
  • Theorem proving

ASJC Scopus subject areas

  • Computer Science(all)
  • Engineering(all)


Dive into the research topics of 'N-sorted logic for automatic theorem-proving in higher-order logic'. Together they form a unique fingerprint.

Cite this