THE COMPLEXITY OF FORMAL PROVING

被引：0
|
作者：
洪加威
机构：
[1] Beijing Computer
来源：
ScienceinChina,SerA. | 1984年 / Ser.A.1984卷 / 10期
关键词：
D O I：
暂无
中图分类号：
学科分类号：
摘要：
<正> In this paper, conceptions of the length, the depth and the width of a proof in a formalsystem are proposed. It is proved that the depth, the width and the logarithm of the lengthare linearly related to each other. Therefore, the proof of any theorem can be highly paral-lelized, which is a completely different conclusion from deterministic computation.
引用
收藏
页码：1046 / 1054
页数：9
相关论文
共 50 条
  • [41] Formal reasoning about systems biology using theorem proving
    Rashid, Adnan
    Hasan, Osman
    Siddique, Umair
    Tahar, Sofiene
    PLOS ONE, 2017, 12 (07):
  • [42] Formal reliability analysis of combinational circuits using theorem proving
    Hasan, Osman
    Patel, Jigar
    Tahar, Sofiene
    JOURNAL OF APPLIED LOGIC, 2011, 9 (01) : 41 - 60
  • [43] Formal complexity, real cognitive complexity and reaction time
    Vylegzhanin, Vasily
    Druzhinin, Yury
    INTERNATIONAL JOURNAL OF PSYCHOLOGY, 2008, 43 (3-4) : 522 - 522
  • [44] PROVING LOWER BOUNDS ON THE MONOTONE COMPLEXITY OF BOOLEAN FUNCTIONS
    WEGENER, I
    LECTURE NOTES IN COMPUTER SCIENCE, 1984, 171 : 446 - 456
  • [45] Towards Formal Fault Tree Analysis Using Theorem Proving
    Ahmed, Waqar
    Hasan, Osman
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2015, 2015, 9150 : 39 - 54
  • [46] Formal Analysis of Linear Control Systems Using Theorem Proving
    Rashid, Adnan
    Hasan, Osman
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2017, 2017, 10610 : 345 - 361
  • [47] Expressing versus Proving: Relating Forms of Complexity in Logic
    Kolokolova, Antonina
    JOURNAL OF LOGIC AND COMPUTATION, 2012, 22 (02) : 267 - 280
  • [48] An approach for the formal verification of DSP designs using theorem proving
    Akbarpour, Behzad
    Tahar, Sofiene
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2006, 25 (08) : 1441 - 1457
  • [49] Theorem proving method for ERM-model formal system
    Babanov, Alexey M.
    Skachkova, Anna S.
    VESTNIK TOMSKOGO GOSUDARSTVENNOGO UNIVERSITETA-UPRAVLENIE VYCHISLITELNAJA TEHNIKA I INFORMATIKA-TOMSK STATE UNIVERSITY JOURNAL OF CONTROL AND COMPUTER SCIENCE, 2010, 11 (02): : 113 - 123
  • [50] A theorem proving framework for the formal verification of Web Services Composition
    Papapanagiotou, Petros
    Fleuriot, Jacques D.
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (61): : 1 - 16
12345