On Interpolation and Symbol Elimination in Theory Extensions
From MaRDI portal
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 (13)
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
This page was built for publication: On Interpolation and Symbol Elimination in Theory Extensions
