THE COMPLEXITY OF FORMAL PROVING

被引：0
|
作者：
洪加威
机构：
[1] Beijing Computer Institute
[2] Beijing
来源：
Science China Mathematics | 1984年 / 10期
关键词：
length; THE COMPLEXITY OF FORMAL PROVING;
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 条
  • [1] THE COMPLEXITY OF FORMAL PROVING
    洪加威
    ScienceinChina,SerA., 1984, Ser.A.1984 (10) : 1046 - 1054
  • [2] THE COMPLEXITY OF FORMAL PROVING
    HONG, J
    SCIENTIA SINICA SERIES A-MATHEMATICAL PHYSICAL ASTRONOMICAL & TECHNICAL SCIENCES, 1984, 27 (10): : 1046 - 1054
  • [3] The Complexity of Proving That a Graph Is Ramsey
    Lauria, Massimo
    Pudlak, Pavel
    Roedl, Vojtech
    Thapen, Neil
    AUTOMATA, LANGUAGES, AND PROGRAMMING, PT I, 2013, 7965 : 684 - 695
  • [4] On the Complexity of Proving Polyhedral Reductions
    Amat, Nicolas
    Dal Zilio, Silvano
    Le Botlan, Didier
    FUNDAMENTA INFORMATICAE, 2024, 192 (3-4) : 363 - 394
  • [5] COMPLEXITY OF PROVING PROGRAM CORRECTNESS
    HUNGAR, H
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 526 : 459 - 474
  • [6] The complexity of proving that a graph is Ramsey
    Lauria, Massimo
    Pudlak, Pavel
    Rodl, Vojtch
    Thapen, Neil
    COMBINATORICA, 2017, 37 (02) : 253 - 268
  • [7] The complexity of proving that a graph is Ramsey
    Massimo Lauria
    Pavel Pudlák
    Vojtěch Rödl
    Neil Thapen
    Combinatorica, 2017, 37 : 253 - 268
  • [8] A formal method for proving programs correct
    Chiang, CC
    Neubart, D
    2001 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-5: E-SYSTEMS AND E-MAN FOR CYBERNETICS IN CYBERSPACE, 2002, : 718 - 723
  • [9] Formal Availability Analysis Using Theorem Proving
    Ahmed, Waqar
    Hasan, Osman
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2016, 2016, 10009 : 226 - 242
  • [10] Formal Reliability Analysis Using Theorem Proving
    Hasan, Osman
    Tahar, Sofiene
    Abbasi, Naeem
    IEEE TRANSACTIONS ON COMPUTERS, 2010, 59 (05) : 579 - 592
12345