Uniform interpolants in EUF: algorithms using DAG-representations
From MaRDI portal
Publication:5094130
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
- An interpolation theorem in the predicate calculus
- Conditional congruence closure over uninterpreted and interpreted symbols
- Cover Algorithms and Their Combination
- Deciding Combinations of Theories
- Interpolant strength
- Interpolant strength revisited
- Interpolation systems for ground proofs in automated deduction: a survey
- Lazy Abstraction with Interpolants
- Lower bounds for resolution and cutting plane proofs and monotone computations
- MCMT: a model checker modulo theories
- Model theory.
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- On interpolation in automated theorem proving
- Playing in the grey area of proofs
- Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
- Shostak's congruence closure as completion
- Simplification by Cooperating Decision Procedures
- Term Rewriting and All That
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
Cited in
(2)
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)
