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 条
  • [31] HUMAN ORIENTED LOGIC FOR AUTOMATIC THEOREM-PROVING
    NEVINS, AJ
    JOURNAL OF THE ACM, 1974, 21 (04) : 606 - 621
  • [32] A new approach for automatic theorem proving in real geometry
    Dolzmann, A
    Sturm, T
    Weispfenning, V
    JOURNAL OF AUTOMATED REASONING, 1998, 21 (03) : 357 - 380
  • [33] ZAPATO: Automatic theorem proving for predicate abstraction refinement
    Ball, T
    Cook, B
    Lahiri, SK
    Zhang, LT
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 457 - 461
  • [34] EXPLOITING SMALL CLAUSES IN AUTOMATIC THEOREM-PROVING
    LEE, SJ
    COMPUTERS AND ARTIFICIAL INTELLIGENCE, 1993, 12 (03): : 209 - 228
  • [35] A case of automatic theorem proving in Euclidean geometry: The Maclane 8(3) theorem
    Conti, P
    Traverso, C
    APPLIED ALGEBRA, ALGEBRAIC ALGORITHMS AND ERROR-CORRECTING CODES, 1995, 948 : 183 - 193
  • [36] A reflective functional language for hardware design and theorem proving
    Grundy, J
    Melham, T
    O'Leary, J
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2006, 16 : 157 - 196
  • [37] Automatic Parallel Programming Using the Descartes Specification Language
    Sakhnini, Nina
    Inukollu, Venkata N.
    Urban, Joseph E.
    2016 7TH INTERNATIONAL CONFERENCE ON INFORMATION AND COMMUNICATION SYSTEMS (ICICS), 2016, : 298 - 303
  • [38] PLATO: A tool to assist programming as term rewriting and theorem proving
    Sampaio, AJ
    Haeberer, AM
    Prates, CT
    Ururahy, CD
    Frias, MF
    Albuquerque, NC
    TAPSOFT '95: THEORY AND PRACTICE OF SOFTWARE DEVELOPMENT, 1995, 915 : 797 - 798
  • [39] AUTOMATED THEOREM-PROVING AND LOGIC PROGRAMMING - A NATURAL SYMBIOSIS
    WOS, L
    MCCUNE, W
    JOURNAL OF LOGIC PROGRAMMING, 1991, 11 (01): : 1 - 53
  • [40] Automatic geometry theorem-proving and automatic geometry problem-solving
    Wu, WT
    AUTOMATED DEDUCTION IN GEOMETRY, PROCEEDINGS, 1999, 1669 : 1 - 13
12345