Combination of uniform interpolants via Beth definability

DOI10.1007/s10817-022-09627-1OpenAlexW4280625473MaRDI QIDQ2090132

Diego Calvanese, Marco Montali, Andrey Rivkin, Alessandro Gianola, Silvio Ghilardi

Publication date: 24 October 2022

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

Full work available at URL: https://doi.org/10.1007/s10817-022-09627-1

zbMATH Keywords

coverstheory combinationuniform interpolationBeth definability

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions

Uses Software

• Mcmt

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-theoretic methods in combined constraint satisfiability
• Uniform interpolation and propositional quantifiers in modal logics
• Interpolation theorems in modal logics. Sufficient conditions
• Model theory.
• An algebraic theory of normal forms
• Model completions and r-Heyting categories
• Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
• Interpolation, amalgamation and combination (the non-disjoint signatures case)
• Uniform interpolation and coherence
• Undefinability of propositional quantifiers in the modal system S4
• Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
• From model completeness to verification of data aware processes
• Model completeness, covers and superposition
• On invariant synthesis for parametric systems
• Uniform interpolation and compact congruences
• Modularity results for interpolation, amalgamation and superamalgamation
• On Interpolation and Symbol Elimination in Theory Extensions
• Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
• Simplification by Cooperating Decision Procedures
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• A sheaf representation and duality for finitely presented Heyting algebras
• Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
• Soundness Verification of Data-Aware Process Models with Variable-to-Variable Conditions
• SMT-based verification of data-aware processes: a model-theoretic approach
• Automated Deduction – CADE-20
• Quantifier-free interpolation in combinations of equality interpolating theories
• Cover Algorithms and Their Combination
• MCMT: A Model Checker Modulo Theories

This page was built for publication: Combination of uniform interpolants via Beth definability