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.