On connections and higher-order logic (Q908896)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | On connections and higher-order logic |
scientific article |
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
