Automated Deduction in Ring Theory

被引：1

作者：

Padmanabhan, Ranganathan ^{[1
]}

Zhang, Yang ^{[1
]}

机构：

[1] Univ Manitoba, Dept Math, Winnipeg, MB R3T 2N2, Canada

来源：

MATHEMATICAL SOFTWARE, ICMS 2016 | 2016年 / 9725卷

关键词：

Prover9; Otter; Commutativity; Associative rings;

D O I：

10.1007/978-3-319-42432-3_9

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Pover9/Mace4 or its predecessor Otter is one of the powerful automated theorem provers for first-order and equational logic. In this paper we explore various possibilities of using Prover9 in ring theory and semiring theory, in particular, associative rings, rings with involutions, semirings with cancellation laws and near-rings. We code the corresponding axioms in Prover9, check some well-known theorems, for example, Jacobson's commutativity theorem, give some new proofs, and also present some new results.

引用

页码：67 / 74

页数：8

共 50 条

[1] INSTANTIATION THEORY - ON THE FOUNDATIONS OF AUTOMATED DEDUCTION
WILLIAMS, JG
[J]. LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1991, 518 : UR8 - &
[2] AUTOMATED DEDUCTION BY THEORY RESOLUTION.
Stickel, Mark E.
[J]. Journal of Automated Reasoning, 1985, 1 (04) : 333 - 355
[3] An automated deduction system for orthomodular lattice theory
Homer, JK
[J]. ICAI '05: PROCEEDINGS OF THE 2005 INTERNATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOLS 1 AND 2, 2005, : 260 - 265
[4] Automated deduction
[J]. 1600, Morgan Kaufmann Publ Inc, San Mateo, CA, USA (01):
[5] Research in automated deduction as a basis for a probabilistic proof-theory
Forcheri, P
Gentilini, P
Molfino, MT
[J]. LOGIC AND ALGEBRA, 1996, 180 : 491 - 527
[6] AN INTRODUCTION TO AUTOMATED DEDUCTION
STICKEL, ME
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1986, 232 : 75 - 132
[7] AND - AUTOMATED NATURAL DEDUCTION
BARKERPLUMMER, D
BAILIN, SC
MERRILL, AS
[J]. LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1992, 607 : 716 - 720
[8] Automated Deduction for Verification
Shankar, Natarajan
[J]. ACM COMPUTING SURVEYS, 2009, 41 (04)
[9] Automated deduction in von Neumann-Bernays-Goedel set theory
Quaife, Art
[J]. Journal of Automated Reasoning, 1992, 8 (01)
[10] Automated Generation of Exam Sheets for Automated Deduction
Hozzova, Petra
Kovacs, Laura
Rath, Jakob
[J]. INTELLIGENT COMPUTER MATHEMATICS (CICM 2021), 2021, 12833 : 185 - 196

← 1 2 3 4 5 →