Many-sorted equivalence of shiny and strongly polite theories

DOI10.1007/s10817-017-9411-yzbMath1425.68370OpenAlexW2593951067MaRDI QIDQ682380

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

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

Related Items (4)

Combining stable infiniteness and (strong) politeness ⋮ Politeness and stable infiniteness: stronger together ⋮ Polite combination of algebraic datatypes ⋮ Politeness for the theory of algebraic datatypes

Uses Software

• Algorithm 447

Cites Work

• Combining nonstably infinite theories
• Complexity, convexity and combinations of theories
• Revisiting the Equivalence of Shininess and Politeness
• Sorting and Selection in Posets
• Combining Theories: The Ackerman and Guarded Fragments
• A Gentle Non-disjoint Combination of Satisfiability Procedures
• Combinations of Theories for Decidable Fragments of First-Order Logic
• Simplification by Cooperating Decision Procedures
• Polite Theories Revisited
• Frontiers of Combining Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item

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