A formulation of the simple theory of types (for Isabelle)
A formulation of the simple theory of types (for Isabelle)
复制标题
简单类型理论的表述（伊莎贝尔）
DOI：
--
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
Lawrence Charles Paulson
中科院分区：
文献类型：
--
作者：
Lawrence Charles Paulson
简单的类型理论是制定使用与生成定理证明伊莎贝尔。这需要显式的类型推理规则。有函数、产品和子集类型，它们可以为空。描述（η-算子）引入了选择公理。高阶逻辑是通过公式和布尔类型项之间的反射获得的。递归类型和函数可以正式构造。
Simple type theory is formulated for use with the genertic theorem prover Isabelle. This requires explicit type inference rules. There are function, product, and subset types, which may be empty. Descriptions (the η-operator) introduce the Axiom of Choice. Higher-order logic is obtained through reflection between formulae and terms of type bool. Recursive types and functions can be formally constructed.