首页> 外文会议>Intelligent computer mathematics >Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems

【24h】

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems

机译：高可信度交互式定理证明系统中的普遍并行性

获取原文

获取原文并翻译 | 示例

页面导航

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

摘要

Interactive theorem proving is a technology of fundamental importance for mathematics and computer-science. It is based on expressive logical foundations and implemented in a highly trustable way. Applications include huge mathematical proofs and semi-automated verifications of complex software systems. Interactive development of larger and larger proofs increases the demand for computing power, which means explicit parallelism on current multicore hardware.

机译：交互式定理证明是一种对数学和计算机科学至关重要的技术。它基于表达逻辑基础，并以高度可信赖的方式实现。应用程序包括庞大的数学证明和复杂软件系统的半自动验证。越来越大的证据的交互式开发增加了对计算能力的需求，这意味着当前多核硬件上的显式并行性。

著录项

来源
《Intelligent computer mathematics》|2013年|359-363|共5页
会议地点 Bath(GB)
作者
Bruno Barras; Lourdes del Carmen Gonzalez Huesca; Hugo Herbelin; Yann Regis-Gianas; Enrico Tassi; Makarius Wenzel; Burkhart Wolff;
展开▼
作者单位

INRIA, Laboratoire d'Informatique de l'Ecole Polytechnique;

INRIA, Univ. Paris Diderot, Paris, France;

INRIA, Univ. Paris Diderot, Paris, France;

INRIA, Univ. Paris Diderot, Paris, France;

INRIA, Laboratoire d'Informatique de l'Ecole Polytechnique;

Univ. Paris-Sud, Laboratoire LRI, UMR8623, Orsay, F-91405, France CNRS, Orsay, F-91405, France;

Univ. Paris-Sud, Laboratoire LRI, UMR8623, Orsay, F-91405, France CNRS, Orsay, F-91405, France;

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

相似文献

外文文献
中文文献
专利

1. Proof assistance for real-time systems using an interactive theorem prover [J] . Paul Z. Kolano Theoretical computer science . 2002,第1期

机译：使用交互式定理证明器为实时系统提供证明帮助
2. EXPLOITING PARALLELISM: HIGHLY COMPETITIVE SEMANTIC TREE THEOREM PROVER [J] . CHOON KYU KIM International journal of computer mathematics . 2004,第9期

机译：探索并行性：竞争激烈的语义树定理证明
3. STRATEGY PARALLELISM IN AUTOMATED THEOREM PROVING [J] . ANDREAS WOLF, REINHOLD LETZ International Journal of Pattern Recognition and Artificial Intelligence . 1999,第2期

机译：自动定理证明中的策略并行
4. Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems [C] . Bruno Barras, Lourdes del Carmen Gonzalez Huesca, Hugo Herbelin, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning . 2013

机译：高度可信的互动定理证明系统中的普遍存行性
5. On the applications of Interactive Theorem Proving in computational sciences and engineering. [D] . Tahat, Amer. 2016

机译：关于交互式定理证明在计算科学和工程中的应用。
6. Formal reasoning about systems biology using theorem proving [O] . Adnan Rashid, Osman Hasan, Umair Siddique, 2011

机译：使用定理证明关于系统生物学的形式推理
7. Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems [O] . Bruno Barras, Hugo Herbelin, Lourdes Carmen, 2013

机译：高可信交互式定理证明系统中的普适并行

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems

摘要

著录项

相似文献

相关主题

期刊订阅