On Hierarchical Reasoning in Combinations of Theories

DOI10.1007/978-3-642-14203-1_4zbMath1291.03018MaRDI QIDQ5747749

Carsten Ihlemann, Viorica Sofronie-Stokkermans

Publication date: 14 September 2010

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

Full work available at URL: http://hdl.handle.net/11858/00-001M-0000-000F-14B7-2

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

Related Items

Complete instantiation-based interpolation, Hierarchical Reasoning for the Verification of Parametric Systems, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, On invariant synthesis for parametric systems, On Interpolation and Symbol Elimination in Theory Extensions, On First-Order Model-Based Reasoning, Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-theoretic methods in combined constraint satisfiability
• Combining nonstably infinite theories
• The complexity of linear problems in fields
• Model theory.
• Model-companions and definability in existentially complete structures
• Deciding the word problem in the union of equational theories.
• Unions of non-disjoint theories and combinations of satisfiability procedures
• The metamathematics of algebraic systems. Collected papers: 1936-1967. Translated, edited, and provided with supplementary notes by Benjamin Franklin Wells III
• Automated complexity analysis based on ordered resolution
• Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
• Simplification by Cooperating Decision Procedures
• Polynomial Time Uniform Word Problems
• Automatic recognition of tractability in inference relations
• Automated Reasoning
• Automated Deduction – CADE-20
• On Local Reasoning in Verification
• Computer Aided Verification
• Polynomial-time computation via local inference relations
• Verification, Model Checking, and Abstract Interpretation