On Hierarchical Reasoning in Combinations of Theories
From MaRDI portal
Publication:5747749
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
03B35: Mechanization of proofs and logical operations
Related Items
Complete instantiation-based interpolation, Hierarchical Reasoning for the Verification of Parametric Systems, Symbol elimination and applications to parametric entailment problems, 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