发帖
雷达卡
摘要翻译：
PIDE是一个面向文档的prover交互和集成的通用框架，基于一个结合了ML和Scala的双语体系结构。总体目标是将Isabelle（或Coq或HOL）等LCF风格的Prover与JVM平台上复杂的前端技术连接起来，最终克服命令行交互。本系统描述特别涵盖Isabelle/Jedit，作为Isabelle2011-1(2011.10)正式发布的一部分。它是一个具体的Prover IDE实现，一方面基于Isabelle/PIDE库模块（用Scala实现），另一方面基于jEdit的文本编辑器框架（用Java实现）。我们的证明者IDE的交互模型遵循了连续证明检查的思想：证明者在理论源文本逐渐变得可用时，用语义信息对其进行注释。这是通过一个异步协议工作的，该协议既不阻止编辑器，也不阻止证明程序利用多核硬件上的并行性。jEdit GUI为增强的文本编辑提供了标准的隐喻（突出显示、弯曲、工具提示、超链接等），我们已经将这些工具用于呈现prover上下文中的正式内容。通过适当的插件和字体对jEdit显示引擎进行进一步的细化，可以近似于文本缓冲区中的数学呈现，包括来自TeX汇辑的符号和子/上标。Isabelle/Jedit在这里既是当前Isabelle的一个可用接口，也是启发基于PIDE的进一步项目的一个参考应用程序。
---
英文标题：
《Isabelle/jEdit --- a Prover IDE within the PIDE framework》
---
作者：
Makarius Wenzel
---
最新提交年份：
2012
---
分类信息：
一级分类：Computer Science 计算机科学
二级分类：Logic in Computer Science 计算机科学中的逻辑
分类描述：Covers all aspects of logic in computer science, including finite model theory, logics of programs, modal logic, and program verification. Programming language semantics should have Programming Languages as the primary subject area. Roughly includes material in ACM Subject Classes D.2.4, F.3.1, F.4.0, F.4.1, and F.4.2; some material in F.4.3 (formal languages) may also be appropriate here, although Computational Complexity is typically the more appropriate subject area.
涵盖计算机科学中逻辑的所有方面，包括有限模型理论，程序逻辑，模态逻辑和程序验证。程序设计语言语义学应该把程序设计语言作为主要的学科领域。大致包括ACM学科类D.2.4、F.3.1、F.4.0、F.4.1和F.4.2中的材料；F.4.3（形式语言）中的一些材料在这里也可能是合适的，尽管计算复杂性通常是更合适的主题领域。
--
一级分类：Computer Science 计算机科学
二级分类：Artificial Intelligence 人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--
一级分类：Computer Science 计算机科学
二级分类：Mathematical Software 数学软件
分类描述：Roughly includes material in ACM Subject Class G.4.
大致包括ACM学科类G.4的材料。
--
---
英文摘要：
PIDE is a general framework for document-oriented prover interaction and integration, based on a bilingual architecture that combines ML and Scala. The overall aim is to connect LCF-style provers like Isabelle (or Coq or HOL) with sophisticated front-end technology on the JVM platform, overcoming command-line interaction at last. The present system description specifically covers Isabelle/jEdit as part of the official release of Isabelle2011-1 (October 2011). It is a concrete Prover IDE implementation based on Isabelle/PIDE library modules (implemented in Scala) on the one hand, and the well-known text editor framework of jEdit (implemented in Java) on the other hand. The interaction model of our Prover IDE follows the idea of continuous proof checking: the theory source text is annotated by semantic information by the prover as it becomes available incrementally. This works via an asynchronous protocol that neither blocks the editor nor stops the prover from exploiting parallelism on multi-core hardware. The jEdit GUI provides standard metaphors for augmented text editing (highlighting, squiggles, tooltips, hyperlinks etc.) that we have instrumented to render the formal content from the prover context. Further refinement of the jEdit display engine via suitable plugins and fonts approximates mathematical rendering in the text buffer, including symbols from the TeX repertoire, and sub-/superscripts. Isabelle/jEdit is presented here both as a usable interface for current Isabelle, and as a reference application to inspire further projects based on PIDE.
---
PDF链接：
https://arxiv.org/pdf/1207.3441
京公网安备 11010802022788号
