Combined covers and Beth definability

DOI10.1007/978-3-030-51074-9_11MaRDI QIDQ2096445zbMATH OpenOpenAlexFDO

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

Publication date 9 November 2022

Full work available at URL https://doi.org/10.1007/978-3-030-51074-9_11

Mathematics Subject Classification ID

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

Recommendations

• Combination of uniform interpolants via Beth definability
• Cover Algorithms and Their Combination
• Interpolation, amalgamation and combination (the non-disjoint signatures case)
• Quantifier-free interpolation in combinations of equality interpolating theories
• Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)

Cites work

• scientific article; zbMATH DE number 3485746 (Why is no real title available?)
• scientific article; zbMATH DE number 1140674 (Why is no real title available?)
• scientific article; zbMATH DE number 219032 (Why is no real title available?)
• scientific article; zbMATH DE number 922620 (Why is no real title available?)
• A sheaf representation and duality for finitely presented Heyting algebras
• An algebraic theory of normal forms
• Automated Deduction – CADE-20
• Cover Algorithms and Their Combination
• From model completeness to verification of data aware processes
• Interpolation, amalgamation and combination (the non-disjoint signatures case)
• MCMT: a model checker modulo theories
• Model completeness, covers and superposition
• Model completions and r-Heyting categories
• Model theory.
• Model-theoretic methods in combined constraint satisfiability
• Modularity results for interpolation, amalgamation and superamalgamation
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• On invariant synthesis for parametric systems
• Quantifier-free interpolation in combinations of equality interpolating theories
• SMT-based verification of data-aware processes: a model-theoretic approach
• Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
• Simplification by Cooperating Decision Procedures
• Undefinability of propositional quantifiers in the modal system S4
• Uniform interpolation and coherence
• Uniform interpolation and compact congruences
• Uniform interpolation and propositional quantifiers in modal logics

Cited in

(5)

• Beth definability and the Stone-Weierstrass theorem
• Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions
• Craig interpolation for decidable first-order fragments
• Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
• Combination of uniform interpolants via Beth definability

Describes a project that uses

Uses Software

• Mcmt

This page was built for publication: Combined covers and Beth definability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2096445)