Symbol Elimination and Applications to Parametric Entailment Problems

Abstract

We analyze possibilities of second-order quantifier elimination 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 weakest constraints on parameters which guarantee satisfiability. We identify situations in which entailment between formulae expressed using secondorder quantification can be effectively checked. We illustrate the ideas on an example from wireless network research.

Introduction

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, HResP , 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 consider signatures of the form Π = (S, Σ, Pred), where S is a set of sorts, Σ is a family 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 countable 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 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 (Compf ) 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 LocfΨ 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 (CompfΨ ) 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 |=⊥. Algorithm 1 Symbol elimination in theory extensions [ 23,24 ] 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 firstorder Π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. t d for every domain element d of interpreted sort s and every ground term t that is not a domain element. Let HResP be the calculus containing the following ordered resolution and factorization rules for constrained P -clauses: 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 Rc0 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. HResP if every HResP 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 HResP (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 Rredundancy) w.r.t. HRes P is finite; let N0∗ be the set of clauses in N ∗ not containing P . Let Σpar ⊆ Σ be a set of parameters. If (i) T allows quantifier elimination or (ii) T0 ⊆ T = T0 ∪ K is a local theory extension satisfying condition Ψ (Compf ) 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.

The saturation of a set N of constrained P -clauses up to redundancy under HResP 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 1F1 and G2 ≡T ∃P 2F2 (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 1F1 and G2 ≡T ∃P 2F2. If T is a decidable theory then we can effectively 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 1F1 and G2 ≡T ∃P 2F2, 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 constants 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 elimination and the formulae F1, F2 (hence also G1, G2) contain parametric constants 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:

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 ∀x, y πri(x, y) ∧ πe(x, y) → ⊥ ∀x, y πri(x, y) ∧ πri(y, x) → F (y, x) ∀x, y πe(x, y) → ¬F (x, y) ∀x, y πe(x, y) → ¬F (y, x) ∀x, y F (x, y) → F (y, x)

G2 ∀x, y πri(x, y) ∧ πe(x, y) → ⊥ ∀x, y πe(x, y) ∧ πe(y, x) → ¬F (y, x) ∀x, y πri(x, y) → F (x, y) ∀x, y πri(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 unsatisfiable 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) (g4) πri(a, b) ∧ ¬F (a, b) (g2) πe(a, a) ∧ F (a, a) (g5) πri(a, b) ∧ ¬F (b, a) (g3) F (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).

Cd,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¨oltz 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 u¨ber das Eliminationsproblem der mathematischen Logik . Mathematische Annalen , 110 : 390 -- 413 , 1935 .

2. W. Ackermann . Zum Eliminationsproblem der mathematischen Logik. Mathematische 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 abstraction . In M. P. Bonacina, editor, Automated Deduction - CADE-24 - 24th International 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 . Beitra¨ge zur Algebra der Logik, insbesondere zum Entscheidungsproblem . 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 - Essays 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´e de Li`ege, 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: Foundations 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 fu¨r Informatik, Saarbru¨cken, and in the South African Computer Journal , 1992 .

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. Mo¨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 Workshop on Applications of Kleene Algebra, LNCS 3051 , pages 149 - 162 . Springer, 2004 .

14. K. Hoder , L. Kova´cs, and A. Voronkov . Interpolation and symbol elimination in Vampire . In J. Giesl and R. Ha¨hnle, editors, Automated Reasoning, 5th International 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. Gra¨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 verification . 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 combinations of theories . In J. Giesl and R . Ha¨hnle, editors, Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Proceedings, LNCS 6173 , pages 30 - 45 . Springer, 2010 .

19. L. Kova´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 parametric 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 extensions . In N. Olivetti and A . Tiwari, editors, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings, LNCS 9706 , pages 273 - 289 . Springer, 2016 .

24. V. Sofronie-Stokkermans . On interpolation and symbol elimination in theory extensions . Log. Methods Comput. Sci. , 14 ( 3 ), 2018 .