Formal Proof of Meta-Theorem in First-Order Logic in Coq

被引：0
|
作者：
Wang, Qiming [1 ]
Liu, Jianghao [1 ]
Guo, Dakai [1 ]
Yu, Wensheng [1 ]
机构：
[1] Beijing Univ Posts & Telecommun, Beijing Key Lab Space Ground Interconnect & Conve, Beijing 100876, Peoples R China
来源：
INTELLIGENT NETWORKED THINGS, CINT 2024, PT I | 2024年 / 2138卷
关键词：
Artificial intelligence; First-Order logic; Meta-Theorem; Formalization; Coq;
D O I：
10.1007/978-981-97-3951-6_5
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Formal mathematics is a method to accurately describe and prove mathematical structures and propositions through symbols and inference rules. Formal mathematics is an important part of mathematical mechanization. This paper aims to complete the formal proof of important meta-theorems in first-order logic system within the theorem proving tool Coq. Starting from the symbols of first-order logic language, this paper formally describes the concepts of formula, proof and deduction of first-order logic, and gives the formal verification of the related properties of these concepts. On this basis, the formal proof of important meta-theorems is completed, and the simplification of formula proof sequence is finally realized. The successful verification of the meta-theorem serves as a vital step towards substantiating the validity of first-order logic formulas and culminating in the creation of a comprehensive logical framework. All the codes in this paper are verified by Coq, which fully embodies the reliability, intelligence and interactivity of mathematical theorem proving in Coq.
引用
收藏
页码：45 / 52
页数：8
相关论文
共 50 条
  • [31] Semantical Completeness of First-Order Predicate Logic and the Weak Fan Theorem
    Krivtsov, Victor N.
    STUDIA LOGICA, 2015, 103 (03) : 623 - 638
  • [32] A model generation based theorem prover MGTP for first-order logic
    Hasegawa, Ryuzo
    Fujita, Hiroshi
    Koshimura, Miyuki
    Shirai, Yasuyuki
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2002, 2408 (PART2): : 178 - 213
  • [33] Ultraproduct theorem of first-order lattice-valued logic FM
    Wang, XF
    Xu, Y
    6TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XVI, PROCEEDINGS: COMPUTER SCIENCE III, 2002, : 125 - 129
  • [34] Semantical Completeness of First-Order Predicate Logic and the Weak Fan Theorem
    Victor N. Krivtsov
    Studia Logica, 2015, 103 : 623 - 638
  • [35] A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving
    Crouse, Maxwell
    Abdelaziz, Ibrahim
    Makni, Bassem
    Whitehead, Spencer
    Cornelio, Cristina
    Kapanipathi, Pavan
    Srinivas, Kavitha
    Thost, Veronika
    Witbrock, Michael
    Fokoue, Achille
    THIRTY-FIFTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THIRTY-THIRD CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE AND THE ELEVENTH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2021, 35 : 6279 - 6287
  • [36] A focusing inverse method theorem prover for first-order linear logic
    Chaudhuri, K
    Pfenning, F
    AUTOMATED DEDUCTION - CADE-20, PROCEEDINGS, 2005, 3632 : 69 - 83
  • [37] A model generation based theorem prover MGTP for first-order logic
    Hasegawa, R
    Fujita, H
    Koshimura, M
    Shirai, Y
    COMPUTATIONAL LOGIC: LOGIC PROGRAMMING AND BEYOND, PT II: ESSAYS IN HONOUR OF ROBERT A KOWALSKI, 2002, 2408 : 178 - 213
  • [38] First-Order Modal Logic: Frame Definability and a Lindström Theorem
    R. Zoghifard
    M. Pourmahdian
    Studia Logica, 2018, 106 : 699 - 720
  • [39] A first-order isomorphism theorem
    Allender, E
    Balcazar, J
    Immerman, N
    SIAM JOURNAL ON COMPUTING, 1997, 26 (02) : 557 - 567
  • [40] A FORMAL AND INTUITIONISTIC PROOF OF THE COMPLETENESS THEOREM OF CLASSICAL LOGIC
    Krivine, Jean-Louis
    BULLETIN OF SYMBOLIC LOGIC, 1996, 2 (04) : 405 - 421
12345