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 条
  • [21] Higher-Order Distributions for Differential Linear Logic
    Kerjean, Marie
    Lemay, Jean-Simon Pacaud
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2019, 2019, 11425 : 330 - 347
  • [22] HIGHER-ORDER LOGIC THEOREM-PROVING AND ITS APPLICATIONS - SPECIAL ISSUE
    MELHAM, TF
    COMPUTER JOURNAL, 1995, 38 (02): : 89 - 90
  • [23] Indexed linear logic and higher-order model checking
    Grellois, Charles
    Mellies, Paul-Andre
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (177): : 43 - 52
  • [24] Tutorial: Using TPS for higher-order theorem proving and ETPS for teaching logic
    Andrews, PB
    Brown, CE
    AUTOMATED DEDUCTION - CADE-17, 2000, 1831 : 511 - 512
  • [25] ON HIGHER-ORDER LOGIC
    KOGALOVS.SR
    DOKLADY AKADEMII NAUK SSSR, 1966, 171 (06): : 1272 - &
  • [26] Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
    Maletzky, Alexander
    MATHEMATICAL SOFTWARE, ICMS 2016, 2016, 9725 : 59 - 66
  • [27] On Bisimulation Theory in Linear Higher-Order π-Calculus
    Xu, Xian
    TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY III, 2009, 5800 : 244 - 274
  • [28] Elements of model theory in higher-order fuzzy logic
    Novak, Vilem
    FUZZY SETS AND SYSTEMS, 2012, 205 : 101 - 115
  • [29] Combining Higher-Order Logic with Set Theory Formalizations
    Kaliszyk, Cezary
    Pak, Karol
    JOURNAL OF AUTOMATED REASONING, 2023, 67 (02)
  • [30] Higher-Order Logic or Set Theory: A False Dilemma
    Shapiro, Stewart
    PHILOSOPHIA MATHEMATICA, 2012, 20 (03) : 305 - 323
12345