Formalization of Linear Space Theory in the Higher-Order Logic Proving System

被引：1
|
作者：
Zhang, Jie [1 ]
Mao, Danwen [1 ]
Guan, Yong [2 ]
机构：
[1] Beijing Univ Chem Technol, Coll Informat Sci & Technol, Beijing 100029, Peoples R China
[2] Capital Normal Univ, Coll Informat Engn, Beijing 100048, Peoples R China
来源：
JOURNAL OF APPLIED MATHEMATICS | 2013年
关键词：
D O I：
10.1155/2013/218492
中图分类号：
O29 [应用数学];
学科分类号：
070104 ;
摘要：
Theorem proving is an important approach in formal verification. Higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and stronger semantics. Higher-order logic is more expressive. This paper presents the formalization of the linear space theory in HOL4. A set of properties is characterized in HOL4. This result is used to build the underpinnings for the application of higher-order logic in a wider spectrum of engineering applications.
引用
收藏
页数：6
相关论文
共 50 条
  • [1] On the Formalization of Fourier Transform in Higher-order Logic
    Rashid, Adnan
    Hasan, Osman
    INTERACTIVE THEOREM PROVING (ITP 2016), 2016, 9807 : 483 - 490
  • [2] A formalization of abstract argumentation in higher-order logic
    Steen, Alexander
    Fuenmayor, David
    JOURNAL OF LOGIC AND COMPUTATION, 2024, 34 (02) : 229 - 260
  • [3] Formalization of Complex Vectors in Higher-Order Logic
    Afshar, Sanaz Khan
    Aravantinos, Vincent
    Hasan, Osman
    Tahar, Sofiene
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2014, 2014, 8543 : 123 - 137
  • [4] Proving pointer programs in higher-order logic
    Mehta, F
    Nipkow, T
    AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS, 2003, 2741 : 121 - 135
  • [5] Proving pointer programs in higher-order logic
    Mehta, F
    Nipkow, T
    INFORMATION AND COMPUTATION, 2005, 199 (1-2) : 200 - 227
  • [6] Formalization of geometric algebra theories in higher-order logic
    Ma S.
    Shi Z.-P.
    Li L.-M.
    Guan Y.
    Zhang J.
    Song X.
    Shi, Zhi-Ping (zhizp@cnu.edu.cn), 1600, Chinese Academy of Sciences (27): : 497 - 516
  • [7] Towards the Formalization of Fractional Calculus in Higher-Order Logic
    Siddique, Umair
    Hasan, Osman
    Tahar, Sofiene
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2015, 2015, 9150 : 316 - 324
  • [8] Formalization of Reliability Block Diagrams in Higher-order Logic
    Ahmed, Waqar
    Hasan, Osman
    Tahar, Sofiene
    JOURNAL OF APPLIED LOGIC, 2016, 18 : 19 - 41
  • [9] FORMALIZATION OF FRACTIONAL FLOW COMPONENT IN HIGHER -ORDER LOGIC THEOREM PROVING
    Zhao, Chunna
    Jiang, Murong
    Huang, Yaqun
    PROCEEDINGS OF THE ASME INTERNATIONAL DESIGN ENGINEERING TECHNICAL CONFERENCES AND COMPUTERS AND INFORMATION IN ENGINEERING CONFERENCE, 2019, VOL 9, 2019,
  • [10] Graph Representations for Higher-Order Logic and Theorem Proving
    Paliwal, Aditya
    Loos, Sarah M.
    Rabe, Markus N.
    Bansal, Kshitij
    Szegedy, Christian
    THIRTY-FOURTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THE THIRTY-SECOND INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE AND THE TENTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2020, 34 : 2967 - 2974
12345