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 条
  • [21] Formal Analysis of Linear Control Systems Using Theorem Proving
    Rashid, Adnan
    Hasan, Osman
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2017, 2017, 10610 : 345 - 361
  • [22] Elementary Algebra Proof Exercises Using a Theorem Proving System
    Li, Bing
    Li, Lian
    PRACTICAL APPLICATIONS OF INTELLIGENT SYSTEMS, 2011, 124 : 275 - 280
  • [23] Formalization of Functional Block Diagrams Using HOL Theorem Proving
    Abdelghany, Mohamed
    Tahar, Sofiene
    FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2022, 2022, 13768 : 22 - 35
  • [24] An approach for the formal verification of DSP designs using theorem proving
    Akbarpour, Behzad
    Tahar, Sofiene
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2006, 25 (08) : 1441 - 1457
  • [25] Decision Making as Theorem Proving
    Zhu Mingyuan and Wang ChengweiBeijing Institute of Systems Engineering
    Chinese Journal of Systems Engineering and Electronics, 1993, (01) : 3 - 32
  • [26] Computer Theorem Proving in Mathematics
    Carlos Simpson
    Letters in Mathematical Physics, 2004, 69 : 287 - 315
  • [27] THEOREM PROVING IN THE ONTOLOGY LIFECYCLE
    Katsumi, Megan
    Gruninger, Michael
    KEOD 2010: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON KNOWLEDGE ENGINEERING AND ONTOLOGY DEVELOPMENT, 2010, : 37 - 49
  • [28] Formal reliability analysis of combinational circuits using theorem proving
    Hasan, Osman
    Patel, Jigar
    Tahar, Sofiene
    JOURNAL OF APPLIED LOGIC, 2011, 9 (01) : 41 - 60
  • [29] Theorem proving by chain resolution
    Dehornoy, P
    Marzouk, A
    THEORETICAL COMPUTER SCIENCE, 1998, 206 (1-2) : 163 - 180
  • [30] Computer theorem proving in mathematics
    Simpson, C
    LETTERS IN MATHEMATICAL PHYSICS, 2004, 69 (1) : 287 - 315
12345