## Abstract

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 language | English (US) |
---|---|

Pages | 71-81 |

Number of pages | 11 |

DOIs | |

State | Published - Aug 1 1972 |

Event | 1972 ACM Annual Conference/Annual Meeting, ACM 1972 - Boston, United States Duration: Aug 1 1972 → Aug 1 1972 |

### Conference

Conference | 1972 ACM Annual Conference/Annual Meeting, ACM 1972 |
---|---|

Country/Territory | United States |

City | Boston |

Period | 8/1/72 → 8/1/72 |

## Keywords

- Artificial intelligence
- Higher-order logic
- Theorem proving

## ASJC Scopus subject areas

- Computer Science(all)
- Engineering(all)