=Paper=
{{Paper
|id=Vol-3009/abstract3
|storemode=property
|title=Symbol Elimination and Applications to Parametric Entailment Problems (Abstract)
|pdfUrl=https://ceur-ws.org/Vol-3009/abstract3.pdf
|volume=Vol-3009
|authors=Dennis Peuter,Viorica Sofronie-Stokkermans
|dblpUrl=https://dblp.org/rec/conf/kr/PeuterS21
}}
==Symbol Elimination and Applications to Parametric Entailment Problems (Abstract)==
https://ceur-ws.org/Vol-3009/abstract3.pdf
Symbol Elimination and Applications to
Parametric Entailment Problems
(Abstract)
Dennis Peuter and Viorica Sofronie-Stokkermans
University Koblenz-Landau, Koblenz, Germany
{dpeuter,sofronie}@uni-koblenz.de
Abstract. We analyze possibilities of second-order quantifier elimina-
tion for formulae containing parameters – constants or functions. For
this, we use a constraint resolution calculus obtained from specializing
the hierarchical superposition calculus. If the saturated set of formulae
has a finite representation, we analyze possibilities of obtaining weak-
est constraints on parameters which guarantee satisfiability. We identify
situations in which entailment between formulae expressed using second-
order quantification can be effectively checked. We illustrate the ideas on
an example from wireless network research.
1 Introduction
The motivation for this work was a study of models for graph classes naturally
occurring in wireless network research – in which nodes that are close are always
connected, nodes that are far apart from each other are never connected and
any other node pairs can, but do not need to be connected. Transformations
can be applied to such graphs to make them symmetric; this leads to further
graph classes. When checking inclusion between graph classes described using
transformations we need to check entailment of second-order formulae. If inclu-
sion cannot be proved and the graph class descriptions are parametric we want
to obtain (weakest) conditions on these parameters that guarantee that inclu-
sions hold. This can be achieved by eliminating “non-parametric” constants or
function symbols used in the description of such classes.
We show that it is possible to combine methods for general symbol elimination
(for eliminating existentially quantified predicates) with methods for property-
directed symbol elimination (for obtaining conditions on “parameters” under
which formulae are satisfiable or second-order entailment holds). For general
second-order quantifier elimination we use a form of ordered resolution similar
to that proposed in [11]. For property-directed symbol elimination we use a
Copyright © 2021 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
84 Dennis Peuter and Viorica Sofronie-Stokkermans
method we proposed in [24]. The advantage of using such a two-layered approach
is that it avoids non-termination that might occur if using only general symbol
elimination methods. The main application area we consider in this paper is the
analysis of inclusions between graph classes arising in wireless network research.
The study of second-order quantifier elimination goes back to [7,1,2]. Most of its
known applications are in the study of modal logics or knowledge representation
[12,13]. In [11], Gabbay and Ohlbach proposed a resolution-based algorithm for
second-order quantifier elimination which is implemented in the system SCAN.
In [4], Bachmair et al. mention that hierarchical superposition (cf. [5,6] for further
refinements) can be used for second-order quantifier elimination modulo a theory.
In [19,14], Hoder et al. study possibilities of symbol elimination in inference
systems (e.g. the superposition calculus and its extension with ground linear
rational arithmetic and uninterpreted functions). Since the saturated sets might
be infinite, possibilities of finding finite representations were investigated in the
context of superposition [15] or in verification, in relationship to acceleration
[9,10,3,8]. Orthogonal to this direction of study is the “property-directed” symbol
elimination: Given a theory T and a ground formula G satisfiable w.r.t. T , the
goal is to derive a (weakest) universal formula Γ over a subset of the signature,
such that Γ ∧ G is unsatisfiable w.r.t. T . In [24] we proved that this is possible
for local extensions of theories allowing quantifier elimination.
Structure of the paper. In Sect. 2 we introduce the theoretical results needed
in the paper. In Sect. 3 we present an ordered hierarchical resolution calculus,
HRes P , which can be used for eliminating predicate P , and mention possibilities
of giving finite representations for infinite saturated sets and of investigating the
satisfiability of the saturated sets. In Sect. 4 we use these ideas for checking
entailment and illustrate the method with an example.
This is an abstract containing results published in [21]. Details of the proofs and
additional examples can be found in [20] (which is the extended version of [21]).
2 Local Extensions; Hierarchical Symbol Elimination
We assume known the basic notions in (many-sorted) first-order logic. We con-
sider signatures of the form Π = (S, Σ, Pred), where S is a set of sorts, Σ is a fam-
ily of function symbols and Pred a family of predicate symbols, such that for every
function symbol f (resp. predicate symbol p) their arity a(f ) = s1 . . . sn → s
(resp. a(p) = s1 . . . sm ), where s1 , . . . , sn , s ∈ S, is specified. If C is a fixed count-
able set of fresh constants, we denote by Π C the extension of Π with constants
in C. A Π-structure A is a tuple ({As }s∈S , {fA }f ∈Σ , {pA }p∈Pred ) where for every
function symbol f with arity a(f ) = s1 . . . sn → s, fA : As1 × . . . ×Asn → As ,
and for every predicate symbol p with a(p) = s1 . . . sm , pA ⊆ As1 × . . . ×Asm . If
Π ⊆ Π 0 and A is a Π 0 -structure, we denote its reduct to Π by A|Π .
A theory T can be defined by specifying a set of axioms, or by specifying a
class of structures (the models of the theory). If F and G are formulae we write
F |= G (resp. F |=T G – also written as T ∪ F |= G) to express the fact that
Symbol Elimination and Applications 85
every model of F (resp. every model of F which is also a model of T ) is a model
of G. We write F |=⊥ (resp. F |=T ⊥) to express the fact that F has no model
(resp. that there is no model of T which is a model of F ). A theory T over a
signature Π allows quantifier elimination (QE) if for every formula φ over Π
there exists a quantifier-free formula φ∗ over Π which is equivalent to φ modulo
T . Examples of theories which allow quantifier elimination are rational and real
linear arithmetic (LI(Q), LI(R)) and the theory of real closed fields.
Let Π0 =(Σ0 , Pred) be a signature, and T0 be a “base” theory with signature Π0 .
We consider extensions T := T0 ∪K of T0 with new function symbols Σ (extension
functions) whose properties are axiomatized using a set K of (universally closed)
clauses in the extended signature Π = (Σ0 ∪ Σ, Pred), such that each clause in K
contains function symbols in Σ. Especially well-behaved are the Ψ -local theory
extensions, where Ψ is a suitable closure operator (for details on the properties
of the closure operators we consider we refer to [18]). Ψ -local theory extensions
are extensions T0 ⊆ T0 ∪ K satisfying the following condition:
Ψ
(Locf ) For every finite set G of ground Π C -clauses (for an additional
set C of constants) it holds that T0 ∪ K ∪ G |= ⊥ if and only if
T0 ∪ K[ΨK (G)] ∪ G is unsatisfiable.
where, for every set G of ground Π C -clauses, K[ΨK (G)] is the set of instances
of K in which the terms starting with a function symbol in Σ are in ΨK (G) =
Ψ (est(K, G)), where est(K, G) is the set of ground terms starting with a function
in Σ occurring in G or K. Ψ -local extensions can be recognized by showing that
certain partial models embed into total ones [22,18]. Especially well-behaved are
theory extensions with the property (CompΨ f ) which requires that every partial
model of T whose reduct to Π0 is total and the “set of defined terms” is finite
and closed under Ψ embeds into a total model of T with the same support (cf.
[16,18]). If Ψ is the identity, we denote LocΨ Ψ
f by Locf and Compf by Compf . In
(Ψ )-local theory extensions hierarchical reasoning is possible. If the base theory
allows quantifier elimination, a form of property-directed symbol elimination
is also possible: the symbol elimination problem is hierarchically reduced to a
quantifier elimination problem w.r.t. the base theory.
Theorem 1 ([23,24]) Let T0 be a Π0 -theory allowing quantifier elimination,
Σpar be a set of parameters (function and constant symbols) and Π = (S, Σ, Pred)
be such that Σ ∩ (Σ0 ∪ Σpar ) = ∅. Let K be a set of clauses in the signature
Π0 ∪Σpar ∪Σ in which all variables occur also below functions in Σ1 = Σpar ∪ Σ.
Assume T ⊆ T0 ∪ K satisfies condition (CompΨ f ) for a suitable closure operator
Ψ with est(G) ⊆ ΨK (G) for every set G of ground Π C -clauses. Then Algorithm 1
can be used to construct a universal Π0 ∪ Σpar -formula ∀xΓT (x) such that T0 ∪
∀xΓT (x) ∪ K ∪ G |=⊥ which is entailed by every universal formula Γ with T0 ∪
Γ ∪ K ∪ G |=⊥.
86 Dennis Peuter and Viorica Sofronie-Stokkermans
Algorithm 1 Symbol elimination in theory extensions [23,24]
Input: Theory extension T0 ∪ K with signature Π = Π0 ∪ Σ1 , where Σ1 = Σ ∪ Σpar
where Σpar is a set of parameters
G: set of ground Π C -clauses; T : set of ground Π C -terms with ΨK (G) ⊆ T
Output: ∀yΓT (y) (universal Π0 ∪ Σpar -formula)
Step 1 Purify K[T ] ∪ G (with set of extension symbols Σ1 ). Let K0 ∪ G0 ∪ Con0 be
the set of Π0C -clauses obtained this way.
Step 2 Let G1 = K0 ∪ G0 ∪ Con0 . Among the constants in G1 , we identify
(i) the constants cf , f ∈ Σpar , where cf is a constant parameter or cf is introduced
by a definition cf ≈ f (c1 , . . . , ck ) in the hierarchical reasoning method,
(ii) all constants cp occurring as arguments of functions in Σpar in such definitions.
Replace all the other constants c with existentially quantified variables x (i.e.
replace G1 (cp , cf , c) with ∃xG1 (cp , cf , x)).
Step 3 Construct a formula Γ1 (cp , cf ) equivalent to ∃xG1 (cp , cf , x) w.r.t. T0 using a
method for quantifier elimination in T0 .
Step 4 Replace each constant cf introduced by definition cf = f (c1 , . . . , ck ) with
the term f (c1 , . . . , ck ) in Γ1 (cp , cf ). Let Γ2 (cp ) be the formula obtained this way.
Replace cp with existentially quantified variables y.
Step 5 Let ∀yΓT (y) be ∀y¬Γ2 (y).
3 Second-Order Quantifier Elimination
We consider only the elimination of one predicate; for formulae of the form
∃P1 . . . Pn F the process can be iterated.
Let T be a theory over a many-sorted signature Π = (S, Σ, Pred) where
the set of sorts S = Si ∪ Su consists of a set Si of interpreted sorts and
a set Su of uninterpreted sorts. The models of the theories are Π-structures
A = ({As }s∈S , {fA }f ∈Σ , {pA }p∈Pred ), where each support of interpreted sort is
considered to be fixed. Following the terminology used in [5,6], we will refer to
elements in the fixed domain of sort s ∈ Si as domain elements of sort s.
Let Π 0 = (S, Σ, Pred ∪ {P }), where P 6∈ Pred. Let F be a universal first-
order Π 0 -formula. We can assume, without loss of generality, that F is a set of
clauses of the form ∀x D(x) ∨ C(x), where D(x) is a clause over the signature
Π and C(x) is a clause containing literals of the form (¬)P (x1 , . . . , xn ), where
x1 , . . . , xn are variables1 . Such clauses can also be represented as constrained
clauses in the form ∀x φ(x) || C(x), where φ(x) := ¬D(x). We will refer to
clauses of this form as constrained P -clauses.
Our goal is to compute, if possible, a first-order Π-formula G such that
G ≡T ∃P F .
Let be a strict, well-founded ordering on terms that is compatible with contexts
and stable under substitutions, total on ground terms and with the property that
1
We can bring the clauses to this form using variable abstraction.
Symbol Elimination and Applications 87
t d for every domain element d of interpreted sort s and every ground term t
that is not a domain element. Let HRes P be the calculus containing the following
ordered resolution and factorization rules for constrained P -clauses:
φ1 || P (x) ∨ C φ2 || ¬P (y) ∨ D φ || P (x) ∨ P (y) ∨ C
(φ1 ∧ φ2 )σ || (C ∨ D)σ φσ || (P (x) ∨ C)σ
where (i) σ = mgu(P (x), P (y)) (i) σ = mgu(P (x), P (y))
(ii) P (x)σ is strictly maximal in (P (x) ∨ C)σ (ii) P (x)σ is maximal in
(iii) ¬P (y)σ is maximal in (¬P (y) ∨ D)σ. (P (x) ∨ C)σ
The inference rules are supplemented by a redundancy criterion R = (Rc , Ri )
meant to specify a set Rc of redundant clauses (which can be removed) and a set
Ri of redundant inferences (which do not need to be computed). The following
notion of redundancy R0c for clauses is often used: A (constrained) clause is
redundant w.r.t. a set N of clauses if all its ground instances are entailed w.r.t.
T by ground instances of clauses in N which are strictly smaller w.r.t. . We
will use the following notion of redundancy for inferences: If Rc is a redundancy
criterion for clauses, we say that an inference ι on ground clauses is redundant
w.r.t. N if either one of its premises is redundant w.r.t. N and Rc or, if C0 is the
conclusion of ι then there exist clauses C1 , . . . , Cn ∈ N that are smaller w.r.t.
than the maximal premise of ι and C1 , . . . , Cn |= C0 . A non-ground inference is
redundant if all its ground instances are redundant.
We say that a set of clauses N ∗ is saturated up to R-redundancy w.r.t.
HRes P P ∗
if every HRes inference with premises in N is redundant.
Theorem 2 ([4,21]) Let N be a set of constrained P -clauses over background
theory T , N ∗ its saturation (up to R-redundancy) under HRes P ∗
, and N0 the
set of clauses in N ∗ not containing P . For every model A of T , A is a model of
N0∗ iff there exists a Π 0 -structure B with B |= N and B|Π = A.
If the saturation N ∗ of N under HRes P (up to R-redundancy) is finite, the
universal closure of the conjunction of the clauses in N0∗ is equivalent to ∃P N .
Theorem 3 ([21]) Let T be a theory with signature Π = (S, Σ, Pred), N a
set of constrained P -clauses. Assume that the saturation N ∗ of N (up to R-
redundancy) w.r.t. HRes P ∗ ∗
is finite; let N0 be the set of clauses in N not con-
taining P . Let Σpar ⊆ Σ be a set of parameters. If (i) T allows quantifier elim-
ination or (ii) T0 ⊆ T = T0 ∪ K is a local theory extension satisfying condition
(CompΨ f ) and T0 allows quantifier elimination, then we can use Algorithm 1 to
obtain a (weakest) universal constraint Γ on the parameters such that every
model A of T ∪ Γ is a model of (the universal closure of ) N0∗ , hence A |= ∃P N .
Since the implementations of the hierarchical superposition calculus we are aware
of have as background theory linear arithmetic and in our examples we had more
complex theories, in [21] and [20] we used a form of abstraction first: We renamed
the constraints over more complex theories with new predicate symbols, and used
SCAN [11] for second-order quantifier elimination.
88 Dennis Peuter and Viorica Sofronie-Stokkermans
The saturation of a set N of constrained P -clauses up to redundancy under
HRes P
might be infinite. In [21] we discuss two possibilities of obtaining finite
representations for it: using an encoding of the constraints as minimal models of
suitable sets of constrained Horn clauses [8] or using acceleration [9,10].
4 Checking Entailment
Let T be a theory with signature Π = (S, Σ, Pred), and let P 1 = P11 , . . . , Pn11
and P 2 = P12 , . . . , Pn22 be finite sequences of different predicate symbols with
Pji 6∈ Pred, and Πi = (Σ, Pred ∪ {Pji | 1 ≤ j ≤ ni }) for i = 1, 2.
Let F1 be a universal Π1 -formula and F2 be a universal Π2 -formula. If there exist
Π-formulae G1 and G2 such that G1 ≡T ∃P 1 F1 and G2 ≡T ∃P 2 F2 (which can be
found either by saturation or by using acceleration techniques or other methods)
then ∃P 1 F1 |=T ∃P 2 F2 iff G1 |=T G2 (which is the case iff G1 ∧ ¬G2 |=T ⊥).
Below are some situations in which this can be effectively decided.
Theorem 4 ([21]) Assume that there exist Π-formulae G1 and G2 such that
G1 ≡T ∃P 1 F1 and G2 ≡T ∃P 2 F2 . If T is a decidable theory then we can effec-
tively check whether ∃P 1 F1 |=T ∃P 2 F2 . If T has quantifier elimination and the
formulae F1 , F2 contain parametric constants, we can use quantifier elimination
in T to derive conditions on these parameters under which ∃P 1 F1 |=T ∃P 2 F2 .
Theorem 5 ([21]) Assume that there exist universal Π-formulae G1 and G2
such that G1 ≡T ∃P 1 F1 and G2 ≡T ∃P 2 F2 , and that T = T0 ∪ K, where
T0 is a decidable theory with signature Π0 = (S0 , Σ0 , Pred0 ) where S0 is a
set of interpreted sorts and K is a set of (universally quantified) clauses over
Π = (S0 ∪ S1 , Σ0 ∪ Σ1 , Pred0 ∪ Pred1 ), where (i) S1 is a new set of uninterpreted
sorts, (ii) Σ1 , Pred1 are sets of new function, resp. predicate symbols which have
only arguments of uninterpreted sort ∈ S1 , and all function symbols in Σ1 have
interpreted output sort ∈ S0 . Assume, in addition, that all variables and con-
stants of sort ∈ S1 in K, G1 and ¬G2 occur below function symbols in Σ1 .
We can use the decision procedure for T0 to effectively check whether G1 ∧
¬G2 |=T ⊥ (hence whether ∃P 1 F1 |=T ∃P 2 F2 ). If T0 allows quantifier elim-
ination and the formulae F1 , F2 (hence also G1 , G2 ) contain parametric con-
stants and functions, we can use the property-directed symbol elimination in
Algorithm 1 (cf. Theorem 1) for obtaining a universal formula Γ representing
weakest universal constraints on the parameters under which ∃P 1 F1 |=T ∃P 2 F2 .
We illustrate how the previous results can be used for checking an inclusion
between two classes of graphs of interest in wireless network theory.
Example 1. Let QUDG(r) = (MinDG(r) ∩ MaxDG(1))− be axiomatized by
MinDG(r) ∧ MaxDG(1) ∧ Tr− (E, F ), where r is a function symbol (where r(v)
models the maximum communication distance of node v), and:
Symbol Elimination and Applications 89
MinDG(r) : ∀x, y πri (x, y) → E(x, y) where πri (x, y) = x 6= y ∧ d(x, y) ≤ r(x)
MaxDG(1) : ∀x, y π e (x, y) → ¬E(x, y) where π e (x, y) = d(x, y) > 1
Tr− (E, F ) : ∀x, y (F (x, y) ↔ E(x, y) ∧ E(y, x))
Tr+ (E, F ) : ∀x, y (F (x, y) ↔ E(x, y) ∨ E(y, x)) .
We want to check2 whether A(r) ⊆ B(r), where A(r) = QUDG(r) and B(r) =
(MinDG(r)∩MaxDG(1))+ is described by MinDG(r)∧MaxDG(1)∧Tr+ (E, F ).
We obtain axiomatizations G1 ≡ ∃E(MinDG(r)∧MaxDG(1)∧Tr−(E, F )) for
A(r) and G2 ≡ ∃E(MinDG(r)∧MaxDG(1)∧Tr+(E, F )) for B(r) by eliminating
E. As mentioned before, the implementations of the hierarchical superposition
calculus we are aware of allow only linear arithmetic as a background theory,
whereas in our examples we had more complex theories. This is why we renamed
the constraints over more complex theories with new predicate symbols πri , π e , π t
and used SCAN [11] for second-order quantifier elimination in first-order logic.
We obtained the following formulae:
G1 G2
∀x, y πri (x, y) ∧ π e (x, y) → ⊥ ∀x, y πri (x, y) ∧ π e (x, y) → ⊥
∀x, y πri (x, y) ∧ πri (y, x) → F (y, x) ∀x, y π e (x, y) ∧ π e (y, x) → ¬F (y, x)
∀x, y π e (x, y) → ¬F (x, y) ∀x, y πri (x, y) → F (x, y)
∀x, y π e (x, y) → ¬F (y, x) ∀x, y πri (x, y) → F (y, x)
∀x, y F (x, y) → F (y, x) ∀x, y F (x, y) → F (y, x)
∀x π e (x, x) → ¬F (x, x)
The task is now to check whether G1 |=T G2 , i.e. whether G1 ∧ ¬G2 is unsat-
isfiable w.r.t. T , where ¬G2 is the disjunction of the following ground formulae
(we ignore the negation of the first clause obviously implied by G1 ).
(g1 ) π e (a, b) ∧ π e (b, a) ∧ F (b, a) (g2 ) π e (a, a) ∧ F (a, a) (g3 ) F (a, b) ∧ ¬F (b, a)
(g4 ) πri (a, b) ∧ ¬F (a, b) (g5 ) πri (a, b) ∧ ¬F (b, a)
Here T = Td ∪ UIF r , where Td is a theory describing the properties of d and
r is considered to be an uninterpreted function symbol. In [21] we analyzed
the situations in which Td is one of the theories Tdm = T0 ∪ Km , where Km are
axioms of a metric, Tds , the extension of T0 with a function d satisfying symmetry,
Tdp = T0 ∪ Kp , where Kp = ∀x, y d(x, y) ≥ 0, and Tdu , the extension of T0 with
an uninterpreted function d – where T0 is the disjoint combination of the theory
E of pure equality (sort p) and linear real arithmetic (sort num).
In [21] we proved that all these theories satisfy suitable locality properties.
For testing entailment, by Theorem 5, we can consider the set of all instances
of G1 in which the variables of sort p are replaced with the constants a, b, then
use a method for checking ground satisfiability of G1 [T ] ∧ gi w.r.t. Td ∪ UIF r ,
where Td ∈ {Tdu , Tdp , Tds , Tdm }. For this, we use H-PILoT [17]. This allows us to
check that G1 [T ] ∧ gi is unsatisfiable for i ∈ {1, 2, 3}, but satisfiable for i ∈ {4, 5}
(this is so for all four theories). For cases 4 and 5 we can use Algorithm 1 to
derive conditions on parameters under which G1 [T ] ∧ gi is unsatisfiable. If e.g.
we consider d and r to be parameters, for Tdm we obtain condition
2
To check that the inclusion holds in one given model A we can choose T = Th(A).
90 Dennis Peuter and Viorica Sofronie-Stokkermans
C d,r = ∀x, y(x 6= y ∧ d(x, y) ≤ 1 ∧ d(x, y) ≤ r(x) → d(y, x) ≤ r(y))
(which is true in any model of T in which r is interpreted as a constant function).
For further details cf. [20].
Acknowledgments: We thank Hannes Frey and Lucas Böltz for the numerous
discussions we had on the problems in wireless network research, Renate Schmidt
for maintaining a website where one can run SCAN online and for sending us
the executables and instructions for running them.
References
1. W. Ackermann. Untersuchungen über das Eliminationsproblem der mathematis-
chen Logik. Mathematische Annalen, 110:390—-413, 1935.
2. W. Ackermann. Zum Eliminationsproblem der mathematischen Logik. Mathema-
tische Annalen, 111:61–63, 1935.
3. F. Alberti, S. Ghilardi, and N. Sharygina. Definability of accelerated relations in
a theory of arrays and its applications. In P. Fontaine, C. Ringeissen, and R. A.
Schmidt, editors, Frontiers of Combining Systems - 9th International Symposium,
FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, LNCS 8152,
pages 23–39. Springer, 2013.
4. L. Bachmair, H. Ganzinger, and U. Waldmann. Refutational theorem proving for
hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput., 5:193–212,
1994.
5. P. Baumgartner and U. Waldmann. Hierarchic superposition with weak abstrac-
tion. In M. P. Bonacina, editor, Automated Deduction - CADE-24 - 24th Interna-
tional Conference on Automated Deduction, Proceedings, LNCS 7898, pages 39–57.
Springer, 2013.
6. P. Baumgartner and U. Waldmann. Hierarchic superposition revisited. In C. Lutz,
U. Sattler, C. Tinelli, A. Turhan, and F. Wolter, editors, Description Logic, Theory
Combination, and All That - Essays Dedicated to Franz Baader on the Occasion
of His 60th Birthday, LNCS 11560, pages 15–56. Springer, 2019.
7. H. Behmann. Beiträge zur Algebra der Logik, insbesondere zum Entschei-
dungsproblem. Mathematische Annalen, 86(3-4):163–229, 1922.
8. N. Bjørner, A. Gurfinkel, K. L. McMillan, and A. Rybalchenko. Horn clause
solvers for program verification. In L. D. Beklemishev, A. Blass, N. Dershowitz,
B. Finkbeiner, and W. Schulte, editors, Fields of Logic and Computation II - Es-
says Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, LNCS 9300,
pages 24–51. Springer, 2015.
9. B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis,
Université de Liège, 1998.
10. A. Finkel and J. Leroux. How to compose Presburger-accelerations: Applications to
broadcast protocols. In M. Agrawal and A. Seth, editors, FST TCS 2002: Founda-
tions of Software Technology and Theoretical Computer Science, 22nd Conference,
Proceedings, LNCS 2556, pages 145–156. Springer, 2002.
11. D. M. Gabbay and H. J. Ohlbach. Quantifier elimination in second–order predicate
logic. In B. Nebel, C. Rich, and W. Swartout, editors, Principles of Knowledge
Representation and Reasoning (KR92), pages 425–435. Morgan Kaufmann, 1992.
Also published as a Technical Report MPI-I-92-231, Max-Planck-Institut für In-
formatik, Saarbrücken, and in the South African Computer Journal, 1992.
Symbol Elimination and Applications 91
12. D. M. Gabbay, R. A. Schmidt, and A. Szalas. Second-Order Quantifier Elimination
- Foundations, Computational Aspects and Applications, volume 12 of Studies in
logic : Mathematical logic and foundations. College Publications, 2008.
13. V. Goranko, U. Hustadt, R. A. Schmidt, and D. Vakarelov. SCAN is complete
for all Sahlqvist formulae. In R. Berghammer, B. Möller, and G. Struth, editors,
Relational and Kleene-Algebraic Methods in Computer Science: 7th International
Seminar on Relational Methods in Computer Science and 2nd International Work-
shop on Applications of Kleene Algebra, LNCS 3051, pages 149–162. Springer, 2004.
14. K. Hoder, L. Kovács, and A. Voronkov. Interpolation and symbol elimination in
Vampire. In J. Giesl and R. Hähnle, editors, Automated Reasoning, 5th Interna-
tional Joint Conference, IJCAR 2010, Proceedings, LNCS 6173, pages 188–195.
Springer, 2010.
15. M. Horbach and C. Weidenbach. Deciding the inductive validity of ∀∃∗ queries.
In E. Grädel and R. Kahle, editors, Computer Science Logic, 23rd international
Workshop, CSL 2009, 18th Annual Conference of the EACSL, Proceedings, LNCS
5771, pages 332–347. Springer, 2009.
16. C. Ihlemann, S. Jacobs, and V. Sofronie-Stokkermans. On local reasoning in ver-
ification. In C. R. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for
the Construction and Analysis of Systems, 14th International Conference, TACAS
2008, Held as Part of the Joint European Conferences on Theory and Practice of
Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings,
LNCS 4963, pages 265–281. Springer, 2008.
17. C. Ihlemann and V. Sofronie-Stokkermans. System description: H-PILoT. In R. A.
Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference
on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, LNCS
5663, pages 131–139. Springer, 2009.
18. C. Ihlemann and V. Sofronie-Stokkermans. On hierarchical reasoning in combi-
nations of theories. In J. Giesl and R. Hähnle, editors, Automated Reasoning,
5th International Joint Conference, IJCAR 2010, Proceedings, LNCS 6173, pages
30–45. Springer, 2010.
19. L. Kovács and A. Voronkov. Interpolation and symbol elimination. In R. A.
Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference
on Automated Deduction, Proceedings, LNCS 5663, pages 199–213. Springer, 2009.
20. D. Peuter, P. Marohn, and V. Sofronie-Stokkermans. Symbol elimination for para-
metric second-order entailment problems (with applications to problems in wireless
network theory). CoRR, https://arxiv.org/abs/2107.02333, 2021.
21. D. Peuter and V. Sofronie-Stokkermans. Symbol elimination and applications to
parametric entailment problems. In B. Konev and G. Reger, editors, Frontiers of
Combining Systems - 13th International Symposium, FroCoS 2021, Proceedings,
LNCS 12941, pages 43–62. Springer, 2021.
22. V. Sofronie-Stokkermans. Hierarchic reasoning in local theory extensions. In
R. Nieuwenhuis, editor, Automated Deduction - CADE-20, 20th International
Conference on Automated Deduction, Proceedings, LNCS 3632, pages 219–234.
Springer, 2005.
23. V. Sofronie-Stokkermans. On interpolation and symbol elimination in theory ex-
tensions. In N. Olivetti and A. Tiwari, editors, Automated Reasoning - 8th Inter-
national Joint Conference, IJCAR 2016, Proceedings, LNCS 9706, pages 273–289.
Springer, 2016.
24. V. Sofronie-Stokkermans. On interpolation and symbol elimination in theory ex-
tensions. Log. Methods Comput. Sci., 14(3), 2018.