Multiple-valued logics for theorem-proving in first order logic with equality

被引：0

作者：

Bignall, RJ ^{[1
]}

Spinks, M ^{[1
]}

机构：

[1] Monash Univ, Gippsland Sch Comp & Informat Technol, Churchill, Vic 3842, Australia

来源：

1998 28TH IEEE INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC - PROCEEDINGS | 1998年

关键词：

D O I：

10.1109/ISMVL.1998.679313

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

We outline a method for proving theorems in first-order logic with equality using some equational logics and their associated multiple-valued propositional logics, and describe an application of the method that makes use of the automated theorem-prover Otter to prove a range of theorems from the TPTP library of problems in first-order logic with equality.

引用

页码：102 / 107

页数：6

共 50 条

[21] UNCERTAINTY, ENERGY, AND MULTIPLE-VALUED LOGICS
HAYES, JP
IEEE TRANSACTIONS ON COMPUTERS, 1986, 35 (02) : 107 - 114
[22] Theorem Proving in Higher Order Logics
Goos, Gerhard
Hartmanis, Juris
Van Leeuwen, Jan
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 1999, 1690 : 1 - 8
[23] Issues on adjointness in multiple-valued logics
Morsi, Nehad N.
Roshdy, Elewa M.
INFORMATION SCIENCES, 2006, 176 (19) : 2886 - 2909
[24] EXPERIMENTS WITH A HEURISTIC THEOREM-PROVING PROGRAM FOR PREDICATE CALCULUS WITH EQUALITY
NORTON, LM
ARTIFICIAL INTELLIGENCE, 1971, 2 (3-4) : 261 - 284
[25] Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
Ansotegui, Carlos
Bofill, Miguel
Manya, Felip
Villaret, Mateu
FUZZY SETS AND SYSTEMS, 2016, 292 : 32 - 48
[26] MULTIPLE-VALUED LOGIC FOR OPTOELECTRONICS
ABRAHAM, G
OPTICAL ENGINEERING, 1986, 25 (01) : 3 - 13
[27] A normal form for temporal logics and its applications in theorem-proving and execution
Fisher, M
JOURNAL OF LOGIC AND COMPUTATION, 1997, 7 (04) : 429 - 456
[28] MULTIPLE-VALUED LOGIC - INTRODUCTION
BUTLER, JT
COMPUTER, 1988, 21 (04) : 13 - 15
[29] MULTIPLE-VALUED LOGIC - AN IMPLEMENTATION
DAO, TT
CAMPBELL, DM
OPTICAL ENGINEERING, 1986, 25 (01) : 14 - 21
[30] A Boolean pruning method for improving tableau reasoning efficiency in first-order multiple-valued logics
Liu, Quan
Cui, Zhi-Ming
Sun, Ji-Gui
Yu, Wan-Jun
PROCEEDINGS OF 2006 INTERNATIONAL CONFERENCE ON MACHINE LEARNING AND CYBERNETICS, VOLS 1-7, 2006, : 2548 - +

← 1 2 3 4 5 →