Interpolation in Local Theory Extensions

DOI10.1007/11814771_21MaRDI QIDQ3613412zbMATH OpenOpenAlexFDO

Authors Viorica Sofronie-Stokkermans

Publication date 12 March 2009

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0806.4553

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Abstract: In this paper we study interpolation in local extensions of a base theory. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in the base theory as black-boxes. We present several examples of theory extensions in which interpolants can be computed this way, and discuss applications in verification, knowledge representation, and modular reasoning in combinations of local theories.

Recommendations

• Interpolation in local theory extensions
• Ground Interpolation for Combined Theories
• On combinations of local theory extensions

Cited in

(22)

• Deciding inseparability and conservative extensions in the description logic
• On local modularity and interpolation in entailment systems.
• NIL: learning nonlinear interpolants
• On invariant synthesis for parametric systems
• A new look at localic interpolation theorems
• Applications of hierarchical reasoning in the verification of complex systems
• Labelled interpolation systems for hyper-resolution, clausal, and local proofs
• Automatic verification of combined specifications: an overview
• The Logical Difference Problem for Description Logic Terminologies
• Interpolation in local theory extensions
• A decidability result for the model checking of infinite-state systems
• On combinations of local theory extensions
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Interpolant Generation for UTVPI
• Interpolation and Symbol Elimination
• Quantifier-free interpolation in combinations of equality interpolating theories
• Rewriting interpolants
• On Local Reasoning in Verification
• Constraint solving for interpolation
• Interpolation Results for Arrays with Length and MaxDiff
• On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics $$\mathcal{E}\mathcal{L}, \mathcal{E}\mathcal{L}^+$$
• On symbol elimination and uniform interpolation in theory extensions

This page was built for publication: Interpolation in Local Theory Extensions

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