Uniform interpolants in EUF: algorithms using DAG-representations
From MaRDI portal
Publication:5094130
Authors: Silvio Ghilardi, Alessandro Gianola, Deepak Kapur 
Publication date: 2 August 2022
Full work available at URL: https://arxiv.org/abs/2002.09784
Recommendations
- Uniform interpolation of \(\mathcal{ALC}\)-ontologies using fixpoints
- Uniform interpolation and propositional quantifiers in modal logics
- (Non-)succinctness of uniform interpolants of general terminologies in the description logic \(\mathcal{EL}\)
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Ground Interpolation for the Theory of Equality
Cites Work
- Interpolant strength
- Simplification by Cooperating Decision Procedures
- Model theory.
- Term Rewriting and All That
- On interpolation in automated theorem proving
- Interpolant strength revisited
- Interpolation systems for ground proofs in automated deduction: a survey
- Playing in the grey area of proofs
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Lower bounds for resolution and cutting plane proofs and monotone computations
- MCMT: a model checker modulo theories
- Lazy Abstraction with Interpolants
- Shostak's congruence closure as completion
- Deciding Combinations of Theories
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- An interpolation theorem in the predicate calculus
- Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
- Cover Algorithms and Their Combination
- Conditional congruence closure over uninterpreted and interpreted symbols
Cited In (2)
Uses Software
This page was built for publication: Uniform interpolants in \(\mathcal{EUF}\): algorithms using DAG-representations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5094130)
