zbMATH — the first resource for mathematics

Constructions: A higher order proof system for mechanizing mathematics. (English) Zbl 0581.03007
Computer algebra, EUROCAL ’85, Proc. Eur. Conf., Linz/Austria 1985, Vol. 1, Lect. Notes Comput. Sci. 203, 151-184 (1985).
[For the entire collection see Zbl 0568.00018.]
The paper presents an extensive set of mathematical propositions and proofs demonstrating the power of expression of the theory of constructions as introduced earlier by the authors. Constructions are well-typed expressions of the typed lambda-calculus with the types being lambda-expressions of the same nature. The apparatus was inspired by de Bruin’s Automath, Girard’s second-order types and Martin-Löf’s theory of types. The paper shows that the language of constructions is capable to express notions from various mathematical fields in a concise way and therefore it can serve as a background for a powerful system for automated theorem-proving.
Reviewer: J.Zlatuska

03B35 Mechanization of proofs and logical operations
03B40 Combinatory logic and lambda calculus
03B15 Higher-order logic; type theory (MSC2010)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03F50 Metamathematics of constructive systems
68Q65 Abstract data types; algebraic specification
03F55 Intuitionistic mathematics