Combination of uniform interpolants via Beth definability
type: Item
instance of: scholarly article
title: Combination of uniform interpolants via Beth definability
author: Diego Calvanese
author: Silvio Ghilardi
author: Alessandro Gianola
author: Marco Montali
author: Andrey Rivkin
published in: Journal of Automated Reasoning
publication date: 2022-10-24T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7606344
zbMATH Keywords: uniform interpolation
zbMATH Keywords: covers
zbMATH Keywords: theory combination
zbMATH Keywords: Beth definability
describes a project that uses: Mcmt
MaRDI profile type: Publication
full work available at URL: s10817-022-09627-1
OpenAlex ID: W4280625473
cites work: Uniform interpolation and propositional quantifiers in modal logics
cites work: Quantifier-free interpolation in combinations of equality interpolating theories
cites work: From model completeness to verification of data aware processes
cites work: Model completeness, covers and superposition
cites work: SMT-based verification of data-aware processes: a model-theoretic approach
cites work: Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
cites work: Model theory.
cites work: Q5674430
cites work: Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
cites work: Soundness Verification of Data-Aware Process Models with Variable-to-Variable Conditions
cites work: An algebraic theory of normal forms
cites work: Model-theoretic methods in combined constraint satisfiability
cites work: Interpolation, amalgamation and combination (the non-disjoint signatures case)
cites work: Modularity results for interpolation, amalgamation and superamalgamation
cites work: Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
cites work: MCMT: A Model Checker Modulo Theories
cites work: A sheaf representation and duality for finitely presented Heyting algebras
cites work: Undefinability of propositional quantifiers in the modal system S4
cites work: Model completions and r-Heyting categories
cites work: Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
cites work: Q5094130
cites work: Cover Algorithms and Their Combination
cites work: Uniform interpolation and coherence
cites work: Q3875897
cites work: Interpolation theorems in modal logics. Sufficient conditions
cites work: Simplification by Cooperating Decision Procedures
cites work: On invariant synthesis for parametric systems
cites work: On an interpretation of second order quantification in first order intuitionistic propositional logic
cites work: Q4068699
cites work: Q4694581
cites work: On Interpolation and Symbol Elimination in Theory Extensions
cites work: Q4385439
cites work: Uniform interpolation and compact congruences
cites work: Q4893140
cites work: Automated Deduction – CADE-20
DOI: 10.1007/S10817-022-09627-1
description: scientific article; zbMATH DE number 7606344