Many-Sorted Equivalence of Shiny and Strongly Polite Theories

被引：8

作者：

Casal, Filipe ^{[1
,2
]}

Rasga, Joao ^{[1
,2
]}

机构：

[1] Univ Lisbon, Inst Super Tecn, Dept Matemat, Lisbon, Portugal

[2] Univ Lisbon, Ctr Matemat Aplicacoes Fundamentais & Invest Oper, Lisbon, Portugal

来源：

JOURNAL OF AUTOMATED REASONING | 2018年 / 60卷 / 02期

关键词：

Nelson-Oppen method; Combination of satisfiability procedures; Shiny theories; Polite theories; Strongly polite theories; First-order logic; Many-sorted logic; NONSTABLY INFINITE THEORIES;

D O I：

10.1007/s10817-017-9411-y

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Herein we close the question of the equivalence of shiny and strongly polite theories by establishing that, for theories with a decidable quantifier-free satisfiability problem, the set of many-sorted shiny theories coincides with the set of many-sorted strongly polite theories. Capitalizing on this equivalence, we obtain a Nelson-Oppen combination theorem for many-sorted shiny theories.

引用

页码：221 / 236

页数：16

共 50 条

[1] Many-Sorted Equivalence of Shiny and Strongly Polite Theories
Filipe Casal
João Rasga
Journal of Automated Reasoning, 2018, 60 : 221 - 236
[2] Many-Sorted Equivalence of Shiny and Strongly Polite Theories
Casal, Filipe (filipe.casal@tecnico.ulisboa.pt), 1600, Springer Science and Business Media B.V. (60):
[3] Morita equivalence of many-sorted algebraic theories
Adámek, J
Sobral, M
Sousa, L
JOURNAL OF ALGEBRA, 2006, 297 (02) : 361 - 371
[4] Morita Equivalence for Many-Sorted Enriched Theories
Dostal, Matej
Velebil, Jiri
APPLIED CATEGORICAL STRUCTURES, 2016, 24 (06) : 825 - 844
[5] Morita Equivalence for Many-Sorted Enriched Theories
Matĕj Dostál
Jiří Velebil
Applied Categorical Structures, 2016, 24 : 825 - 844
[6] Connecting many-sorted theories
Baader, F
Ghilardi, S
AUTOMATED DEDUCTION - CADE-20, PROCEEDINGS, 2005, 3632 : 278 - 294
[7] On many-sorted ω-categorical theories
Casanovas, Enrique
Pelaez, Rodrigo
Ziegler, Martin
FUNDAMENTA MATHEMATICAE, 2011, 214 (03) : 285 - 294
[8] Connecting many-sorted theories
Baader, Franz
Ghilardi, Silvio
JOURNAL OF SYMBOLIC LOGIC, 2007, 72 (02) : 535 - 583
[9] Automorphic Equivalence of Many-Sorted Algebras
A. Tsurkov
Applied Categorical Structures, 2016, 24 : 209 - 240
[10] A NOTE ON INTERPRETATIONS OF MANY-SORTED THEORIES
HOOK, JL
JOURNAL OF SYMBOLIC LOGIC, 1985, 50 (02) : 372 - 374

← 1 2 3 4 5 →