A Formal Proof Generator from Semi-formal Proof Documents

机译：来自半正式证明文件的正式证明生成器

获取原文

页面导航

摘要
著录项
相似文献
相关主题

摘要

We present the CafelnMaude Proof Assistant (CiMPA) and the CafelnMaude Proof Generator (CiMPG), two complementary extensions of CafelnMaude, a CafeOBJ interpreter implemented in Maude. CiMPA is a proof assistant for inductive properties of CafeOBJ specifications, and CiMPG generates formal proofs that can be fed into CiMPA from semi-formal proof documents called proof scores in CafeOBJ.

机译：我们介绍了CafelnMaude证明助手（CiMPA）和CafelnMaude证明生成器（CiMPG），这是在Maude中实现的CafeOBJ解释器CafelnMaude的两个补充扩展。 CiMPA是CafeOBJ规范的归纳特性的校对助手，CiMPG生成形式化的校对，可以从在CafeOBJ中称为校对分数的半正式校对文档中将其送入CiMPA。

著录项

来源
《International colloquium on theoretical aspects of computing》|2017年|3-12|共10页
会议地点 Hanoi(VN)
作者
Adrian Riesco; Kazuhiro Ogata;
展开▼
作者单位

Facultad de Informatica Universidad Complutense de Madrid Madrid Spain;

School of Information Science JAIST Nomi Japan Research Center for Theoretical Computer Science JAIST Nomi Japan;

展开▼
会议组织
原文格式 PDF
正文语种
中图分类
关键词

相似文献

外文文献
中文文献
专利

1. Interpreting semi-formal utterances in dialogs about mathematical proofs [J] . Helmut Horacek, Magdalena Wolska Data & Knowledge Engineering . 2006,第1期

机译：在关于数学证明的对话中解释半正式话语
2. Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores [J] . Riesco Adrian, Ogata Kazuhiro ACM transactions on software engineering and methodology . 2018,第2期

机译：证明给我看！从CafeOBJ证明分数推断正式证明脚本
3. Trip to the Proof How I discovered an 'automatic' transcendence proof of the formal power series Pi [J] . Jean-Paul Allouche Nieuw Archief voor Wiskunde . 2018,第4期

机译：追求证明如何发现正式电力系列PI的“自动”超越证明
4. A Formal Proof Generator from Semi-formal Proof Documents [C] . Adrian Riesco, Kazuhiro Ogata International Colloquium on Theoretical Aspects of Computing . 2017

机译：来自半正式证明文件的正式证明发生器
5. Reducing the Costs of Proof Assistant Based Formal Verification or: Conviction without the Burden of Proof. [D] . Tatlock, Zachary Lee. 2014

机译：降低基于证明助手的形式验证的成本或：无需证明负担的定罪。
6. Is there a need for formal undergraduate patient handover training and could an educational workshop effectively provide this? A proof-of-concept study in a Scottish Medical School [O] . Nicholas Holt, Kirsty Crowe, Daniel Lynagh, 2020

机译：是否需要进行正式的本科患者交接培训并且教育研讨会可以有效地提供这种培训吗？苏格兰医学院的概念验证研究
7. Literate proving: presenting and documenting formal proofs [O] . Paul Cairns, Jeremy Gow, Ucl Intereaction Centre 2006

机译：文化证明：呈现和记录正式证明

A Formal Proof Generator from Semi-formal Proof Documents

摘要

著录项

相似文献

相关主题

期刊订阅