On Interpolation and Symbol Elimination in Theory Extensions
From MaRDI portal
Publication:2817926
DOI10.1007/978-3-319-40229-1_19zbMath1476.03042arXiv1702.06620OpenAlexW2479293798MaRDI QIDQ2817926
Publication date: 5 September 2016
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1702.06620
Interpolation, preservation, definability (03C40) Quantifier elimination, model completeness, and related topics (03C10)
Related Items
Symbol elimination and applications to parametric entailment problems, Modularity results for interpolation, amalgamation and superamalgamation, Interpolation Results for Arrays with Length and MaxDiff, SMT-based verification of data-aware processes: a model-theoretic approach, Interpolation and amalgamation for arrays with MaxDiff, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes), On Interpolation and Symbol Elimination in Theory Extensions, Model completeness, covers and superposition, NIL: learning nonlinear interpolants, On invariant synthesis for parametric systems, Combination of uniform interpolants via Beth definability, Combined covers and Beth definability
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Model-theoretic methods in combined constraint satisfiability
- Constraint solving for interpolation
- The complexity of linear problems in fields
- Model theory.
- Amalgamation properties and interpolation theorems for equational theories
- Model-companions and definability in existentially complete structures
- A course in model theory. An introduction to contemporary mathematical logic. Transl. from the French by Moses Klein
- Interpolation, amalgamation and combination (the non-disjoint signatures case)
- On Interpolation and Symbol Elimination in Theory Extensions
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
- Interpolation in local theory extensions
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems
- Automatic recognition of tractability in inference relations
- Tools and Algorithms for the Construction and Analysis of Systems
- Automated Deduction – CADE-20
- Quantifier-free interpolation in combinations of equality interpolating theories
- On Local Reasoning in Verification
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Polynomial-time computation via local inference relations
- On Hierarchical Reasoning in Combinations of Theories
- Hierarchical Reasoning for the Verification of Parametric Systems
- Interpolation and Symbol Elimination in Vampire
- Complete instantiation-based interpolation
- Complete instantiation-based interpolation
- Computer Aided Verification
