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 条
[41]   Is Mathematics Problem Solving or Theorem Proving? [J].
Carlo Cellucci .
Foundations of Science, 2017, 22 :183-199
[42]   Machine Learning for Inductive Theorem Proving [J].
Jiang, Yaqing ;
Papapanagiotou, Petros ;
Fleuriot, Jacques .
ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION (AISC 2018), 2018, 11110 :87-103
[43]   On first-order theorem proving using generalized odd-superpositions Ⅱ [J].
吴尽昭 ;
刘卓军 .
Science in China(Series E:Technological Sciences), 1996, (06) :608-619
[44]   Formalization of bond graph using higher-order-logic theorem proving [J].
Qasim, Ujala ;
Rashid, Adnan ;
Hasan, Osman .
ISA TRANSACTIONS, 2022, 128 :453-469
[45]   A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving [J].
Elderhalli, Yassmeen ;
Hasan, Osman ;
Tahar, Sofiene .
IEEE ACCESS, 2019, 7 :136176-136192
[46]   Event Tree Reliability Analysis of Safety Critical Systems Using Theorem Proving [J].
Abdelghany, Mohamed ;
Ahmad, Waqar ;
Tahar, Sofiene .
IEEE SYSTEMS JOURNAL, 2022, 16 (02) :2899-2910
[47]   Error Analysis and Verification of an IEEE 802.11 OFDM Modem using Theorem Proving [J].
Abdullah, Abu Nasser Mohammed ;
Akbarpour, Behzad ;
Taharc, Sofiene .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 242 (02) :3-30
[48]   Formal Reliability Analysis of an Integrated Power Generation System Using Theorem Proving [J].
Ahmad, Waqar ;
Hasan, Osman ;
Awwad, Falah ;
Bastaki, Nabil ;
Hasan, Syed Rafay .
IEEE SYSTEMS JOURNAL, 2020, 14 (04) :4820-4831
[49]   Maude2Lean: Theorem proving for Maude specifications using Lean [J].
Rubio, Ruben ;
Riesco, Adrian .
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2025, 142
[50]   An Automatic Proving Approach to Parameterized Verification [J].
Li, Yongjian ;
Duan, Kaiqiang ;
Jansen, David N. ;
Pang, Jun ;
Zhang, Lijun ;
Lv, Yi ;
Cai, Shaowei .
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2018, 19 (04)
12345