课题基金 / 基金详情

Verständliche halb-automatische Beweise

Verständliche halb-automatische Beweise
可理解的半自动证据
批准号：
5102236
负责人：
Professor Dr. Tobias Nipkow, Ph.D.
金额：
$0.0万
依托单位：
Lehrstuhl für Informatik XXI: Logik und Verifikation
依托单位国家：
德国
项目类别：
Research Grants
财政年份：
1998
资助国家：
德国
项目状态：
已结题
起止时间：
1997-12-31 至 2002-12-31
来源：
https://gepris.dfg.de/gepris/projekt/5102236?language=en
关键词：
VerstndlichehalbautomatischeBeweise

项目摘要

项目成果

Professor Dr. Tobias Nipkow, Ph.D.的其他基金

相似基金

相关文献

中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
In der Fortsetzung dieses Vorhabens soll zunächst der Autor formaler Beweistexte durch weitergehende Konzepte der Isar Entwicklungsumgebung systematisch unterstützt werden. Ferner soll anstelle der bisher rein am Schriftsatz orientierten Präsentation ein allgemeines Modell für Dokumente mit formal-logischen Inhalten inklusive Beweisen treten; dies eröffnet eine weitere Perspektive der Integration von Isar mit anderen Systemen. Als typisches Anwendungsszenario der Gesamtumgebung soll ferner ein Beispiel zur Theorie objekt-orientierter Programmiersprachen in einer didaktish verwertbaren Form umgesetzt werden.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
Verifizierte Algorithmenanalyse
Verification of Probabilistic Models in Interactive Theorem Provers
Hardening the Hammer: More Integration of Automatic and Interactive Theorem Provers
Security Type Systems and Deduction
海外基金