Many-sorted equivalence of shiny and strongly polite theories

DOI10.1007/S10817-017-9411-YMaRDI QIDQ682380zbMATH OpenOpenAlexFDO

Authors Filipe Casal, João Rasga

Publication date 2 February 2018

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-017-9411-y

zbMATH Keywords

first-order logicmany-sorted logiccombination of satisfiability proceduresNelson-Oppen methodpolite theoriesshiny theoriesstrongly polite theories

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mechanization of proofs and logical operations (03B35)

Recommendations

• Morita equivalence for many-sorted enriched theories
• Morita equivalence of many-sorted algebraic theories
• Automated Deduction – CADE-20
• Connecting many-sorted theories
• scientific article; zbMATH DE number 3970817
• A many-sorted variant of Japaridze's polymodal provability logic
• A note on interpretations of many-sorted theories
• scientific article; zbMATH DE number 4049131
• scientific article; zbMATH DE number 3241262
• First-order theories as many-sorted algebras

Cites work

• scientific article; zbMATH DE number 108068 (Why is no real title available?)
• scientific article; zbMATH DE number 1140674 (Why is no real title available?)
• A gentle non-disjoint combination of satisfiability procedures
• A mathematical introduction to logic.
• Combinations of Theories for Decidable Fragments of First-Order Logic
• Combining nonstably infinite theories
• Combining theories: the Ackerman and guarded fragments
• Complexity, convexity and combinations of theories
• Frontiers of Combining Systems
• Polite theories revisited
• Revisiting the equivalence of shininess and politeness
• Simplification by Cooperating Decision Procedures
• Sorting and selection in posets

Cited in

(7)

• Revisiting the equivalence of shininess and politeness
• Politeness and combination methods for theories with bridging functions
• Combining stable infiniteness and (strong) politeness
• Politeness and stable infiniteness: stronger together
• Politeness for the theory of algebraic datatypes
• Combining Finite Combination Properties: Finite Models and Busy Beavers
• Polite combination of algebraic datatypes

Describes a project that uses

Uses Software

• Algorithm 447

This page was built for publication: Many-sorted equivalence of shiny and strongly polite theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q682380)