On connections and higher-order logic (Q908896)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: On connections and higher-order logic |
scientific article; zbMATH DE number 4135911
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | On connections and higher-order logic |
scientific article; zbMATH DE number 4135911 |
Statements
On connections and higher-order logic (English)
0 references
1989
0 references
The paper gives a detailed introduction to proving theorems in Church's typed lambda-calculus. The presented method was developed by D. A. Miller and uses expansion trees: an expansion tree is built from the tree-form negation normal form of the formula by adding subtrees with substitution instances to the nodes. Proofs consist of finding a contradictory tree by establishing right connections between parts of the expansion tree. Detailed examples are given.
0 references
connection method
0 references
proving theorems in Church's typed lambda-calculus
0 references
expansion trees
0 references
