Abstract Let $$\mathcal{T}$$ T be a theory allowing a form of elimination of existential quantifiers (possibly for formulae in a certain class). We analyze possibilities of constructing (most general) solutions w.r.t. $$\mathcal{T}$$ T for formulae of the form $$\exists x_1 \dots \exists x_n \phi (x_1, \dots , x_n, y_1, \dots , y_m)$$ ∃ x 1 ⋯ ∃ x n ϕ ( x 1 , ⋯ , x n , y 1 , ⋯ , y m ) , where $$\phi $$ ϕ is a quantifier-free conjunction of literals in the signature of $$\mathcal{T}$$ T , and the free variables $$y_1, \dots , y_m$$ y 1 , ⋯ , y m are regarded as parameters. We show that in the presence of function symbols which describe “--” constructions in certain models of $$\mathcal{T}$$ T , we can describe the most general solution of such formulae, thus generalizing results about the existence of most general unifiers in discriminator varieties. We illustrate the ideas on examples.

Abstract We define a notion of general uniform interpolant, generalizing the notions of cover and of uniform interpolant and identify situations in which symbol elimination can be used for computing general uniform interpolants. We investigate the limitations of the method we propose, and identify theory extensions for which the computation of general uniform interpolants can be reduced to symbol elimination followed by the computation of uniform quantifier-free interpolants in extensions with uninterpreted function symbols of theories allowing uniform quantifier-free interpolation.

Abstract We study theP-interpolation property for certain local theory extensions, and use these results for proving $$\le $$ ≤ -interpolation in classes of semilattices with monotone operators. For computing the $$\le $$ ≤ -interpolating terms, we use a hierarchic approach. We use these results for the study of $$\sqsubseteq $$ ⊑ -interpolation in the description logics $$\mathcal{E}\mathcal{L}$$ EL and $$\mathcal{E}\mathcal{L}^+$$ EL+ .

In this paper we study possibilities of using hierarchical reasoning, symbol elimination and model generation for the verification of parametric systems, where the parameters can be constants or functions. Our goal is to automatically provide guarant

In this paper we study possibilities of interpolation and symbol elimination in extensions of a theory $\mathcal{T}_0$ with additional function symbols whose properties are axiomatised using a set of clauses. We analyze situations in which we can perform such tasks in a hierarchical way, relying on existing mechanisms for symbol elimination in $\mathcal{T}_0$. This is for instance possible if the base theory allows quantifier elimination. We analyze possibilities of extending such methods to situations in which the base theory does not allow quantifier elimination but has a model completion which does. We illustrate the method on various examples.

In this paper we show that subsumption problems in lightweight description logics (such as ɛℒ and ɛℒ+) can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras, to obtain uniform PTIME decision procedures for CBox subsumption in ɛℒ, ɛℒ+ and extensions thereof. These locality considerations allow us to present a new family of (possibly many-sorted) logics which extend ɛℒ and ɛℒ+ with n-ary roles and/or numerical domains. As a by-product, this allows us to show that the algebraic models of ɛℒ and ɛℒ+ have ground interpolation and thus that ɛℒ, ɛℒ+, and their extensions studied in this paper have interpolation.

This paper identifies an industrially relevant class of linear hybrid automata (LHA) called reasonable LHA for which parametric verification of safety properties with exhaustive entry conditions can be done in polynomial time and time-bounded reachability with exhaustive entry conditions can be decided in nondeterministic polynomial time for non-parametric verification and in exponential time for parametric verification. Deciding whether an LHA is reasonable is shown to be decidable in polynomial time.

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.

We give a method for deciding unifiability in the variety of bounded distributive lattices. For this, we reduce the problem of deciding whether a unification problem S has a solution to the problem of checking the satisfiability of a set Φ S of ground clauses. This is achieved by using a structure-preserving translation to clause form. The satisfiability check can then be performed by either a resolution-based theorem prover or a SAT checker. We apply the method to unification with free constants and to unification with linear constant restrictions, and show that, in fact, it yields a decision procedure for the positive theory of the variety of bounded distributive lattices. We also consider the problem of unification over (i.e., in an algebraic extension of) the free lattice. Complexity issues are also addressed.