On combinations of local theory extensions

DOI10.1007/978-3-642-37651-1_16MaRDI QIDQ4916087zbMATH OpenOpenAlexFDO

Authors Viorica Sofronie-Stokkermans

Publication date 19 April 2013

Published in Programming Logics (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0810.2653

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combined logics (03B62)

Abstract: In this paper we study possibilities of efficient reasoning in combinations of theories over possibly non-disjoint signatures. We first present a class of theory extensions (called local extensions) in which hierarchical reasoning is possible, and give several examples from computer science and mathematics in which such extensions occur in a natural way. We then identify situations in which combinations of local extensions of a theory are again local extensions of that theory. We thus obtain criteria both for recognizing wider classes of local theory extensions, and for modular reasoning in combinations of theories over non-disjoint signatures.

Recommendations

• On Hierarchical Reasoning in Combinations of Theories
• Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
• Automated Deduction – CADE-20
• Interpolation in Local Theory Extensions
• Interpolation in local theory extensions

Cites work

• Automated complexity analysis based on ordered resolution
• Automated Deduction – CADE-20
• Automated Reasoning
• Automated reasoning in some local exensions of ordered structures
• Automatic recognition of tractability in inference relations
• Connecting many-sorted theories
• scientific article; zbMATH DE number 3963900 (Why is no real title available?)
• Interpolation in Local Theory Extensions
• Model-theoretic methods in combined constraint satisfiability
• Modular proof systems for partial functions with Evans equality
• Polynomial Time Uniform Word Problems
• Simplification by Cooperating Decision Procedures

Cited in

(12)

• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Local collection and end-extensions of models of compositional truth
• Local splitters for bounded cotorsion theories
• Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
• Interpolation in Local Theory Extensions
• Interpolation in local theory extensions
• The first main theorem on complements: from global to local
• A decidable fragment of second order logic with applications to synthesis
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Automated Deduction – CADE-20
• Automated reasoning in some local exensions of ordered structures
• The theory of (exclusively) local beables

This page was built for publication: On combinations of local theory extensions

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