=Paper=
{{Paper
|id=Vol-2013/paper17
|storemode=property
|title=Approximating Resultants of Existential Second-Order Quantifier Elimination upon Universal Relational First-Order Formulas
|pdfUrl=https://ceur-ws.org/Vol-2013/paper17.pdf
|volume=Vol-2013
|authors=Christoph Wernhard
|dblpUrl=https://dblp.org/rec/conf/soqe/Wernhard17
}}
==Approximating Resultants of Existential Second-Order Quantifier Elimination upon Universal Relational First-Order Formulas==
https://ceur-ws.org/Vol-2013/paper17.pdf
82
Approximating Resultants of
Existential Second-Order Quantifier Elimination
upon Universal Relational First-Order Formulas
Christoph Wernhard
TU Dresden, Germany
Abstract. We investigate second-order quantifier elimination for a class
of formulas characterized by a restriction on the quantifier prefix: exis-
tential predicate quantifiers followed by universal individual quantifiers
and a relational matrix. For a given second-order formula of this class
a possibly infinite sequence of universal first-order formulas that have
increasing strength and are all entailed by the second-order formula can
be constructed. Any first-order consequence of the second-order formula
is a consequence of some member of the sequence. The sequence provides
a recursive base for the first-order theory of the second-order formula,
in the sense investigated by Craig. The restricted formula class allows
to derive further properties, for example that the set of those mem-
bers of the sequence that are equivalent to the second-order formula, or,
more generally, have the same first-order consequences, is co-recursively
enumerable. Also the set of first-order formulas that entails the second-
order formula is co-recursively enumerable. These properties are proven
with formula-based tools used in automated deduction, such as domain
closure axioms, eliminating individual quantifiers by ground expansion,
predicate quantifier elimination with Ackermann’s Lemma, Craig inter-
polation and decidability of the Bernays-Schönfinkel-Ramsey class.
1 Introduction
The objective of second-order quantifier elimination is to compute from a given
second-order formula a so-called resultant (from German Resultante, used by
Schröder [17]), that is, an equivalent first-order formula. Finding such a resul-
tant is not in general possible for arbitrary second-order formulas. The early
technical investigations of second-order quantifier elimination on the basis of
first-order logic were done jointly with the early investigations of the decision
problem: Löwenheim [14], Skolem [18] and Behmann [3] gave decision methods
for relational1 monadic2 formulas with equality. Their methods are based on
existentially quantifying upon all predicates in the formula to decide and com-
puting a resultant by elimination. The obtained resultant of a relational monadic
formula is then a truth value constant or a formula that just constrains domain
cardinality (see, e.g., [23]).
Whereas much is known today about decidable fragments of first-order logic,
see, e.g., [4], knowledge about fragments on which second-order quantifier elim-
1
No function symbols with exception of individual constants.
2
No predicate symbols with arity larger than one.
Copyright c 2017 by the paper’s authors
In: P. Koopmann, S. Rudolph, R. Schmidt, C. Wernhard (eds.): SOQE 2017 – Pro-
ceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics,
Dresden, Germany, December 6–8, 2017, published at http://ceur-ws.org.
83
ination succeeds seems still scarce [12]. Ackermann [1] was the first to publish3
a proof that second-order quantifier elimination on the basis of first-order logic
does not succeed in general, by means of a second-order formalization of the
induction axiom. Conradie [5] formulated quite specific syntactic conditions un-
der which the modern DLS algorithm [7] for second-order quantifier elimina-
tion succeeds. However, it appears that for the case of simultaneous elimination
of multiple existential predicate quantifiers only a sufficient condition has been
found. In addition, DLS as considered there does not cover the relational monadic
case. Van Benthem and Doets [21] consider three classes of relational formulas
with existential second-order quantifier prefix, distinguished by the subsequent
first-order quantifier prefix: existential first-order quantifiers, universal first-order
quantifiers, and first-order quantifier prefixes of the form ∀x1 . . . ∀xm ∃y1 . . . ∃yn .4
As shown in [21], formulas with arbitrary further first-order prefixes can be con-
verted to the latter class by Skolemization. For the second class, it is sketched in
[21] with model theoretic arguments that a resultant exists which is an (infinite)
disjunction of an (infinite) conjunction of first-order formulas.
Here we will take a closer look on that second class, applying formula-based
tools that are used in automated deduction. In particular, our toolkit comprises
domain closure axioms as familiar from logical modeling of database semantics,
formula normalization and elimination of first-order quantifiers by ground ex-
pansion, second-order quantifier elimination by rewriting with an equivalence of
a second-order formula of a certain form to a first-order formula (Ackermann’s
Lemma [1]), a strengthening of Craig interpolation that can be proven with a
tableau technique, and decidability of the Bernays-Schönfinkel-Ramsey class.
The main original motivation was to explore possible foundations for applying
instance-based [2] techniques as known for theorem proving also to solve elim-
ination tasks. Their underlying principle is Herbrand’s theorem, which justifies
reducing unsatisfiability of a first-order formula to unsatisfiability of a propo-
sitional formula obtained by eliminating first-order quantifiers through ground
expansion with terms constructed from the input vocabulary. The general idea of
instance-based methods for theorem proving is to successively generate conjunc-
tions of instances of the universally quantified input formulas and test these for
propositional unsatisfiability. In presence of various techniques to avoid naive
explicit expansion and the ability of recent SAT solvers to handle quite large
propositional formulas this a practically feasible approach to first-order theorem
proving. Thus, the question came up, whether there are quantifier-free formula
expansions that are large enough to ensure that elimination can be performed
on these instead of the original formula, in analogy to detecting unsatisfiability.
With the expectation of considering an important but somehow easier spe-
cial case we focus on relational formulas, which underlie most formalizations
of databases. Of course, functions can be represented by predicates, such that
3
[15, p. 336] and a letter by Ackermann dated 1 November 1928 [22] suggest that
Löwenheim earlier obtained similar results.
4
That these classes are restricted to relational formulas can be guessed from the
symbolic notation in [21] (actually only the case with a single unquantifed predi-
cate seems considered there) and the observation that if function symbols would be
permitted, then the second class would be as expressive as the third one.
84
without restriction on quantification, the relational property is not a limitation
of expressive power. We focus on the restriction to universal relational formu-
las. In Skolemized form, formulas of the Bernays-Schönfinkel-Ramsey class are
such formulas. Typically, in contrast to many resolution-based methods [10],
instance-based methods decide universal relational formulas. An intuitive argu-
ment is that these formulas trivially have a largest expansion that needs to be
considered to determine satisfiability. Do they also have in some sense a largest
expansion that needs to be considered for elimination?
The obtained results are not as positive as desired, but at least shed some
light on the properties of elimination problems with certain quantification re-
strictions. The considered formulas have an existential second-order quantifier
prefix, followed by a universal first-order prefix and a quantifier-free formula. It
is shown that for such a second-order formula F a sequence {G0 , G1 , G2 , . . .}
of universal relational first-order formulas that have (not necessarily strictly)
increasing strength and are all entailed by F can be constructed. Any first-order
consequence of F is a consequence of some Gi . Formula F has a resultant if and
only if it is equivalent to some Gi . The set of the formulas Gi that constitute a
resultant of F or, more generally, have the same first-order consequences as F
is co-recursively enumerable. Also the set of first-order formulas that entail F is
co-recursively enumerable.
Craig [6] considered the question of constructing a so-called base for a given
formula with existential second-order prefix, that is, a recursive set of first-
order formulas whose set of consequences is identical to the set of first-order
consequences of the given second-order formula. He notes that this corresponds
to a weakened version of Ackermann’s [1] generalized notion of resultant. Our
construction of {G0 , G1 , G2 , . . .} can be viewed as construction of a monotonic
base, actually with similar techniques as in [6], but where the restriction to
universal relational formulas allows to derive additional properties.
The rest of the paper is structured as follows: Notation and definitions of
the considered formula classes are introduced in Sect. 2 and the toolkit of the
used techniques is specified in Sect. 3. In Sect. 4 then the main results are
stated, proven and informally described, followed by a discussion of related work,
potential applications and open issues in Sect. 5. Section 6 concludes the paper.
2 Notation and Preliminaries
We consider second-order formulas where second-order quantification is just
upon predicates (in contrast to functions), or, in other words, first-order formulas
extended by second-order quantification upon predicates. They are constructed
from atoms (including equality atoms), constant operators >, ⊥, the unary op-
erator ¬, binary operators ∧, ∨ and quantifiers ∀, ∃ with their usual meaning.
Further binary operators →, ←, ↔, as well as n-ary versions of ∧ and ∨ can be
understood as meta-level notation. The operators ∧ and ∨ bind stronger than
→, ← and ↔. The scope of ¬, the quantifiers, and the n-ary connectives is the
immediate subformula to the right.
85
A subformula occurrence has in a given formula positive (negative) polarity if
it is in the scope of an even (odd) number of negations. A vocabulary is a set of
symbols, that is, predicate symbols (briefly predicates), function symbols (briefly
functions) and individual symbols. (Function symbols are assumed to have an
arity ≥ 1. Individual symbols are not partitioned into variables and constants.
Thus, an individual symbol is – like a predicate in second-order logic – considered
as variable if and only if it is bound by a quantifier.) The set of symbols that
occur free in a formula F is denoted by V(F ), the set of predicate symbols that
occur free in F by VP (F ), and the set of individual symbols that occur free in F
(commonly termed the set of constants occurring in F ) by VC (F ). The arity of
a predicate or function symbol s is denoted by arity(s).
We use straightforward shorthands based on sequences of terms for expressing
application of predicates and functions to arguments, simultaneous comparison
of multiple terms and quantifying upon multiple variables: If t = t1 , . . . , tn is
an n-ary sequence of terms, and s is an n-ary predicate or function symbol, we
write st for s(t1 , . . . , tn ), or, in case n = 0, for s, respectively. If t = t1 , . . . , tn
and u = u1 , . . . , un are both n-ary sequences of terms, we write t = u for
t1 = u1 ∧ . . . ∧ tn = un and t 6= u for ¬(t = u). If x = x1 , . . . , xn is a sequence
of individual symbols or of predicates, we write ∃s (∀s, resp.) for ∃s1 . . . ∃sn
(∀s1 . . . ∀sn , resp.).
We consider three specific formula classes whose members are constructed as
a second-order quantifier prefix followed by a first-order quantifier prefix and a
quantifier-free relational formula of first-order logic with equality. These classes
are characterized by restrictions on the second-order and first-order prefix as
shown in the following table, where the r in the class names points out the
restriction to relational formulas:
Formula class Second-order prefix First-order prefix
∀r-formulas empty ∀x1 . . . ∀xn
∃∀r-formulas empty ∃x1 . . . ∃xm ∀y1 . . . ∀yn
∃∀r-formulas ∃p1 . . . ∃pm ∀x1 . . . ∀xn
The class ∀r-formulas is the class of universal relational first-order formulas. The
class ∃∀r-formulas is also known as Bernays-Schönfinkel-Ramsey class.
If F, G are formulas, we write F |= G for F entails G; |= F for F is valid ;
and F ≡ G for F is equivalent to G, that is, F |= G and G |= F . If I is an
interpretation and F is a formula, we write I |= F for I is a model of F .
3 Underlying Toolkit
We now specify the technical background underlying the proofs of the main re-
sults. It is essentially a small toolkit of formula-based concepts and construction
techniques used in automated deduction.
3.1 Second-Order Quantifier Elimination
The objective of second-order quantifier elimination is to compute for a given
second-order formula a first-order resultant, which is characterized as follows:
86
Definition 1 (Resultant). A resultant of a second-order formula F is a for-
mula F 0 such that
1. F 0 is first-order,
2. F 0 ≡ F ,
3. V(F 0 ) ⊆ V(F ).
It follows immediately from condition 2. of Def. 1 that all resultants of a given
formula are equivalent. Hence, we also speak of the resultant of a second-order
formula. From conditions 1. and 3. it follows that none of the quantified predi-
cates possibly occurring in F do occur in F 0 . They are, so-to-speak, “forgotten”
in F 0 .
The following proposition shows an equivalence of a second-order formula
with a certain shape and a first-order formula, due to Ackermann [1]. It can be
applied to compute the resultant of a second-order formula that matches its left
side by rewriting with the right side. The DLS algorithm [7,5] for second-order
quantifier elimination surrounds such rewriting steps with pre- and postprocess-
ing operations.
Proposition 2 (Ackermann’s Lemma [1]). Let p be an n-ary predicate, let G
and H be first-order formulas such that p does not occur in G, let x = x1 , . . . , xn
be a sequence of distinct individual symbols that do not occur bound in G and
do not occur in H. Let H[p 7→ G] stand for H with each occurrence of atoms
p(t1 , . . . , tn ) whose predicate is p replaced by G{x1 7→ t1 , . . . , xn 7→ tn }, that is,
G under the substitution that maps xi to ti , for i ∈ {1, . . . , n}. If p does not
occur with positive polarity in H, then
∃p (∀x(px ∨ G) ∧ H) ≡ H[p 7→ G].
Ackermann’s lemma also holds in a dual variant: If p does not occur with negative
polarity in H, then ∃p (∀x(¬px ∨ G) ∧ H) ≡ H[p 7→ G]. For quantifier-free
formulas (also with function symbols) with an existential second-order prefix, it
is always possible to compute a resultant on the basis of Ackermann’s lemma,
as demonstrated with the following algorithm:
Algorithm 3 (Second-Order Quantifier Elimination upon Quantifier-
Free Formulas).
Input: An formula that consists of a prefix of existential predicate quantifiers
followed by a quantifier-free formula of first-order logic with equality.
Method: Starting with the input formula, repeatedly eliminate the innermost
existential second-order quantifier with the following method: Given is a formula
∃p F , where F is quantifier-free. Convert F to disjunctive normal form K1 ∨ . . . ∨
Kn , where each disjunct is a conjunction of literals. Propagate the second-order
quantifier inwards to obtain the formula ∃p K1 ∨ . . . ∨ ∃p Kn , which is equivalent
to ∃p F . Eliminate ∃p in each disjunct individually: Arrange the disjunct in the
form
∃p (pt1 ∧ . . . ∧ ptk ∧ ¬pu1 ∧ . . . ∧ ¬pul ) ∧ K 0 ,
where p does not occur in K 0 and k, l ≥ 0. Rewrite this formula to the equivalent
formula
∃p (∀x (px ∨ x 6= t1 ∧ . . . ∧ x 6= tk ) ∧ ¬pu1 ∧ . . . ∧ ¬pul ) ∧ K 0 ,
87
where x is a sequence of fresh individual symbols whose length is the arity of p.
Apply Ackermann’s Lemma (Prop. 2) to rewrite this formula to its resultant
(u1 6= t1 ∧ . . . ∧ u1 6= tk ) ∧ . . . ∧ (ul 6= t1 ∧ . . . ∧ ul 6= tk ) ∧ K 0 .
Combine these individual resultants disjunctively to obtain a resultant of ∃p F .
Output: A resultant of the input formula.
Algorithm 3 also justifies the computation of resultants of formulas of the
form
∃p1 . . . ∃pm ∃x1 . . . ∃xn F, (i)
where F is quantifier-free. These are the formulas of the first of the three classes
with existential second-order quantification explicitly considered in [21] as men-
tioned in the introduction, now generalized by allowing function symbols. For-
mula (i) is equivalent to ∃x1 . . . ∃xn ∃p1 . . . ∃pn F , obtained by switching the first-
and second-order quantifier prefix. If F 0 is a resultant of ∃p1 . . . ∃pn F , obtained
for example with Algorithm 3, then ∃x1 . . . ∃xn F 0 is a resultant of (i).
Algorithm 3 can be considered as a specialized variant of DLS [7], with a
simpler pre- and postprocessing that just suffices to handle predicate quantifi-
cation applied to quantifier-free first-order formulas. In [6] a similar technique
is used and some refinements are shown. In [9] a further variant of DLS is in-
troduced that computes resultants of quantifier-free formulas under existential
second-order quantification, however constrained such that all occurrences of a
quantified predicate are replaced by the same “witness” formula, whereas in Al-
gorithm 3 it is allowed that in the processing of each disjunct Ki a different
formula (x 6= t1 ∧ . . . ∧ x 6= tk ) is used to replace p. In fact, the algorithm from
[9] can be considered as based on Algorithm 3, but followed by a second step
in which the different replacement formulas in each disjunct are combined to a
single witness that is suitable as replacement in all disjuncts. The necessity of
only a single replacement formula is imposed by the restricted form of second-
order quantifier elimination through finding a witnesses that is considered in [9],
which can be also viewed as finding a Boolean unifier and as finding a particular
solution of the Boolean solution problem [24].
3.2 Domain Closure Axioms and Restricted Prefixes
The domain closure axiom, which restricts the universe of discourse to just those
individuals denoted by constants in the given formula, emerged as a tool for
the logical modeling of relational databases [16]. Following [8], we consider a
generalized variant that in addition permits a fixed number of further objects.
Definition 4 (Domain Closure Axiom). Let C = {c1 , . . . , cn } be a nonempty
set of individual symbols, let k ∈ N0 , and assume that x, y1 , . . . , yk are individual
symbols that are not in C. Define
DCAkC def
= ∃y1 . . . ∃yk ∀x (x = y1 ∨ . . . ∨ x = yk ∨ x = c1 ∨ . . . ∨ x = cn ).
It is possible, to specify domain closure axiom with a formula as parameter
whose free individual symbols are taken as considered set C. However, consid-
ered as a function of formulas, domain closure axiom is then not “semantic”,
88
that is, it might have semantically different values for semantically equivalent
argument formulas, which, despite being equivalent, might have different sets of
free individual symbols. To avoid “non-semantic” functions of formulas, we use
here a version of domain closure axiom that is explicitly parameterized with a
set C of individual symbols.
Domain closure axioms play a role in general domain circumscription [8]. As
shown with [8, Thm. 6.1], the domain circumscription of an ∀r-formula F such
that VC (F ) 6= ∅ is equivalent to DCA0C ∧ F , where C = VC (F ).
The remaining propositions in this section show properties of first-order for-
mulas with restricted quantifier prefixes conjoined with domain closure axioms.
Roughly, the intuition there is that for these formulas the addition of domain
closure axioms does not essentially alter the semantics, but allows to eliminate
first-order quantification by ground expansion with respect to the finite set of
symbols presupposed in the domain closure axioms. The underlying core prop-
erty is that from a model of an ∃∀r-formula a further model can be derived that
in addition also satisfies the domain closure axiom with respect to length of the
existential quantifier prefix and the free individual symbols:
Proposition 5 (Domain Closure Extension for ∃∀r-Formulas). Let F be
an ∃∀r-formula and let I be an interpretation such that I |= F . Then for all
non-empty sets C ⊇ VC (F ) of individual symbols and for all natural numbers k
larger than or equal to the length of the existential quantifier prefix of F there
exists an interpretation I0 such that
1. I0 |= DCAkC ∧ F.
2. For all ground atoms A constructed from predicates in F and individual
symbols in C it holds that I |= A iff I0 |= A.
This proposition is not hard to prove by considering the submodel of I obtained
by restricting the domain to the union of the ≤ k individuals whose existence
is presupposed by the existential quantifier prefix of F and the set of the values
of the members of VC (F ) in I. From this proposition it follows that if an ∃∀r-
formula conjoined with a suitable domain closure axiom entails an ∀∃r-formula,
then also the ∃∀r-formula alone entails that formula:
Proposition 6 (Redundancy of Domain Closure for ∃∀r-∀∃r Entailments).
Let F be an ∃∀r-formula and let G be an ∀∃r-formula, let C ⊇ VC (F ) ∪ VC (G)
be a non-empty set of individual symbols, and let k be a natural number that is
larger than or equal to the sum of the length of the existential quantifier prefix
of F and the length of universal quantifier prefix of G. It then holds that
if DCAkC ∧ F |= G, then F |= G.
Proof. Assume the left side of the proposition, that is, DCAkC ∧ F |= G. Assume
further that the right side does not hold. Then there exists an interpretation I
such that I |= F ∧ ¬G. Observe that F ∧ ¬G is equivalent to an ∃∀r-formula
with k existential quantifiers. Thus, by Prop. 5 there exists an interpretation I0
such that I0 |= DCAkC ∧ F ∧ ¬G. With the assumption DCAkC ∧ F |= G it then
follows that I0 |= G ∧ ¬G, which contradicts with I0 being an interpretation. t u
89
From this proposition it follows that the semantics of ∀r-formulas F is preserved
under conjunction with a suitable domain closure axiom:
Proposition 7 (Semanticity of Domain Closure for ∀r-formulas). Let
F, G be ∀r-formulas, let C ⊇ VC (F ) ∪ VC (G) C be a non-empty set of individ-
ual symbols, and let k be a natural number that is larger than or equal to the
maximum of the quantifier prefix lengths of F and G. It then holds that
if DCAkC ∧ F ≡ DCAkC ∧ G, then F ≡ G.
Proof. Follows from Prop. 6. t
u
3.3 Resultants of ∃∀r-formulas are Universal
Based on a strengthening of Craig’s interpolation theorem it can be shown that
whenever an ∃∀r-formula has a resultant, then the resultant is equivalent to an
∀r-formula, and, moreover, that there is an effective method to compute for any
given resultant of an ∃∀r-formula such an equivalent ∀r-formula. Before we state
this as a proposition, we show the underlying interpolation property:
Proposition 8 (Interpolants with ∃∀r-Formula on the Left). Let F be an
∃∀r-formula and let G be a first-order formula such that F |= G. Then there is
an effective method to compute from given F and G a formula H such that
1. H is an ∀r-formula.
2. F |= H |= G.
3. VP (H) ⊆ VP (F ) ∩ VP (G).
4. VC (H) ⊆ VC (F ).
Proof. Let G0 be G conjoined with tautologies such that VC (G0 ) ⊇ VC (F ),
whereas VP (G0 ) = VP (G) and G0 ≡ G. Let F 0 be the ∀r-formula obtained
from F by renaming the quantified predicates with fresh symbols and dropping
the second-order prefix. Compute H as Craig interpolant of F 0 and G0 with the
tableau-based interpolant construction method described in [19] and [11]. Con-
ditions 2.–4. of the proposition follow from the properties of Craig interpolants:
F 0 |= H |= G0 implies F |= H |= G; from V(H) ⊆ V(F 0 ) ∩ V(G0 ) it follows, since
VP (F 0 ) = VP (F ) and VP (G0 ) = VP (G), that VP (H) ⊆ VP (F ) ∩ VP (G), and,
since VC (F 0 ) = VC (F ) ⊆ VC (G0 ), that VC (H) ⊆ VC (F ). Condition 1. follows
from particular features of the interpolant construction method of [19,11], where
an existential quantifier in the interpolant would not be introduced if the left
formula of the interpolation is universal and all individual symbols that occur
free in the left formula also occur free in the right formula. t
u
Proposition 9 (Resultants of ∃∀r-Formulas are Universal). A resultant of
an ∃∀r formula F is equivalent to an ∀r-formula. Moreover, there is an effective
method to compute from F and any given resultant a resultant that is an ∀r-
formula.
Proof. Assume that G is an arbitrary resultant of F . Thus F ≡ G. Let H be
computed from F and G according to Prop. 8. It is easy to verify that H an
∀r-formula and is a resultant of F . t
u
90
4 Approximating Resultants of ∃∀r-formulas
The main results of the paper are now shown: For a given ∃∀r-formula F a
sequence {G0 , G1 , G2 , . . .} of universal first-order formulas that have (not neces-
sarily strictly) increasing strength and are all entailed by F can be constructed.
Any first-order consequence of F is a consequence of some Gi . Formula F has
a resultant if and only if it is equivalent to some Gi . However, only methods
are provided to detect that the consequences of a given Gi do not include all
first-order consequences of F , or, respectively, Gi is not equivalent to F . This
leads to co-recursive enumerability of the first-order formulas that are equivalent
to F or entail F , directly in case F has a resultant, or with respect the first-
order consequences of F in case it has no resultant. Theorem 11 below makes
this precise and shows further properties of the formulas Gi , some of which are
underlying the proofs of the mentioned results. First the theorem is stated and
proven formally, then the individual claimed properties are described informally.
The following definition is used in the statement of Theorem 11. It specifies
notions of entailment and equivalence of second-order formulas modulo the sets
of entailed first-order formulas.
Definition 10 (Entailment and Equivalence Modulo First-Order Con-
sequences). For second-order formulas F, G define
(i) F |=FO G if and only if for all first-order formulas H it holds that if G |= H,
then F |= H.
(ii) F ≡FO G if and only if F |=FO G and G |=FO F .
These notions are helpful to express properties of second-order formulas that
possibly have no resultant. Their meaning is identical to the standard notions
of entailment and equivalence, respectively, if no such second-order formulas
are involved: If G is a first-order formula or a second-order formula that has
a resultant, then, also in the case where F is a second-order formula, it holds
that F |=FO G if and only if F |= G. If each of F and G is first-order or has a
resultant, then F ≡FO G if and only if F ≡ G.
Theorem 11 (Approximating Resultants of ∃∀r-formulas). Let F be an
∃∀r-formula and let C ⊇ VC (F ) be a nonempty set of individual constants. Then
there exist ∀r-formulas G0 , G1 , G2 , . . . such that
(a) The set {G0 , G1 , G2 , . . .} is recursive.
(b) G0 =| G1 =| G2 =| . . . =| F.
(c) For all i ∈ N0 it holds that DCAiC ∧ Gi ≡ DCAiC ∧ F.
(d) For all i, j ∈ N0 such that i ≤ j it holds that DCAiC ∧ Gi |= DCAjC ∧ Gj .
(e) For all i ∈ N0 it holds that F has a resultant that is an ∀r-formula with
quantifier prefix length i if and only if Gi ≡ F.
(f ) F has a resultant if and only if there exists a k ∈ N0 such that Gk ≡ F.
(g) For all i ∈ N0 and ∀r-formulas H with quantifier prefix length i it holds that
F |= H if and only if Gi |= H.
(h) There is an effective method to compute from F and a given first-order
formula H such that F |= H a number k ∈ N0 such that Gk |= H.
91
(i) The set {i | i ∈ N0 and Gi ≡FO F } is co-recursively enumerable.
(j) The set {i | i ∈ N and Hi |=FO F }, where {H1 , H2 , H3 , . . .} is the set of all
∃∀r-formulas, is co-recursively enumerable (under assumption of a countable
vocabulary).
Proof. Let
F = ∃p1 . . . ∃pn ∀x1 . . . ∀xm F 0 ,
where F 0 is quantifier-free. Let F 0 [a1 , . . . , am ] denote F 0 with xi replaced by
some individual symbol ai , for all i ∈ {1, . . . , m}. Let U be a set {u1 , u2 , u3 , . . .}
of individual symbols that are not in C and let Ui denote {u1 , . . . , ui }. For i ∈ N0
construct Gi as
= ∀u1 . . . ∀ui G0i ,
Gi def
where G0i is the resultant, computed by Algorithm 3, of the following formula:
^
∃p1 . . . ∃pn F 0 [a1 , . . . , am ].
a1 ,...,am ∈C∪Ui
The following semantic property of Gi , for all i ∈ N0 , then immediately follows
from the construction of Gi :
V 0
(∗) Gi ≡ ∀u1 . . . ∀ui ∃p1 . . . ∃pn a1 ,...,am ∈C∪Ui F [a1 , . . . , am ].
(a) Follows from the construction of the formulas Gi : For any given first-order
formula whose universal first-order quantifier prefix has length i ≥ 0 it can be
decided whether it is a member of {G0 , G1 , G1 , . . .} by comparing it syntactically
with Gi .
(b) Let i, j ∈ N0 that i ≤ j. Since then Uj ⊇ Ui it follows that
^ ^
F 0 [a1 , . . . , am ] |= F 0 [a1 , . . . , am ].
a1 ,...,am ∈C∪Uj a1 ,...,am ∈C∪Ui
With (∗) this implies Gj |= Gi . To conclude the proof of (b) we show that for
an arbitrary number i ∈ N0 it holds that F |= Gi . This can be proven in the
following steps, where the last step, the contraction into Gi , is justified by (∗):
F
≡ ∃p1 . . . ∃pn ∀x1 . . . ∀xmVF0
|= ∃p1 . . . ∃pn ∀u1 . . . ∀ui a1 ,...,am ∈C∪Ui F 0 [a1 , . . . , am ]
V
|= ∀u1 . . . ∀ui ∃p1 . . . ∃pn a1 ,...,am ∈C∪Ui F 0 [a1 , . . . , am ]
≡ Gi .
(c) The right-to-left direction follows immediately from (b). The left-to-right
direction can be shown in the following steps, where the expansion of Gi at the
first step is justified by (∗):
92
DCAiC ∧ Gi
V
≡ DCAiC ∧ ∀u1 . . . ∀ui ∃p1 . . . ∃pn a1 ,...,am ∈C∪Ui F 0 [a1 , . . . , am ]
≡ ∃u1 . . . ∃ui DCA0C∪Ui ∧ V
∀u1 . . . ∀ui ∃p1 . . . ∃pn a1 ,...,am ∈C∪Ui F 0 [a1 , . . . , am ]
V
|= ∃u1 . . . ∃ui (DCA0C∪Ui ∧ ∃p1 . . . ∃pn a1 ,...,am ∈C∪Ui F 0 [a1 , . . . , am ])
≡ ∃u1 . . . ∃ui DCA0C∪Ui ∧ ∃p1 . . . ∃pn ∀x1 . . . ∀xm F 0
≡ DCAiC ∧ ∃p1 . . . ∃pn ∀x1 . . . ∀xm F 0
≡ DCAiC ∧ F.
(d) From i ≤ j it follows that DCAiC |= DCAjC . By (c) we can conclude
DCAiC ∧ Gi ≡ DCAiC ∧ F |= DCAjC ∧ F ≡ DCAjC ∧ Gj .
(e) The right-to-left direction follows immediately from the construction of
Gi : If Gi ≡ F , then Gi clearly is a resultant of F that is an ∀r-formula with
quantifier prefix length i. The left-to-right direction can be show as follows:
Assume that there exists an ∀r-formula H with quantifier prefix length i that is
a resultant of F . Since H ≡ F it follows from (c) that
DCAiC ∧ Gi ≡ DCAiC ∧ H.
This equivalence matches the precondition of Prop. 7 that lets us deduce Gi ≡ H,
implying Gi ≡ F .
(f ) Follows from (e) and Prop. 9.
(g) The right-to-left direction follows immediately from (b). The left-to-right
direction can be shown in the following steps, where the last two equivalences
follow from (c) and Prop. 6, respectively:
F |= H implies DCAiC ∧ F |= H iff DCAiC ∧ Gi |= H iff Gi |= H.
(h) By Prop. 8, we can compute from F and H an ∀r-formula K such that
F |= K |= H. Let k be the length of the quantifier prefix of K. From (g) it
follows that Gk |= K, hence Gk |= H.
(i) The following algorithm halts for a given i ∈ N0 if and only if Gi 6≡FO F :
Let j be an integer variable that satisfies the invariant j > i and is initialized
to i + 1. Proceed in a loop: Test whether Gi 6|= Gj , that is, whether Gi ∧ ¬Gj
is satisfiable. Since Gi and Gj are ∀r-formulas, Gi ∧ ¬Gj is an ∃∀r-formula, and
thus decidable. If the test succeeds, then halt, else increment j by 1 and re-enter
the loop.
That the algorithm indeed halts if and only if Gi 6≡FO F can be shown as
follows: By (b) it holds that F |= Gi . Hence Gi 6≡FO F if and only Gi 6|=FO F .
Consider the case Gi 6|=FO F and first the subcase where there exists a natural
number j > i such that Gi 6|= Gj . Then the satisfiability test in the algorithm
eventually succeeds and the algorithm halts. Now consider the alternate subcase
where no such number j exists. From (b) it then follows that for all l ∈ N0 it holds
that Gi |= Gl . With (h) we can conclude that it holds for all first-order formula
H that if F |= H, then Gi |= H. Hence Gi |=FO F , contradicting the assumption
Gi 6|=FO F made for that case, and thus yielding the alternate subcase impossible.
93
Now consider the case Gi |=FO F . From the definition of |=FO it follows that for
all j ≥ 0 it holds that if F |= Gj , then Gi |= Gj . With (b) it follows that for
all j ≥ 0 it holds that Gi |= Gj , which implies that the satisfiability test in the
algorithm never succeeds and the algorithm thus loops forever.
(j) The following algorithm halts for a given ∃∀r-formula H if and only if
H 6|=FO F : Let j be an integer variable that is initialized to 0. Proceed in a loop:
Test whether H 6|= Gj , that is, whether H ∧ ¬Gj is satisfiable. Since H is an ∃∀r-
formula and Gi is an ∀r-formula, H ∧ ¬Gj is an ∃∀r-formula, and thus decidable.
If the test succeeds, then halt, else increment j by 1 and re-enter the loop.
That the algorithm indeed halts if and only if H 6|=FO F follows since H 6|=FO F
holds if and only if there exists a j ∈ N0 such that H 6|= Gj , or, equivalently,
H |=FO F if and only if for all j ∈ N0 it holds that H |= Gj . The left-to-right direc-
tion of this equivalence can be proven as follow: Assume the left side H |=FO F .
By expanding |=FO this can be expressed as: For all first-order formulas K it
holds that if F |= K, then H |= K. Hence, for all j ∈ N0 it holds that if F |= Gj ,
then H |= Gj . With (b) it follows that for all j ∈ N0 it holds that H |= Gj ,
that is, the right side. The right-to-left direction of the equivalence to show can
be proven as follows: From (h) it follows that for all first-order formulas K it
holds that if F |= K, then there exists a k ∈ N0 such that Gk |= K. Hence, if for
all i ∈ N0 it holds that H |= Gj , then for all first-order formulas K such that
F |= K it holds that H |= K. By contracting into |=FO , the latter statement can
be expressed as: If for all j ∈ N0 it holds that H |= Gj , then for H |=FO F , that
is, the right-to-left direction of the equivalence to show. t
u
The formulas Gi whose existence is claimed by Theorem 11 are constructed
from F and i as follows: The first-order quantifiers in F , which are universal,
are eliminated by expansion with respect to the members of C and i additional
individual symbols u1 , . . . , ui . Then a resultant of the obtained formula, that is,
of the second-order quantifier prefix of F applied to the quantifier-free expansion,
is computed. The formula Gi is then obtained by prefixing that resultant, which
is quantifier-free, with existential first-order quantifiers upon u1 , . . . , ui .
By property (b), with increasing i the formulas Gi get (not necessarily strictly)
stronger, and all the formulas Gi are entailed by F .
Property (c) holds invariantly for all i ∈ N0 : Formula Gi “under domain
closure with i existential individuals” (that is, conjoined with DCAiC ) is equivalent
to F under domain closure with the same number of existential individuals. This
property is used in the proofs of (d), (e), and (g).
Property (d), which follows from (c), shows that with increasing i the for-
mulas Gi under domain closure with i existential objects get (not necessarily
strictly) weaker, conversely to the formulas Gi themselves, as shown with (b).
Properties (e) and (f ) show necessary and sufficient conditions for the ex-
istence of a resultant of F , and in case of existence give a resultant. The first
of these, (e), states that F has a resultant that is a universal relational formula
with quantifier prefix length i if and only if Gi is equivalent to F . This property
follows from (c) and Prop. 7. With Prop. 9 it leads to (f ), which states that
F has a resultant if and only if it is equivalent to Gk for some k ∈ N0 . The
94
right-to-left directions of the respective equivalences Gi ≡ F and Gk ≡ F are
immediate from (b), such that the existence of a resultant can be also charac-
terized with just the entailments Gi |= F and Gk |= F , respectively, instead.
These entailments have F on their right side, a second-order formula, such that,
differently from first-order logic, there is in general no algorithm that halts if
and only if such an entailment holds.
Property (g) shows that F and Gi have the same ∀r-formulas with quantifier
prefix length i as consequences. This follows from (c) and Prop. 6. It is used
together with the strengthened Craig interpolation property Prop. 8 to prove (h),
by which any first-order consequence of F is a consequence of some Gk , and,
moreover, such an index k can be effectively computed from F and the given
consequence. Property (h) is applied to prove (i) and (j).
Properties (i) and (j) show certain settings where co-recursive enumerability
with respect to equivalence and entailment, respectively, of the second-order
formula F can be established. Property (i) states that the set of (the index
numbers i of) the formulas Gi that are different from F with respect to their
first-order consequences is recursively enumerable. This means that there is an
algorithm that halts for given i if and only if Gi is not a formula with the
same first-order consequences as F . If F has a resultant, this is equivalent to
the statement that Gi is not a resultant of F . Property (i) is proven by giving
such an algorithm and showing its correctness with referring to (b) and (h).
By (b) the negated equivalence Gi 6≡FO F can also be expressed as the negated
entailment Gi 6|=FO F , which in the case where F has a resultant is equivalent
to Gi 6|= F . From the perspective of trying to find a resultant of F or, more
generally, a formula with the same first-order consequences as F , the property (i)
only justifies a method to exclude failing candidate formulas Gi .
Property (j) states that the set of (the code numbers in some arithmetization
of syntax of) the first-order formulas that do not entail F with respect to its
first-order consequences is recursively enumerable. This means that there is an
algorithm that halts for a given first-order formula H and only if H 6|=FO F .
Like (i), this property is proven by giving such an algorithm and showing its
correctness with referring to (b) and (h). The property justifies a method that
detects for a given first-order formula H in the case where F has a resultant that
F is not a consequence of H, and in the case where F has no resultant that not
all first-order consequences of F are included in the consequences of H.
5 Discussion and Open Issues
In this section, Craig’s work [6] on recursive bases is briefly compared, attempts
are made to place the results of Theorem 11 in the context of applications of
second-order quantifier elimination, open issues are shown, and potential direc-
tions for further research are indicated.
Comparison to Craig’s Construction of Recursive Bases. The setting
in [6] is more general and comprehensive: First-order formulas under existential
second-order quantification are considered without assuming syntactic restric-
tions and also the case without equality is considered. Our syntactic restriction
allows an apparently simpler construction of the approximation formulas Gi for
95
which monotonicity (i.e., G0 =| G1 =| G2 =| . . .) directly follows. The restriction
also allows to derive further properties of the approximation formulas: They are
universal and the length of their quantifier prefix is related to that of entailed
universal first-order consequences of the second-order formula. Decidability of
specific entailment problems, which is implied by the syntactic restrictions, leads
to co-recursive enumerability of certain sets.
Our construction of an approximation formula Gi for a second-order formula
F = ∃p F 0 where F 0 is first-order involves the construction of a first-order prefix
Qi and of an intermediate quantifier-free formula Fi0 such that F = ∃p F 0 |=
∃pQFi0 |= Q∃pFi0 ≡ Gi . The setting in [6] is the same, except that the first
entailment is replaced by an equivalence, that is, it holds that ∃p F 0 ≡ ∃pQFi0 .
Actually, the techniques in [6] seem even to preserve F 0 ≡ QFi0 . Of course, more
weakly constrained transformations, in our case mainly justified through the use
of domain closure axioms, are favorable. However, it remains to be investigated in
how far the weaker constraints are made possible through the restricted formula
class and whether there are associated complexity properties.
Entailments Involving Existential Second-Order Formulas. Property (j)
of Theorem 11 can be considered in the context of mechanical verification and
falsification (that is, existence of an algorithm that terminates in case a statement
does hold or does not hold, respectively) of entailments of the forms F |= H and
H |= F , where F is a second-order formula with an existential second-order
quantifier prefix applied to a first-order formula and H is a first-order formula.
An application of the first form F |= H is to verify that a first-order formula
A is semantically independent from predicates p1 . . . , pn , which can be expressed
as ∃p1 . . . ∃pn A |= A. The first form F |= H is straightforwardly accessible to
verification: The set {i | i ∈ N and F |= Hi }, where {H1 , H2 , H3 , . . .} is the set
of all first-order formulas, is recursively enumerable, which follows from recursive
enumerability of the set of (the code numbers of) the valid first-order formulas.
The entailment F |= Hi is equivalent to the first-order entailment F 0 |= Hi ,
where F 0 is obtained from F by dropping the second-order prefix and renaming
the quantified predicates with fresh symbols. The entailment F 0 |= Hi can then
be expressed as validity of F 0 → Hi . Moreover, if F and Hi are restricted such
that F 0 ∧ ¬Hi belong to a decidable formula class, then {i | i ∈ N and F |= Hi }
is recursive, allowing then also to falsify entailments of the form F |= H.
An application of the second form H |= F is expressing for first-order for-
mulas A and B that A ∧ B is a conservative extension of A as the entailment
A |= ∃p1 . . . ∃pn (A ∧ B), where p1 , . . . , pn are the predicates that occur in B but
not in A. Justified by property (j) of Theorem 11, the second form H |= F (if
restricted to ∃∀r-formulas H and ∃∀-formulas F ) can be mechanically falsified.
To sum up, entailments of the form F |= H can always be verified and
for formula classes that lead to decidable formulas F ∧ ¬H also be falsified.
Property (j) of Theorem 11 extends this, by establishing that also entailments
of the form H |= F can be falsified, for certain formula classes.
Approximate Resultants with Respect to Quantifier Prefix Length.
By property (g) of Theorem 11, the ∃∀r-formula F and the formulas Gi con-
structed from it have the same ∀r-formulas with quantifier prefix length i as
96
consequences. In a sense, the formulas Gi can be considered as capturing the
first-order semantics of F “up to quantifier prefix length i”. This suggests to
consider Gi as resultant of a generalized form of elimination where not just the
existentially quantified predicates are “forgotten”, but also the part of the for-
mula’s meaning that would be only expressible with quantifier prefix length > i.
Exploring this idea is an open issue.
Showing Non-Recursiveness. Properties (i) and (j) of Theorem 11 show
co-recursive enumerability of certain sets related to second-order quantifier elim-
ination. It remains to consider the question whether this is the strongest recur-
siveness property that can be asserted about these sets, that is, to show whether
they are actually not recursive. It is expected that this holds because the formula
∃f (x ∧ ¬f y ∧ ∀u∀v (¬f u ∨ f v ∨ ¬nuv) used in [1] to show non-existence of a
resultant is actually an ∃∀r-formula.
Potential Approaches for Strengthening the Co-Recursive Enumer-
ability. Of course, it would be of interest, not just for practical application,
to strengthen the co-recursive enumerability of finding resultants and verifying
entailments shown with properties (i) and (j) of Theorem 11 to recursiveness,
at least for special cases. So far, this is an open issue. A direction for further in-
vestigation might be trying to determine for certain ∃∀r-formulas the maximally
required quantifier prefix length of the resultant. A further direction could be
ensuring that a semantic fixed point Gk of the sequence G0 , G1 , G2 , . . . subsumes
all Gi with i ≥ k, that is, for all i ≥ k it holds that Gi ≡ Gk . This would follow,
for example, if for all i, j ∈ N0 it holds that if Gi ≡ Gj , then Gi+1 ≡ Gj+1 . A
third direction would be trying to express for all i ≥ k it holds that Gi ≡ Gk in
some algorithmically verifiable way.
Possibly Generalization to Further Formula Classes. Theorem 11 takes
decidability of the Bernays-Schönfinkel-Ramsey class (∃∀r-formulas) as basis to
derive co-recursive enumerability of problems related to computing elimination
resultants of existential second-order quantifiers upon universal relational for-
mulas (∃∀-formulas). This raises the question, whether the techniques applied
there can be generalized to further formula classes.
A straightforward transfer appears to be the computation of resultants of
formulas of the Bernays-Schönfinkel-Ramsey class under existential second-order
quantification, by switching the existential second- and first-order quantifier pre-
fixes and then considering elimination of the inner ∃∀r-formula. However, with
this approach a further source of failure to find resultants sneaks in: There are
∃∃∀r-formulas that have a resultant, but where after the suggested quantifier
switching the obtained inner ∃∀r-formula does not have a resultant. As an ex-
ample, consider a formula ∃p (x = a∨F ) that does not have a resultant. However,
∃p ∃x (x = a ∨ F ) clearly has for arbitrary formulas F the resultant >.
Avoiding Explicit Ground Expansion. The construction of the approxima-
tion formulas Gi described in the proof of Theorem 11 involves ground expansion
of the input formula F . As in instance-based theorem proving, such expansions
are useful as a conceptual construct, but their construction should in practice
usually be avoided as much as possible. With respect to elimination, a poten-
97
tial approach might be the use of quantifier relativizations to compactly express
formulas equivalent to expansions. Possibly the resultant required in the con-
struction of Gi can then be computed by applying the elimination method for
single ground atoms described in [13] to the finite number of atoms upon which
the quantifiers are relativized. Also techniques of [6], where quantified formulas
are duplicated by conjoining copies of them, but without performing instantia-
tion, might be relevant here.
6 Conclusion
We have considered second-order quantifier elimination for a class of relational
formulas characterized by a restriction of the quantifier prefix: existential pred-
icate quantifiers followed by universal individual quantifiers. The main original
motivation was to transfer instance-based techniques from automated theorem
proving to second-order quantifier elimination. The technical result, however,
does not indicate an immediate possibility for such a transfer, but gives some
insight into the elimination problem for this class: The set of elimination resul-
tants of a given formula and the set of formulas entailing the given second-order
formula of that class is co-recursively enumerable. Candidate resultants can be
generated, and there is an algorithm that halts on exactly those candidates that
are not a resultant. Similarly, there is a method to detect that a given first-order
formula does not entail the given second-order formula. By comparing formulas
with respect to their first-order consequences, it is possible to express the respec-
tive theorem statements in a generalized way that applies to given second-order
formulas independently of whether they have a resultant. These results were
proven on the basis of small number of formula-based tools used in automated
deduction. Actually, the results and involved constructions might be seen as a
specialization to a formula class of Craig’s setting of determining recursive bases
for subtheories of first-order formulas. The hope is that some inspiration and
material for further investigation of “eliminability”, that is, existence of a resul-
tant, or, more generally, of a formula that is equivalent with respect to first-order
consequences, is provided.
Acknowledgments. This work was supported by DFG grant WE 5641/1-1.
References
1. Ackermann, W.: Untersuchungen über das Eliminationsproblem der mathemati-
schen Logik. Math. Ann. 110, 390–413 (1935)
2. Baumgartner, P., Thorstensen, E.: Instance based methods – A brief overview. KI
24(1), 35–42 (Apr 2010)
3. Behmann, H.: Beiträge zur Algebra der Logik, insbesondere zum Entschei-
dungsproblem. Math. Ann. 86(3–4), 163–229 (1922)
4. Börger, E., E., Grädel, Gurevich, Y.: The Classical Decision Problem. Springer
(1997)
5. Conradie, W.: On the strength and scope of DLS. J. Applied Non-Classical Logic
16(3–4), 279–296 (2006)
6. Craig, W.: Bases for first-order theories and subtheories. J. Symb. Log. 25(2),
97–142 (1960)
98
7. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited: A
reduction algorithm. J. Autom. Reasoning 18(3), 297–338 (1997)
8. Doherty, P., Łukaszewicz, W., Szałas, A.: General domain circumscription and its
effective reductions. Fundamenta Informaticae 36, 23–55 (1998)
9. Eberhard, S., Hetzl, S., Weller, D.: Boolean unification with predicates. J. Logic
and Computation 27(1), 109–128 (2017)
10. Fermüller, C., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision proce-
dures. In: Robinson, A., Voronkov, A. (eds.) Handb. of Autom. Reasoning, vol. 2,
pp. 1793–1849. Elsevier (2001)
11. Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, 2nd
edn. (1995)
12. Gabbay, D.M., Schmidt, R.A., Szałas, A.: Second-Order Quantifier Elimina-
tion: Foundations, Computational Aspects and Applications. College Publications
(2008)
13. Lin, F., Reiter, R.: Forget It! In: Working Notes, AAAI Fall Symposium on Rele-
vance. pp. 154–159 (1994)
14. Löwenheim, L.: Über Möglichkeiten im Relativkalkül. Math. Ann. 76, 447–470
(1915)
15. Löwenheim, L.: Funktionalgleichungen im Gebietekalkül und Umformungs-
möglichkeiten im Relativkalkül. History of Philosophy and Logic 28, 305–336
(2007), assumed to be written in 1935 [20]
16. Reiter, R.: Deductive quastion-answering on relational databases. In: Gallaire, H.,
Minker, J. (eds.) Logic and Databases, pp. 149–178. Plenum Press, New York
(1978)
17. Schröder, E.: Vorlesungen über die Algebra der Logik, vol. 1. Teubner (1890)
18. Skolem, T.: Untersuchungen über die Axiome des Klassenkalküls und über
Produktations- und Summationsprobleme welche gewisse Klassen von Aussagen
betreffen. Videnskapsselskapets Skrifter I. Mat.-Nat. Klasse(3) (1919)
19. Smullyan, R.M.: First-Order Logic. Springer, New York (1968), also republished
with corrections by Dover publications, New York, 1995
20. Thiel, C.: A short introduction to Löwenheim’s life and work and to a hitherto
unknown paper. History of Philosophy and Logic 28, 289–302 (2007)
21. Van Benthem, J., Doets, K.: Higher-order logic. In: Handbook of Philosophical
Logic, vol. 1, pp. 189–243. Springer, second edn. (2001)
22. Wernhard, C.: Heinrich Behmann’s contributions to second-order quantifier elimi-
nation. Tech. Rep. KRR 15–05, TU Dresden (2015)
23. Wernhard, C.: Second-order quantifier elimination on relational monadic formulas
– A basic method and some less expected applications. In: TABLEAUX 2015.
LNCS (LNAI), vol. 9323, pp. 249–265. Springer (2015)
24. Wernhard, C.: The Boolean solution problem from the perspective of predicate
logic. In: FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 333–350 (2017)