Superposition-based equality handling for analytic tableaux

被引：0

作者：

Giese, Martin ^{[1
]}

机构：

[1] Austrian Acad Sci, Johann Radon Inst Computat & Appl Math, A-4040 Linz, Austria

来源：

JOURNAL OF AUTOMATED REASONING | 2007年 / 38卷 / 1-3期

关键词：

superposition rules; equality handling; analytic tableaux;

D O I：

10.1007/s10817-006-9050-1

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We present a variant of the basic ordered superposition rules to handle equality in an analytic free-variable tableau calculus. We prove completeness of this calculus by an adaptation of the model generation technique commonly used for completeness proofs of superposition in the context of resolution calculi. The calculi and the completeness proof are compared to earlier results of Degtyarev and Voronkov. Some variations and refinements are discussed.

引用

页码：127 / 153

页数：27

共 8 条

[1] Superposition-based Equality Handling for Analytic Tableaux
Martin Giese
Journal of Automated Reasoning, 2007, 38 : 127 - 153
[2] Database Repairs and Analytic Tableaux
Leopoldo Bertossi
Camilla Schwind
Annals of Mathematics and Artificial Intelligence, 2004, 40 : 5 - 35
[3] Analytic tableaux and model elimination
Coldwell, J
Wrightson, G
AUSTRALIAN COMPUTER JOURNAL, 1998, 30 (01): : 1 - 11
[4] Database repairs and analytic tableaux
Bertossi, L
Schwind, C
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2004, 40 (1-2) : 5 - 35
[5] The proof complexity of analytic and clausal tableaux
Massacci, F
THEORETICAL COMPUTER SCIENCE, 2000, 243 (1-2) : 477 - 487
[6] An Analytic Tableaux Model for Deductive Mastermind Empirically Tested with a Massively Used Online Learning System
Nina Gierasimczuk
Han L. J. van der Maas
Maartje E. J. Raijmakers
Journal of Logic, Language and Information, 2013, 22 : 297 - 314
[7] An Analytic Tableaux Model for Deductive Mastermind Empirically Tested with a Massively Used Online Learning System
Gierasimczuk, Nina
van der Maas, Han L. J.
Raijmakers, Maartje E. J.
JOURNAL OF LOGIC LANGUAGE AND INFORMATION, 2013, 22 (03) : 297 - 314
[8] From Simplified Kripke-Style Semantics to Simplified Analytic Tableaux for Some Normal Modal Logics
Petrukhin, Yaroslav
Zawidzki, Michal
ADVANCES IN ARTIFICIAL INTELLIGENCE, AI*IA 2019, 2019, 11946 : 116 - 131

← 1 →