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] Cancellation Patterns in Automatic Geometric Theorem Proving
Apel, Susanne
Richter-Gebert, Juergen
AUTOMATED DEDUCTION IN GEOMETRY, 2011, 6877 : 1 - 33
[22] SPLITTING AND REDUCTION HEURISTICS IN AUTOMATIC THEOREM PROVING
BLEDSOE, WW
ARTIFICIAL INTELLIGENCE, 1971, 2 (01) : 55 - 77
[23] AUTOMATIC THEOREM-PROVING IN THE ISDV SYSTEM
BEIERLE, C
OLTHOFF, W
VOSS, A
LECTURE NOTES IN COMPUTER SCIENCE, 1986, 230 : 670 - 671
[24] AUTOMATIC THEOREM-PROVING IN COMBINATORICS ON WORDS
Goc, Daniel
Henshall, Dane
Shallit, Jeffrey
INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2013, 24 (06) : 781 - 798
[25] A knowledge markup language and distributed theorem proving
Xu, ZQ
Wang, JB
Wang, NC
PARALLEL AND DISTRIBUTED COMPUTING, APPLICATIONS AND TECHNOLOGIES, PDCAT'2003, PROCEEDINGS, 2003, : 127 - 131
[26] MUSCADET - AN AUTOMATIC THEOREM-PROVING SYSTEM USING KNOWLEDGE AND METAKNOWLEDGE IN MATHEMATICS
PASTRE, D
ARTIFICIAL INTELLIGENCE, 1989, 38 (03) : 257 - 318
[27] Functional Programming and Theorem Proving for Undergraduates: A Progress Report
Page, Rex
Eastlund, Carl
Felleisen, Matthias
FDPE'08: PROCEEDINGS OF THE 2008 ACM SIGPLAN WORKSHOP ON FUNCTIONAL AND DECLARATIVE PROGRAMMING IN EDUCATION, 2008, : 21 - 29
[28] SEMANTICALLY GUIDED DEDUCTIVE SYSTEM FOR AUTOMATIC THEOREM PROVING
REITER, R
IEEE TRANSACTIONS ON COMPUTERS, 1976, 25 (04) : 328 - 334
[29] A New Approach for Automatic Theorem Proving in Real Geometry
Andreas Dolzmann
Thomas Sturm
Volker Weispfenning
Journal of Automated Reasoning, 1998, 21 : 357 - 380
[30] Automatic theorem proving and fuzzy situational search for decisions
Samokhvalov Y.Y.
Cybernetics and Systems Analysis, 2001, 37 (4) : 509 - 514

← 1 2 3 4 5 →