首页/论文/1208.1368

arXiv 1208.13682012-08cs.LO

2018年开始使用Isabelle/jEdit

Getting Started with Isabelle/jEdit in 2018

Christian Sternagel

备注：: 5 pages, Isabelle Users Workshop 2012 (updated in 2019)

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

这是对Isabelle/jEdit（证明助手Isabelle的主用户界面）的面向初学者的介绍。

英文摘要：

This is a beginner-oriented introduction to Isabelle/jEdit, the main user interface for the proof assistant Isabelle.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

系统描述：2014年Isabelle/jEdit

System description: Isabelle/jEdit in 2014

这是Isabelle/jEdit的更新系统描述，根据官方发布Isabelle 2014（2014年8月）。解释了以下新的PIDE概念：异步打印功能和文档覆盖，语法和语义完成，编辑器导航，文档模型中辅助文件的管理。

2014-10-30cs.HCcs.LO

Isabelle/jEdit-PIDE框架内的证明程序IDE

Isabelle/jEdit --- a Prover IDE within the PIDE framework

Univ. Paris-Sud（巴黎南大学）；CNRS（法国国家科学研究中心）

PIDE是面向文档的证明器交互和集成的通用框架，基于结合ML和Scala的双语架构。总体目标是将LCF风格的证明器（如Isabelle或Coq或HOL）与JVM平台上的复杂前端技术连接起来，最终克服命令行交互。本系统描述特别涵盖Isabelle/jEdit，作为Isabelle 2011 -1（2011年10月）正式发布的一部分。它是一个具体的Prover IDE实现，一方面基于Isabelle/PIDE库模块（用Scala实现），另一方面基于著名的jEdit文本编辑器框架（用Java实现）。我们的Prover IDE的交互模型遵循连续证明检查的思想：理论源文本由prover在语义信息中进行注释，因为它逐渐变得可用。这通过异步协议工作，既不阻止编辑器也不阻止证明器在多核硬件上利用并行性。jEdit GUI为增强的文本编辑（突出显示、曲线、工具提示、超链接等）提供了标准的隐喻。我们已经从证明者上下文中检测出了形式内容。通过合适的插件和字体对jEdit显示引擎的进一步改进近似于文本缓冲区中的数学渲染，包括来自TeX指令表的符号和子/上标。Isabelle/jEdit在这里既作为当前Isabelle的可用接口，也作为参考应用程序，以激发基于PIDE的进一步项目。

2012-07-14cs.AIcs.LOcs.MS

Isabelle中的交互式化简器追踪与重构

Interactive Simplifier Tracing and Debugging in Isabelle

Isabelle证明助手配备了一个非常强大的术语简化策略。虽然非常有用，但简化术语的结果并不总是与用户的期望相匹配：有时，所得到的术语不是用户期望的形式，或者简化器未能应用规则。我们描述了一个新的，交互式的跟踪设施，它提供了深入了解的层次结构的简化与用户定义的过滤，memoization和搜索。新的验证器跟踪集成到Isabelle/jEdit Prover IDE中。

2014-06-02cs.LOcs.MS

用于与Coq异步交互的PIDE

PIDE for Asynchronous Interaction with Coq

本文介绍了初步的进展，对集成的Coq证明助手与PIDE架构最初开发的伊莎贝尔。该架构旨在与证明助手进行异步、并行交互，并且与允许jEdit编辑器与Isabelle一起工作的插件紧密相关。我们对PIDE架构进行了一些概括，以适应更多的证明器，而不仅仅是Isabelle，并调整Coq以理解核心协议：这在大约两个人工月内交付了一个工作系统。

2014-10-30cs.HCcs.LO

一个伊莎贝尔的Linter：实现与评价

A Linter for Isabelle: Implementation and Evaluation

在交互式定理证明中，形式化质量是开发的可维护性和可重用性的关键因素，也会影响证明检查性能。通常，导致质量问题的反模式对于有经验的用户来说是已知的。然而，在许多定理证明器系统中，没有自动工具来检查它们的存在并使经验不足的用户意识到它们。我们试图通过开发一个linter作为一个公共可用的附加组件来填补Isabelle环境中的这一空白。linter提供了基本的可配置性、可扩展性、Isabelle/jEdit集成和独立的命令行工具。我们在Isabelle/HOL中发现了480个潜在问题，在Isabelle分布的其他形式化中发现了14016个问题，在AFP中发现了惊人的59573个问题。对于AFP提交的特定lint捆绑包，我们发现在1595个案例中违反了提交指南。我们着手缓解Isabelle/HOL中的问题，到目前为止解决了168个问题;我们发现，大多数情况下，高严重性的lint与实际问题相对应，个人用户经常在许多地方犯同样的错误，并且回顾性地解决这些问题需要大量的工作。相比之下，为新开发交互式地解决这些问题通常只会带来很少的开销，正如我们在一个有22名参与者的定量用户调查中发现的那样（超过60%的参与者不到一分钟）。我们还发现，对问题的良好解释是用户容易解决这些问题（相关系数0.48）和他们对最终结果满意度（相关系数0.62）的关键。

2022-07-21cs.LO

并行异步证明中的READ-EVAL-PRINT

READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking

Univ. Paris-Sud（巴黎第十一大学）；CNRS（法国国家科学研究中心）

LCF传统的交互式定理证明，这是由米尔纳在20世纪70年代开始，似乎是绑在经典的读取-评估-打印循环的顺序和同步评估的证明命令。我们打破了这个循环，并将读取-评估-打印阶段改造为并行和异步证明处理的模型。因此，我们解释了Isabelle/Scala方法的一些关键概念，以证明交互和集成，以及Isabelle/jEdit Prover IDE作为前端技术。我们希望再次开启关于ITP系统的非平凡交互模型的科学讨论，并帮助其他老派的证明助手走上类似的道路。

2013-07-08cs.AIcs.HCcs.LO