Many-Sorted Equivalence of Shiny and Strongly Polite Theories

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...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2018-02, Vol.60 (2), p.221-236
Main Authors: Casal, Filipe, Rasga, João
Format: Article
Language:English
Subjects:
Artificial Intelligence
Computer Science
Equivalence
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Symbolic and Algebraic Manipulation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-017-9411-y