Reasoning with Inductively Defined Relations in the HOL Theorem Prover

Reasoning with Inductively Defined Relations in the HOL Theorem Prover
复制标题

HOL 定理证明器中的归纳定义关系推理

DOI：
--
复制
发表时间：
1992
期刊：
影响因子：
--
通讯作者：
T. Melham
T. Melham
中科院分区：
--
文献类型：
--
作者：
Juanito Camilleri;T. Melham

文献摘要

被引文献

相似文献

Inductively defined relations are among the basic mathematical tools of computer science. Examples include evaluation and computation relations in structural operational semantics, labelled transition relations in process algebra semantics, inductively-defined typing judgements, and proof systems in general. This paper describes a set of HOL theorem-proving tools for reasoning about such inductively defined relations. We also describe a suite of worked examples using these tools. First printed: August 1992 Parts of this report have previously appeared as: T. Melham, ‘A Package for Inductive Relation Definitions in HOL’, in Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991, edited by M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley (IEEE Computer Society Press, 1992), pp. 350–357.