Locales - A Sectioning Concept for Isabelle

Locales - A Sectioning Concept for Isabelle
复制标题

区域设置 - Isabelle 的切片概念

DOI：
--
复制
发表时间：
1999
期刊：
International Conference on Theorem Proving in Higher Order Logics
影响因子：
--
通讯作者：
Lawrence Charles Paulson
Lawrence Charles Paulson
中科院分区：
--
文献类型：
--
作者：
F. Kammüller;M. Wenzel;Lawrence Charles Paulson

文献摘要

被引文献

相似文献

Locales是一种定义局部作用域的方法，用于定理证明器Isabelle的交互式证明过程。他们划定了一个范围内的固定的假设，并证明了定理，依赖于这些假设。区域设置还可以包含本地定义的常量，并与漂亮的打印语法相关联。 区域设置可以被看作是一种简单的模块形式。它们类似于AUTOMATH或Coq中的部分。区域用于增强抽象推理和定理证明器的类似应用。本文通过抽象代数推理中的例子来激发locales的概念。它还讨论了一些执行问题。
Locales are a means to define local scopes for the interactive proving process of the theorem prover Isabelle. They delimit a range in which fixed assumption are made, and theorems are proved that depend on these assumptions. A locale may also contain constants defined locally and associated with pretty printing syntax. Locales can be seen as a simple form of modules. They are similar to sections as in AUTOMATH or Coq. Locales are used to enhance abstract reasoning and similar applications of theorem provers. This paper motivates the concept of locales by examples from abstract algebraic reasoning. It also discusses some implementation issues.