Using the VIRT programming language for automatic theorem proving

被引：0
|
作者：
Baranovskii, AI [1 ]
机构：
[1] State Inst Artificial Intelligence, Donetsk, Ukraine
来源：
CYBERNETICS AND SYSTEMS ANALYSIS | 1999年 / 35卷 / 06期
关键词：
artificial intelligence; theorem proving; Lisp language; VIRT language; descriptive means of languages; comparison of languages; resolution method; unit binary resolution;
D O I：
10.1007/BF02742284
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
The expressiveness of the VIRT programming language from the viewpoint of theorem proving is discussed. A program of unit binary resolution is proposed. A comparative analysis of the programming languages VIRT and Lisp is performed.
引用
收藏
页码：918 / 929
页数：12
相关论文
共 50 条
  • [1] Using the VIRT programming language for automatic theorem proving
    A. I. Baranovskii
    Cybernetics and Systems Analysis, 1999, 35 : 918 - 929
  • [2] Combining programming with theorem proving
    Chen, CY
    Xi, HW
    ACM SIGPLAN NOTICES, 2005, 40 (09) : 66 - 77
  • [3] EXPLOITING SMALL CLAUSES IN AUTOMATIC THEOREM-PROVING
    LEE, SJ
    COMPUTERS AND ARTIFICIAL INTELLIGENCE, 1993, 12 (03): : 209 - 228
  • [4] Formal Analysis of Language-Based Android Security Using Theorem Proving Approach
    Khan, Wilayat
    Kamran, Muhammad
    Ahmad, Aakash
    Khan, Farrukh Aslam
    Derhab, Abdelouahid
    IEEE ACCESS, 2019, 7 : 16550 - 16560
  • [5] Verifying programs using abstraction and theorem proving
    Qian, Junyan
    Xu, Baowen
    IMECS 2007: INTERNATIONAL MULTICONFERENCE OF ENGINEERS AND COMPUTER SCIENTISTS, VOLS I AND II, 2007, : 1044 - +
  • [6] Formal Availability Analysis Using Theorem Proving
    Ahmed, Waqar
    Hasan, Osman
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2016, 2016, 10009 : 226 - 242
  • [7] Formal Reliability Analysis Using Theorem Proving
    Hasan, Osman
    Tahar, Sofiene
    Abbasi, Naeem
    IEEE TRANSACTIONS ON COMPUTERS, 2010, 59 (05) : 579 - 592
  • [8] On the Formal Analysis of HMM Using Theorem Proving
    Liu, Liya
    Aravantinos, Vincent
    Hasan, Osman
    Tahar, Sofiene
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2014, 2014, 8829 : 316 - 331
  • [9] An approach for lifetime reliability analysis using theorem proving
    Abbasi, Naeem
    Hasan, Osman
    Tahar, Sofiene
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2014, 80 (02) : 323 - 345
  • [10] Evaluation of anonymity and confidentiality protocols using theorem proving
    Mhamdi, Tarek
    Hasan, Osman
    Tahar, Sofiene
    FORMAL METHODS IN SYSTEM DESIGN, 2015, 47 (03) : 265 - 286
12345