Mechanizing equivalence of regular expression and FA in Isabelle/HOL

被引：0
|
作者：
Wu, Chun-Han [1 ]
Zhang, Xing-Yuan [1 ]
He, Xun [1 ]
机构：
[1] Institute of Command Automation, PLA Univ. of Sci. and Tech., Nanjing 210007, China
来源：
Jiefangjun Ligong Daxue Xuebao/Journal of PLA University of Science and Technology (Natural Science Edition) | 2010年 / 11卷 / 04期
关键词：
D O I：
暂无
中图分类号：
学科分类号：
摘要：
9
引用
收藏
页码：403 / 407
相关论文
共 50 条
  • [1] Mechanizing the Godel Numbering Theory in Isabelle/HOL
    Wang, Lili
    Xie, Jianchun
    PROCEEDINGS OF 2008 INTERNATIONAL PRE-OLYMPIC CONGRESS ON COMPUTER SCIENCE, VOL I: COMPUTER SCIENCE AND ENGINEERING, 2008, : 353 - 358
  • [2] Importing HOL into Isabelle/HOL
    Obua, Steven
    Skalberg, Sebastian
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 298 - 302
  • [3] An interpretation of Isabelle/HOL in HOL Light
    McLaughlin, Sean
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 192 - 204
  • [4] Mechanizing relevant logics with HOL
    Sawamura, H
    Asanuma, D
    THEOREM PROVING IN HIGHER ORDER LOGICS, 1998, 1479 : 443 - 460
  • [5] Safety and Conservativity of Definitions in HOL and Isabelle/HOL
    Kuncar, Ondrej
    Popescu, Andrei
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2 (POPL):
  • [6] Unifying Theories in Isabelle/HOL
    Feliachi, Abderrahmane
    Gaudel, Marie-Claude
    Wolff, Burkhart
    UNIFYING THEORIES OF PROGRAMMING, 2010, 6445 : 188 - +
  • [7] Random testing in Isabelle/HOL
    Berghofer, S
    Nipkow, T
    PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2004, : 230 - 239
  • [8] Nominal techniques in Isabelle/HOL
    Urban, Christian
    JOURNAL OF AUTOMATED REASONING, 2008, 40 (04) : 327 - 356
  • [9] A comparison of PVS and Isabelle/HOL
    Griffioen, D
    Huisman, M
    THEOREM PROVING IN HIGHER ORDER LOGICS, 1998, 1479 : 123 - 142
  • [10] Data Refinement in Isabelle/HOL
    Haftmann, Florian
    Krauss, Alexander
    Kuncar, Ondrej
    Nipkow, Tobias
    INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 : 100 - 115
12345