Providing documentation and testcases for the theorem prover Isabelle

为定理证明者 Isabelle 提供文档和测试用例

• 批准号: 70489253
• 负责人: Dr. Christian Urban
• 金额: --
• 依托单位: Department of Informatics
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2008
• 资助国家: 德国
• 起止时间: 2007-12-31 至 2010-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/70489253?language=en
• 关键词: Providing; documentation; testcases; theorem; prover

Isabelle ist einer der erfolgreichsten interaktiven Theorembeweiser. Er wird seit 20 Jahren entwickelt und wurde mit großem wissenschaftlichen Nutzen in mehreren umfangreichen Verifikationsprojekten eingesetzt. Wir möchten hiermit Gelder beantragen, die für die Dokumentation der API-Schnittstelle und für die Aufstellung einer Sammlung von Testfällen ausgegeben werden können. Damit wollen wir sicherstellen, dass Isabelle langfristig weiterentwickelt werden kann und unabhängige Wissenschaftler ihre Arbeiten auf Isabelle aufbauen können.

伊莎贝尔是一位研究交互式理论的专家。20年来，他一直在努力，并在越来越多的验证项目中获得了大量的科学知识。We möchten hiermit Gelder beantragen，die für die Dokumentation der API-Schnittstelle und für die Aufstellung einer Sammlung von Testfällen ausgegeben韦尔登können.我们希望伊莎贝尔能够在韦尔登的帮助下工作，并且不受科学家的影响。