arXiv:1706.08329v3 [cs.LO] 18 Dec 2017

Faculty of Computer Science

Institute of Artificial Intelligence

Knowledge Representation and Reasoning

The Boolean Solution Problem
from the Perspective of Predicate Logic
– Extended Version –

Christoph Wernhard

KRR Report 17-01

Mail to
Technische Universität Dresden
01062 Dresden

Office
Room 2006
Nöthnitzer Straße 46
01187 Dresden

Internet
http://www.wv.inf.tu-dresden.de

The Boolean Solution Problem
from the Perspective of Predicate Logic
– Extended Version –
Christoph Wernhard
Technische Universität Dresden

Abstract. Finding solution values for unknowns in Boolean equations
was a principal reasoning mode in the Algebra of Logic of the 19th century. Schröder investigated it as Auflösungsproblem (solution problem). It
is closely related to the modern notion of Boolean unification. Today it is
commonly presented in an algebraic setting, but seems potentially useful
also in knowledge representation based on predicate logic. We show that
it can be modeled on the basis of first-order logic extended by secondorder quantification. A wealth of classical results transfers, foundations
for algorithms unfold, and connections with second-order quantifier elimination and Craig interpolation show up. Although for first-order inputs
the set of solutions is recursively enumerable, the development of constructive methods remains a challenge. We identify some cases that allow
constructions, most of them based on Craig interpolation, and show a
method to take vocabulary restrictions on solution components into account.

Revision: December 18, 2017

2

TABLE OF CONTENTS

Table of Contents
1

Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3

2

Notation and Preliminaries . . . . . . . . . . . . . . . . . . . . . . . .

4

2.1
2.2

Notational Conventions . . . . . . . . . . . . . . . . . . . . . . .
Substitution with Terms and Formulas . . . . . . . . . . . . . . .

4
5

The Solution Problem from Different Angles . . . . . . . . . . . . . . .

6

3.1
3.2
3.3
3.4

.
.
.
.

6
8
8
9

The Method of Successive Eliminations – Abstracted . . . . . . . . . .

10

3

4

4.1
4.2
4.3
4.4

Basic Formal Modeling . . . . . . . . . . . . . .
View as Unification . . . . . . . . . . . . . . . .
View as Construction of Elimination Witnesses
View as Related to Definientia and Interpolants

.
.
.
.

.
.
.
.

.
.
.
.

Reducing n-ary to 1-ary Solution Problems . . . . .
Solving on the Basis of Second-Order Formulas . . .
Solving with the Method of Successive Eliminations
Solving by Inside-Out Witness Construction . . . . .

.
.
.
.

5.1
5.2
5.3

Conditions for the Existence of Solutions . . . . . . . . . . . . . .
Characterization of SOL-Witnessed in Terms of ELIM-Witness .
The Elimination Result as Precondition of Solution Existence . .

15
17
17

Reproductive Solutions as Most General Solutions . . . . . . . . . . .

18

6.1
6.2
6.3
6.4

.
.
.
.

19
23
26
28

Approaching Constructive Solution Techniques . . . . . . . . . . . . .

29

7.1
7.2
7.3
7.4

Background: Craig Interpolation, Definability and Independence
Cases Related to Definability and Interpolation . . . . . . . . . .
The EHW-Combination of ELIM-Witnesses for Disjuncts . . . .
Relational Monadic Formulas and Relaxed Substitutibility . . . .

30
31
32
34

Solutions in Restricted Vocabularies . . . . . . . . . . . . . . . . . . .

35

8.1
8.2
8.3

An Example: Synthesizing Definitional Equivalence . . . . . . . .
Modeling with Two Consecutive Solution Problems . . . . . . . .
Expressing a Vocabulary Restriction on all Unknowns . . . . . .

35
35
36

A Herbrand View on the Solution Problem . . . . . . . . . . . . . . .

36

10 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

37

References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

39

7

8

9

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

15

.
.
.
.

.
.
.
.

.
.
.
.

Existence of Solutions . . . . . . . . . . . . . . . . . . . . . . . . . . .

Parametric, General and Reproductive Solutions
The Rigorous Solution . . . . . . . . . . . . . . .
Schröder’s Reproductive Interpolant . . . . . . .
From Unary to n-ary Reproductive Solutions . .

.
.
.
.

.
.
.
.

10
12
13
14

6

.
.
.
.

.
.
.
.

.
.
.
.

5

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

Introduction

1

3

Introduction

Finding solution values for unknowns in Boolean equations was a principal reasoning mode in the Algebra of Logic of the 19th century. Schröder [34] investigated it as Auflösungsproblem (solution problem). It is closely related to the
modern notion of Boolean unification. For a given formula that contains unknowns formulas are sought such that after substituting the unknowns with
them the given formula becomes valid or, dually, unsatisfiable. Of interest are
also most general solutions, condensed representations of all solution substitutions. A central technique there is the method of successive eliminations, which
traces back to Boole. Schröder investigated reproductive solutions as most general solutions, anticipating the concept of most general unifier. A comprehensive
modern formalization based on this material, along with historic remarks, is
presented by Rudeanu [30] in the framework of Boolean algebra. In automated
reasoning variants of these techniques have been considered mainly in the late
80s and early 90s with the motivation to enrich Prolog and constraint processing
by Boolean unification with respect to propositional formulas handled as terms
[26,9,27,28,21,22]. An early implementation based on [30] has been also described
in [37]. An implementation with BDDs of the algorithm from [9] is reported in
[10]. The ΠP
2 -completeness of Boolean unification with constants was proven
only later in [21,22] and seemingly independently in [2]. Schröder’s results were
developed further by Löwenheim [24,25]. A generalization of Boole’s method beyond propositional logic to relational monadic formulas has been presented by
Behmann in the early 1950s [6,7]. Recently the complexity of Boolean unification in a predicate logic setting has been investigated for some formula classes,
in particular for quantifier-free first-order formulas [16]. A brief discussion of
Boolean reasoning in comparison with predicate logic can be found in [8].
Here we remodel the solution problem formally along with basic classical results and some new generalizations in the framework of first-order logic extended
by second-order quantification. The main thesis of this work is that it is possible
and useful to apply second-order quantification consequently throughout the formalization. What otherwise would require meta-level notation is then expressed
just with formulas. As will be shown, classical results can be reproduced in this
framework in a way such that applicability beyond propositional logic, possible algorithmic variations, as well as connections with second-order quantifier
elimination and Craig interpolation become visible. Of course, methods to solve
Boolean equations on first-order formulas do not necessarily terminate. However, the set of solutions is recursively enumerable. By the modeling in predicate
logic we try to pin down the essential points of divergence from propositional
logic. Special cases that allow solution construction are identified, most of them
related to definiens computation by Craig interpolation. In addition, a way to
express a generalization of the solution problem where vocabulary restrictions
are taken into account in terms of two related solution problems is shown.
The envisaged application scenario is to let solving “solution problems”, or
Boolean equation solving, on the basis of predicate logic join reasoning modes
like second-order quantifier elimination (or “semantic forgetting”), Craig interpo-

4

Section 2

lation and abduction to support the mechanized reasoning about relationships
between theories and the extraction or synthesis of subtheories with given properties. On the practical side, the aim is to relate it to reasoning techniques such
as Craig interpolation on the basis of first-order provers, SAT and QBF solving, and second-order quantifier elimination based on resolution [19] and the
Ackermann approach [15]. Numerous applications of Boolean equation solving
in various fields are summarized in [31, Chap. 14]. Applications in automated
theorem proving and proof compression are mentioned in [16, Sect. 7]. The prevention of certain redundancies has been described as application of (concept)
unification in description logics [4]. Here the synthesis of definitional equivalences
is sketched as an application.
The rest of the paper is structured as follows: Notation, in particular for
substitution in formulas, is introduced in Sect. 2. In Sect. 3 a formalization of
the solution problem is presented and related to different points of view. Section 4
is concerned with abstract properties of and algorithmic approaches to solution
problems with several unknowns. Conditions under which solutions exist are
discussed in Sect. 5. Adaptions of classical material on reproductive solutions
are given in Sect. 6. In Sect. 7 various techniques for solution construction in
particular cases are discussed. The solution problem with vocabulary restrictions
is discussed in Sect. 8. The solution problem is displayed in Sect. 9 as embedded
in a setting with Skolemization and Herbrand expansion. Section 10 closes the
paper with concluding remarks.
The material in Sect. 2–5 has also been published as [40].

2
2.1

Notation and Preliminaries
Notational Conventions

We consider formulas in first-order logic with equality extended by second-order
quantification upon predicates. They are constructed from atoms (including
equality atoms), constant operators >, ⊥, the unary operator ¬, 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. 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. (Individual symbols
are not partitioned into variables and constants. Thus, an individual symbol is –
like a predicate – considered as variable if and only if it is bound by a quantifier.)
The arity of a predicate or function s is denoted by arity(s). The set of symbols
that occur free in a formula F is denoted by free(F ). The property that no
member of free(F ) is bound by a quantifier occurrence in F is expressed as
CLEAN(F ). Symbols not present in the formulas and other items under discussion

Notation and Preliminaries

5

are called fresh. The clean variant of a given formula F is the formula G obtained
from F by successively replacing all bound symbols with fresh symbols such that
CLEAN(G). The replacement is done in some way not specified here further such
that each formula has a unique clean variant.
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 .
We write sequences of symbols, of terms and of formulas by juxtaposition.
Their length is assumed to be finite. The empty sequence is written . A sequence
with length 1 is not distinguished from its sole member. In contexts where a set
is expected, a sequence stands for the set of its members. Atoms are written
in the form p(t), where t is a sequence of terms whose length is the arity of
the predicate p. Atoms of the form p(), that is, with a nullary predicate p, are
written also as p. For a sequence of fresh symbols we assume that its members
are distinct. A sequence p1 . . . pn of predicates is said to match another sequence
q1 . . . qm if and only if n = m and for all i ∈ {1, . . . , n} it holds that arity(pi ) =
arity(qi ). If s = s1 . . . sn is a sequence of symbols, then ∀s stands for ∀s1 . . . ∀sn
and ∃s for ∃s1 . . . ∃sn .
If F = F1 . . . Fn is a sequence of formulas,
then CLEAN(F ) states CLEAN(Fi )
Sn
for all i ∈ {1, . . . , n}, and free(F ) = i=1 free(Fi ). If G = G1 . . . Gn is a second
sequence of formulas, then F ≡ G stands for F1 ≡ G1 and . . . and Fn ≡ Gn .
As explained below, in certain contexts the individual symbols in the set
X = {xi | i ≥ 1} play a special role. For example in the following shorthands for a
predicate p, a formula F and x = x1 . . . xarity(p) : p ⇔ F stands for ∀x (p(x) ↔ F );
p 6⇔ F for ¬(p ⇔ F ); p ⇒ F for ∀x (p(x) → F ); and p ⇐ F for ∀x (p(x) ← F ).
2.2

Substitution with Terms and Formulas

To express systematic substitution of individual symbols and predicates concisely
we use the following notation:
– F (c) and F (t) – Notational Context for Substitution of Individual Symbols.
Let c = c1 . . . cn be a sequence of distinct individual symbols. We write F as
F (c) to declare that for a sequence t = t1 . . . tn of terms the expression F (t)
denotes F with, for i ∈ {1, . . . , n}, all free occurrences of ci replaced by ti .
– F [p], F [G] and F [q] – Notational Context for Substitution of Predicates. Let
p = p1 . . . pn be a sequence of distinct predicates and let F be a formula. We
write F as F [p] to declare the following:
• For a sequence G = G1 (x1 . . . xarity(p1 ) ) . . . Gn (x1 . . . xarity(pn ) ) of formulas
the expression F [G] denotes F with, for i ∈ {1, . . . , n}, each atom occurrence pi (t1 . . . tarity(pi ) ) where pi is free in F replaced by Gi (t1 . . . tarity(pi ) ).
• For a sequence q = q1 . . . qn of predicates that matches p the expression F [q] denotes F with, for i ∈ {1, . . . , n}, each free occurrence of pi
replaced by qi .
• The above notation F [S], where S is a sequence of formulas or of predicates, is generalized to allow also pi at the ith position of S, for example
F [G1 . . . Gi−1 pi . . . pn ]. The formula F [S] then denotes F with only those

6

Section 3

predicates pi with i ∈ {1, . . . , n} that are not present at the ith position
in S replaced by the ith component of S as described above (in the
example only p1 , . . . , pi−1 would be replaced).
– F [p] – Notational Context for Substitution in a Sequence of Formulas. If
F = F1 . . . Fn is a sequence of formulas, then F [p] declares that F [S], where
S is a sequence with the same length as p, is to be understood as the sequence
F1 [S] . . . Fn [S] with the meaning of the members as described above.
In the above notation for substitution of predicates by formulas the members
x1 , . . . , xarity(p) of X play a special role: F [G] can be alternatively considered as
obtained by replacing predicates pi with λ-expressions λx1 . . . λxarity(pi ) .Gi followed by β-conversion. The shorthand p ⇔ F can be correspondingly considered
as p ↔ λx1 . . . λxarity(p) .G. The following property substitutible specifies preconditions for meaningful simultaneous substitution of formulas for predicates:
Definition 1 (SUBST(G, p, F ) – Substitutible Sequence of Formulas).
A sequence G = G1 . . . Gm of formulas is called substitutible for a sequence
p = p1 . . . pn of distinct predicates in a formula F , written SUBST(G, p, F ), if
and only if m = n and for all i ∈ {1, . . . , n} it holds that (1.) No free occurrence
of pi in F is in the scope of a quantifier occurrence that binds a member of
free(Gi ); (2.) free(Gi ) ∩ p = ∅; and (3.) free(Gi ) ∩ {xj | j > arity(pi )} = ∅.
The following propositions demonstrate the introduced notation for formula substitution. It is well known that terms can be “pulled out of” and “pushed in to”
atoms,
justified by the equivalences p(t1 . .W. tn ) ≡ ∃x1 . . . ∃xn (p(x1 . . . xn ) ∧
Vn
n
x
i=1 i = ti ) ≡ ∀x1 . . . ∀xn (p(x1 . . . xn ) ∨ i=1 xi 6= ti ), which hold if no member of {x1 , . . . , xn } does occur in the terms t1 , . . . , tn . Analogously, substitutible
subformulas can be “pulled out of” and “pushed in to” formulas:
Proposition 2 (Pulling-Out and Pushing-In of Subformulas). Let G =
G1 . . . Gn be a sequence of formulas, let p = p1 . . . pn be a sequence of distinct
predicates and let F = F [p] be a formula such that SUBST(G, p, F ). Then
Vn
Wn
(i) F [G] ≡ ∃p (F ∧ i=1 (pi ⇔ Gi )) ≡ ∀p (F ∨ i=1 (pi 6⇔ Gi )).
(ii) ∀p F |= F [G] |= ∃p F.
Ackermann’s Lemma [1] can be applied in certain cases to eliminate second-order
quantifiers, that is, to compute for a given second-order formula an equivalent
first-order formula. It plays an important role in many modern methods for
elimination and semantic forgetting – see, e.g., [15,12,18,33,23,41]:
Proposition 3 (Ackermann’s Lemma, Positive Version). Let F, G be formulas and let p be a predicate such that SUBST(G, p, F ), p ∈
/ free(G) and all free
occurrences of p in F have negative polarity. Then ∃p ((p ⇐ G) ∧ F [p]) ≡ F [G].

3
3.1

The Solution Problem from Different Angles
Basic Formal Modeling

Our formal modeling of the Boolean solution problem is based on two concepts,
solution problem and particular solution:

The Solution Problem from Different Angles

7

Definition 4 (F [p] – Solution Problem (SP), Unary Solution Problem
(1-SP)). A solution problem (SP) F [p] is a pair of a formula F and a sequence p
of distinct predicates. The members of p are called the unknowns of the SP. The
length of p is called the arity of the SP. A SP with arity 1 is also called unary
solution problem (1-SP).
The notation F [p] for solution problems establishes as a “side effect” a context
for specifying substitutions of p in F by formulas as specified in Sect. 2.2.
Definition 5 (Particular Solution). A particular solution (briefly solution)
of a SP F [p] is defined as a sequence G of formulas such that SUBST(G, p, F )
and |= F [G].
The property SUBST(G, p, F ) in this definition implies that no member of p
occurs free in a solution. Of course, particular solution can also be defined on the
basis of unsatisfiability instead of validity, justified by the equivalence of |= F [G]
and ¬F [G] |= ⊥. The variant based on validity has been chosen here because
then the associated second-order quantifications are existential, matching the
usual presentation of elimination techniques.
Being a solution is aside of the substitutibility condition a semantic property,
that is, applying to formulas modulo equivalence: If G is a solution of F [p], then
all sequences H of formulas such that SUBST(H, p, F ) and G ≡ H (that is, if
G = G1 . . . Gn and H = H1 . . . Hn , then Hi ≡ Gi holds for all i ∈ {1, . . . , n})
are also solutions of F [p].
Solution problem and solution as defined here provide abstractions of computational problems in a technical sense that would be suitable, e.g., for complexity
analysis. Problems in the latter sense can be obtained by fixing involved formula
and predicate classes. The abstract notions are adequate to develop much of the
material on the “Boolean solution problem” shown here. On occasion, however,
we consider restrictions, in particular to propositional and to first-order formulas,
as well as to nullary predicates. As shown in Sect. 6, further variants of solution,
general representations of several particular solutions, can be introduced on the
basis of the notions defined here.
Example 6 (A Solution Problem and its Particular Solutions). As an
example of a solution problem consider F [p1 p2 ] where
F = ∀x (a(x ) → b(x )) →
(∀x (p1 (x ) → p2 (x )) ∧ ∀x (a(x ) → p2 (x )) ∧ ∀x (p2 (x ) → b(x ))).
The intuition is that the antecedent ∀x (a(x ) → b(x )) specifies the “background
theory”, and w.r.t. that theory the unknown p1 is “stronger” than the other
unknown p2 , which, in addition, is “between” a and b. Examples of solutions are:
a(x1 )a(x1 ); a(x1 )b(x1 ); ⊥a(x1 ); b(x1 )b(x1 ); and (a(x1 ) ∧ b(x1 ))(a(x1 ) ∨ b(x1 )).
No solutions are for example b(x1 )a(x1 ); a(x1 )⊥; and all members of {>, ⊥} ×
{>, ⊥}.
Assuming a countable vocabulary, the set of valid first-order formulas is recursively enumerable. It follows that for an n-ary SP F [p] where F is first-order the

8

Section 3

set of those of its particular solutions that are sequences of first-order formulas
is also recursively enumerable: An n-ary sequence G of well-formed first-order
formulas that satisfies the syntactic restriction SUBST(G, p, F ) is a solution of
F [p] if and only if F [G] is valid.
In the following subsections further views on the solution problem will be
discussed: as unification or equation solving, as a special case of second-order
quantifier elimination, and as related to determining definientia and interpolants.
3.2

View as Unification

Because |= F [G] if and only if F [G] ≡ >, a particular solution of F [p] can be
seen as a unifier of the two formulas F [p] and > modulo logical equivalence as
equational theory. From the perspective of unification the two formulas appear
as terms, the members of p play the role of variables and the other predicates
play the role of constants.
Vice versa, a unifier of two formulas can be seen as a particular solution,
justified by the equivalence of L[G] ≡ R[G] and |= (L ↔ R)[G], which holds
for sequences G and p of formulas and predicates, respectively, and formulas
L = L[p], R = R[p], (L ↔ R) = (L ↔ R)[p] such that SUBST(G, p, L) and
SUBST(G, p, R). This view of formula unification can be generalized to sets
with a finite cardinality k of equivalences, since for all i ∈ {1, . . . , k} it holds
Vk
that Li ≡ Ri can be expressed as |= i=1 (Li ↔ Ri ).
An exact correspondence between solving a solution problem F [p1 . . . pn ]
where F is a propositional formula with ∨, ∧, ¬, ⊥, > as logic operators and
E-unification with constants in the theory of Boolean algebra (with the mentioned logic operators as signature) applied to F =E > can be established:
Unknowns p1 , . . . , pn correspond to variables and propositional atoms in F correspond to constants. A particular solution G1 . . . Gn corresponds to a unifier
{p1 ← G1 , . . . , pn ← Gn } that is a ground substitution. The restriction to ground
substitutions is due to the requirement that unknowns do not occur in solutions.
General solutions Sect. 6 are expressed with further special parameter atoms,
different from the unknowns. These correspond to fresh variables in unifiers.
A generalization of Boolean unification to predicate logic with various specific
problems characterized by the involved formula classes has been investigated
in [16]. The material presented here is largely orthogonal to that work, but a
technique from [16] has been adapted to more general cases in Sect. 7.3.
3.3

View as Construction of Elimination Witnesses

Another view on the solution problem is related to eliminating second-order
quantifiers by replacing the quantified predicates with “witness formulas”.
Definition 7 (ELIM-Witness). Let p = p1 . . . pn be a sequence of distinct
predicates. An ELIM-witness of p in a formula ∃p F [p] is defined as a sequence
G of formulas such that SUBST(G, p, F ) and ∃p F [p] ≡ F [G].

The Solution Problem from Different Angles

9

The condition ∃p F [p] ≡ F [G] in this definition is equivalent to |= ¬F [p] ∨ F [G].
If F [p] and the considered G are first-order, then finding an ELIM-witness is
second-order quantifier elimination on a first-order argument formula, restricted
by the condition that the result is of the form F [G]. Differently from the general case of second-order quantifier elimination on first-order arguments, the set
of formulas for which elimination succeeds and, for a given formula, the set of
its elimination results, are then recursively enumerable. Some well-known elimination methods yield ELIM-witnesses, for example rewriting a formula that
matches the left side of Ackermann’s Lemma (Prop. 3) with its right side,
which becomes evident when considering that the right side F [G] is equivalent to ∀x1 . . . ∀xarity(p) (G ← G) ∧ F [G]. Finding particular solutions and finding
ELIM-witnesses can be expressed in terms of each other:
Proposition 8 (Solutions and ELIM-Witnesses). Let F [p] be a SP and let
G be a sequence of formulas. Then:
(i) G is an ELIM-witness of p in ∃p F if and only if G is a solution of the
SP (¬F [q] ∨ F )[p], where q is a sequence of fresh predicates matching p.
(ii) G is a solution of F [p] if and only if G is an ELIM-witness of p in ∃p F
and it holds that |= ∃p F .
Proof (Sketch). Assume SUBST(G, p, F ). (8.i) Follows since ∃p F [p] ≡ F [G]
iff ∃p F [p] |= F [G] iff F [p] |= F [G] iff |= ¬F [q] ∨ F [G]. (8.ii) Left-To-Right:
Follows since |= F [G] implies |= ∃p F [p] and |= F [G], which implies ∃p F [p] ≡
> ≡ F [G]. Right-to-left: Follows since ∃p F [p] ≡ F [G] and |= ∃p F [p] together
imply |= F [G].
t
u
3.4

View as Related to Definientia and Interpolants

The following proposition shows a further view on the solution problem that
relates it to definitions of the unknown predicates:
Proposition 9 (Solution as Entailed by a Definition). A sequence G =
G1 . . . Gn of formulas is a particular
solution of a SP F [p = p1 . . . pn ] if and
Vn
only if SUBST(G, p, F ) and i=1 (pi ⇔ Gi ) |= F .
Proof. Follows from the definition of particular solution and Prop. 2.i.

t
u

In the special case where F [p] is a 1-SP with a nullary unknown p, the characterization of a solution G according to Prop. 9 can be expressed with an entailment
where a definition of the unknown p appears on the right instead of the left side:
If p is nullary, then ¬(p ⇔ G) ≡ p ⇔ ¬G. Thus, the statement p ⇔ G |= F is
for nullary p equivalent to
¬F |= p ⇔ ¬G.
(i)
The second condition of the characterization of solution according to Prop. 9,
that is, SUBST(G, p, F ), holds if it is assumed that p is not in free(G), that
free(G) ⊆ free(F ) and that no member of free(F ) is bound by a quantifier occurrence in F . A solution is then characterized as negated definiens of p in the

10

Section 4

negation of F . Another way to express (i) along with the condition that G is
semantically independent from p is as follows:
∃p (¬F ∧ ¬p) |= G |= ¬∃p (¬F ∧ p).

(ii)

The second-order quantifiers upon the nullary p can be eliminated, yielding the
following equivalent statement:
¬F [⊥] |= G |= F [>].

(iii)

Solutions G then appear as the formulas in a range, between ¬F [⊥] and F [>].
This view is reflected in [30, Thm. 2.2], which goes back to work by Schröder.
If F is first-order, then Craig interpolation can be applied to compute formulas G that also meet the requirements free(G) ⊆ free(F ) and p ∈
/ free(F ) to
ensure SUBST(G, p, F ). Further connections to Craig interpolation are discussed
in Sect. 7.

4

The Method of Successive Eliminations – Abstracted

4.1

Reducing n-ary to 1-ary Solution Problems

The method of successive eliminations to solve an n-ary solution problem by
reducing it to unary solution problems is attributed to Boole and has been formally described in a modern algebraic setting in [30, Chapter 2, § 4]. It has
been rediscovered in the context of Boolean unification in the late 1980s, notably with [9]. Rudeanu notes in [30, p. 72] that variants described by several
authors in the 19th century are discussed by Schröder [34, vol. 1, §§ 26,27]. To
research and compare all variants up to now seems to be a major undertaking on
its own. Our aim is here to provide a foundation to derive and analyze related
methods. The following proposition formally states the core property underlying the method in a way that, compared to the Boolean algebra version in [30,
Chapter 2, § 4], is more abstract in several aspects: Second-order quantification
upon predicates that represent unknowns plays the role of meta-level shorthands
that encode expansions; no commitment to a particular formula class is made,
thus the proposition applies to second-order formulas with first-order and propositional formulas as special cases; it is not specified how solutions of the arising
unary solution problems are constructed; and it is not specified how intermediate
second-order formulas (that occur also for inputs without second-order quantifiers) are handled. The algorithm descriptions in the following subsections show
different possibilities to instantiate these abstracted aspects.
Proposition 10 (Characterization of Solution Underlying the Method
of Successive Eliminations). Let F [p = p1 . . . pn ] be a SP and let G =
G1 . . . Gn be a sequence of formulas. Then the following statements are equivalent:
(a) G is a solution of F [p].

The Method of Successive Eliminations – Abstracted

11

(b) For i ∈ {1, . . . , n}: Gi is a solution of the 1-SP
(∃pi+1 . . . ∃pn F [G1 . . . Gi−1 pi . . . pn ])[pi ]
such that free(Gi ) ∩ p = ∅.
Proof. Left-to-right: From (a) it follows that |= F [G]. Hence, for all i ∈ {1, . . . , n}
by Prop. 2.ii it follows that
|= ∃pi+1 . . . ∃pn F [G1 . . . Gi pi+1 . . . pn ].
From (a) it also follows that SUBST(G, p, F ). This implies that for all i ∈
{1, . . . , n} it holds that
SUBST(Gi , pi , ∃pi+1 . . . ∃pn F [G1 . . . Gi−1 pi . . . pn ]) and free(Gi ) ∩ p = ∅.
We thus have derived for all i ∈ {1, . . . , n} the two properties that characterize
Gi as a solution of the 1-SP as stated in (b).
Right-to-left: From (b) it follows that Gn is a solution of the 1-SP
(F [G1 . . . Gn−1 pn ])[pn ].
Hence, by the characteristics of solution it follows that |= F [G1 . . . Gn ]. The property SUBST(G, p, F ) can be derived from free(G)∩p = ∅ and the fact that for all
i ∈ {1, . . . , n} it holds that SUBST(Gi , pi , (∃pi+1 . . . ∃pn F [G1 . . . Gi−1 pi . . . pn ])).
The properties |= F [G1 . . . Gn ] and SUBST(G, p, F ) characterize G as a solution
of the SP F [p].
t
u
This proposition states an equivalence between the solutions of an n-ary SP
and the solutions of n 1-SPs. These 1-SPs are on formulas with an existential
second-order prefix. The following gives an example of this decomposition:
Example 11 (Reducing an n-ary Solution Problem to Unary Solution
Problems). Consider the SP F [p1 p2 ] of Examp. 6. The 1-SP with unknown p1
according to Prop. 10 is
(∃p2 F [p1 p2 ])[p1 ],
whose formula is, by second-order quantifier elimination, equivalent to ∀x (a(x ) →
b(x )) → ∀x (p1 (x ) → b(x )). Take a(x1 ) as solution G1 of that 1-SP. The 1-SP
with unknown p2 according to Prop. 10 is
(F [G1 p2 ])[p2 ].
Its formula is then, by replacing p1 in F as specified in Examp. 6 with a and
removing the duplicate conjunct obtained then, equivalent to
∀x (a(x ) → b(x )) → (∀x (a(x ) → p2 (x )) ∧ ∀x (p2 (x ) → b(x ))).
A solution of that second 1-SP is, for example, b(x1 ), yielding the pair a(x1 )b(x1 )
as solution of the originally considered SP F [p1 p2 ].

12
4.2

Section 4

Solving on the Basis of Second-Order Formulas

The following algorithm to compute particular solutions is an immediate transfer
of Prop. 10. Actually, it is more an “algorithm template”, since it is parameterized
with a method to compute 1-SPs and covers a nondeterministic as well as a
deterministic variant:
Algorithm 12 (SOLVE-ON-SECOND-ORDER). Let F be a class of formulas
and let 1 -SOLVE be a nondeterministic or a deterministic algorithm that outputs for 1-SPs of the form (∃p1 . . . ∃pn F [p])[p] with F ∈ F solutions G such that
free(G) ∩ {p1 , . . . , pn } = ∅ and F [G] ∈ F.
Input: A SP F [p1 . . . pn ], where F ∈ F, that has a solution.
Method: For i := 1 to n do: Assign to Gi an output of 1 -SOLVE applied to
the 1-SP (∃pi+1 . . . ∃pn F [G1 . . . Gi−1 pi . . . pn ])[pi ].
Output: The sequence G1 . . . Gn of formulas, which is a particular solution of
F [p1 . . . pn ].
The solution components Gi are successively assigned to some solution of the
1-SP given in Prop. 10, on the basis of the previously assigned components
G1 . . . Gi−1 . Even if the formula F of the input problem does not involve secondorder quantification, these 1-SPs are on second-order formulas with an existential
prefix ∃pi+1 . . . ∃pn upon the yet “unprocessed” unknowns.
The algorithm comes in a nondeterministic and a deterministic variant, just
depending on whether 1 -SOLVE is instantiated by a nondeterministic or a deterministic algorithm. Thus, in the nondeterministic variant the nondeterminism
of 1 -SOLVE is the only source of nondeterminism. With Prop. 10 it can be verified that if a nondeterministic 1 -SOLVE is “complete” in the sense that for each
solution there is an execution path that leads to the output of that solution,
then also SOLVE-ON-SECOND-ORDER based on it enjoys that property, with
respect to the n-ary solutions G1 . . . Gn .
For the deterministic variant, from Prop. 10 it follows that if 1 -SOLVE is
“complete” in the sense that it outputs some solution whenever a solution exists,
then, given that F [p1 . . . pn ] has a solution, which is ensured by the specification
of the input, also SOLVE-ON-SECOND-ORDER outputs some solution G1 . . . Gn .
This method applies 1 -SOLVE to existential second-order formulas, which
prompts some issues for future research: As indicated in Sect. 3.4 (and elaborated
in Sect. 7) Craig interpolation can in certain cases be applied to compute solutions of 1-SPs. Can QBF solvers, perhaps those that encode QBF into predicate
logic [35], be utilized to compute Craig interpolants? Can it be useful to allow
second-order quantifiers in solution formulas because they make these smaller
and can be passed between different calls to 1 -SOLVE ?
As shown in Sect. 6, if 1 -SOLVE is a method that outputs so-called reproductive solutions, that is, most general solutions that represent all particular solutions, then also SOLVE-ON-SECOND-ORDER outputs reproductive solutions.
Thus, there are two ways to obtain representations of all particular solutions
whose comparison might be potentially interesting: A deterministic method that

The Method of Successive Eliminations – Abstracted

13

outputs a single reproductive solution and the nondeterministic method with an
execution path to each particular solution.
4.3

Solving with the Method of Successive Eliminations

The method of successive eliminations in a narrower sense is applied in a Boolean
algebra setting that corresponds to propositional logic and outputs reproductive solutions. The consideration of reproductive solutions belongs to the classical material on Boolean reasoning [34,25,30] and is modeled in the present
framework in Sect. 6. Compared to SOLVE-ON-SECOND-ORDER, the method
handles the second-order quantification by eliminating quantifiers one-by-one,
inside-out, with a specific method and applies a specific method to solve 1-SPs,
which actually yields reproductive solutions. These incorporated methods apply
to propositional input formulas (and to first-order input formulas if the unknowns are nullary). Second-order quantifiers are eliminated by rewriting with
the equivalence ∃p F [p] ≡ F [>] ∨ F [⊥]. As solution of an 1-SP F [p] the formula
(¬F [⊥] ∧ t) ∨ (F [>] ∧ ¬t) is taken, where t is a fresh nullary predicate that is
considered specially. The intuition is that particular solutions are obtained by
replacing t with arbitrary formulas in which p does not occur (see Sect. 6 for a
more in-depth discussion).
The following algorithm is an iterative presentation of the method of successive eliminations, also called Boole’s method, in the variant due to [9]. The
presentation in [28, Sect. 3.1], where apparently minor corrections compared
to [9] have been made, has been taken here as technical basis. We stay in the
validity-based setting, whereas [30,9,28] use the unsatisfiability-based setting.
Also differently from [9,28] we do not make use of the xor operator.
Algorithm 13 (SOLVE-SUCC-ELIM).
Input: A SP F [p1 . . . pn ], where F is propositional, that has a solution and a
sequence t1 . . . tn of fresh nullary predicates.
Method:
1. Initialize Fn [p1 . . . pn ] with F .
2. For i := n to 1 do: Assign to Fi−1 [p1 . . . pi−1 ] the formula Fi [p1 . . . pi−1 >] ∨
Fi [p1 . . . pi−1 ⊥].
3. For i := 1 to n do: Assign to Gi the formula (¬Fi [G1 . . . Gi−1 ⊥] ∧ ti ) ∨
(Fi [G1 . . . Gi−1 >] ∧ ¬ti ).
Output: The sequence G1 . . . Gn of formulas, which is a reproductive solution
of F [p1 . . . pn ] with respect to the special predicates t1 . . . tn .
The formula assigned to Fi−1 in step (2.) is the result of eliminating ∃pi in
∃pi Fi [p1 . . . pi ] and the formula assigned to Gi in step (3.) is the reproductive
solution of the 1-SP (Fi [G1 . . . Gi−1 pi ])[pi ], obtained with the respective incorporated methods indicated above. The recursion in the presentations of [9,28]
is translated here into two iterations that proceed in opposite directions: First,

14

Section 4

existential quantifiers of ∃p1 . . . ∃pn F are eliminated inside-out and the intermediate results, which do not involve second-order quantifiers, are stored. Solutions
of 1-SPs are computed in the second phase on the basis of the stored formulas.
In this presentation it is easy to identify two “hooks” where it is possible to
plug-in alternate methods that produce other outputs or apply to further formula classes: In step (2.) the elimination method and in step (3.) the method to
determine solutions of 1-SPs. If the plugged-in method to compute 1-SPs outputs particular solutions, then SOLVE-SUCC-ELIM computes particular instead
of reproductive solutions.
4.4

Solving by Inside-Out Witness Construction

Like SOLVE-SUCC-ELIM, the following algorithm eliminates second-order quantifiers one-by-one, inside-out, avoiding intermediate formulas with existential
second-order prefixes of length greater than 1, which arise with SOLVE-ONSECOND-ORDER. In contrast to SOLVE-SUCC-ELIM, it performs elimination by
the computation of ELIM-witnesses.
Algorithm 14 (SOLVE-BY-WITNESSES). Let F be a class of formulas and
ELIM -WITNESS be an algorithm that computes for formulas F ∈ F and predicates p an ELIM-witness G of p in ∃p F [p] such that F [G] ∈ F.
Input: A SP F [p1 . . . pn ], where F ∈ F, that has a solution.
Method: For i := n to 1 do:
1. Assign to Gi [p1 . . . pi−1 ] the output of ELIM -WITNESS applied to
∃pi F [p1 . . . pi Gi+1 . . . Gn ].
2. For j := n to i+1 do: Re-assign to Gj [p1 . . . pi−1 ] the formula Gj [p1 . . . pi−1 Gi ].
Output: : The sequence G1 . . . Gn of formulas, which provides a particular
solution of F [p1 . . . pn ].
Step (2.) in the algorithm expresses that a new value is assigned to Gj and that
Gj can be designated by Gj [p1 . . . pi−1 ], justified because the new value does not
contain free occurrences of pi , . . . , pn . In step (1.) the respective current values of
Gi+1 . . . Gn are used to instantiate F . It is not hard to see from the specification
of the algorithm that for input F [p] and output G it holds that ∃p F ≡ F [G]
and that SUBST(G, p, F ). By Prop. 8.ii, G is then a solution if |= ∃p F . This
holds indeed if F [p] has a solution, as shown below with Prop. 15.
If ELIM -WITNESS is “complete” in the sense that it computes an elimination witness for all input formulas in F, then SOLVE-BY-WITNESSES outputs a
solution. Whether all solutions of the input SP can be obtained as outputs for different execution paths of a nondeterministic version of SOLVE-BY-WITNESSES
obtained through a nondeterministic ELIM -WITNESS , in analogy to the nondeterministic variant of SOLVE-ON-SECOND-ORDER, appears to be an open
problem.

15

Existence of Solutions

5
5.1

Existence of Solutions
Conditions for the Existence of Solutions

We now turn to the question under which conditions there exists a solution of
a given SP, or, in the terminology of [30], the SP is consistent. A necessary
condition is easy to see:
Proposition 15 (Necessary Condition for the Existence of a Solution).
If a SP F [p] has a solution, then it holds that |= ∃p F .
Proof. Follows from the definition of particular solution and Prop. 2.ii.

t
u

Under certain presumptions that hold for propositional logic this condition is
also sufficient. To express these abstractly we use the following concept:
Definition 16 (SOL-Witnessed Formula Class). A formula class F is called
SOL-witnessed for a predicate class P if and only if for all p ∈ P and F [p] ∈ F
the following statements are equivalent:
(a) |= ∃p F .
(b) There exists a solution G of the 1-SP F [p] such that F [G] ∈ F.
Since the right-to-left direction of that equivalence holds in general, the leftto-right direction alone would provide an alternate characterization. The class
of propositional formulas is SOL-witnessed (for the class of nullary predicates).
This follows since in propositional logic it holds that
∃p F [p] ≡ F [F [>]],

(iv)

which can be derived in the following steps: F [F [>]] ≡ ∃p (F [p]∧(p ↔ F [>])) ≡
(F [>] ∧ (> ↔ F [>])) ∨ (F [⊥] ∧ (⊥ ↔ F [>])) ≡ F [>] ∨ F [⊥] ≡ ∃p F [p].
The following definition adds closedness under existential second-order quantification and dropping of void second-order quantification to the notion of SOLwitnessed, to allow the application on 1-SPs matching with item (b) in Prop. 10:
Definition 17 (MSE-SOL-Witnessed Formula Class). A formula class F
is called MSE-SOL-witnessed for a predicate class P if and only if it is SOLwitnessed for P, for all predicates in p ∈ P and F ∈ F it holds that ∃p F ∈ F,
and, if ∃p F ∈ F and p ∈
/ free(F ), then F ∈ F.
The class of existential QBFs (formulas of the form ∃p F where F is propositional) is MSE-SOL-witnessed (like the more general class of QBFs – secondorder formulas with only nullary predicates). Another example is the class of
first-order formulas extended by second-order quantification upon nullary predicates, which is MSE-SOL-witnessed for the class of nullary predicates. The
following proposition can be seen as expressing an invariant of the method of
successive eliminations that holds for formulas in an MSE-SOL-witnessed class:

16

Section 5

Proposition 18 (Solution Existence Lemma). Let F be a formula class
that is MSE-SOL-witnessed for predicate class P. Let F [p = p1 . . . pn ] ∈ F with
p ∈ P n . If |= ∃p F [p], then for all i ∈ {0, . . . , n} there exists a sequence G1 . . . Gi
of formulas such that free(G1 . . . Gi ) ∩ p = ∅, SUBST(G1 . . . Gi , p1 . . . pi , F ),
|= ∃pi+1 . . . ∃pn F [G1 . . . Gi pi+1 . . . pn ] and ∃pi+1 . . . ∃pn F [G1 . . . Gi pi+1 . . . pn ] ∈ F.
Proof. By induction on the length i of the sequence G1 . . . Gi . The conclusion
of the proposition holds for the base case i = 0: The statement SUBST(, , F )
holds trivially, |= ∃p F is given as precondition, and ∃p F ∈ F follows from
F ∈ F. For the induction step, assume that the conclusion of the proposition
holds for some i ∈ {0, . . . n − 1}. That is, there exists a sequence G1 . . . Gi
of formulas such that free(G1 . . . Gi ) ∩ p = ∅, SUBST(G1 . . . Gi , p1 . . . pi , F ),
|= ∃pi+1 . . . ∃pn F [G1 . . . Gi pi+1 . . . pn ] and ∃pi+1 . . . ∃pn F [G1 . . . Gi pi+1 . . . pn ] ∈
F. Since F is MSE-SOL-witnessed for P and p1 , . . . , pi ∈ P it follows that there
exists a solution Gi+1 of the 1-SP
(∃p1 . . . ∃pi ∃pi+2 . . . ∃pn F [G1 . . . Gi pi+1 . . . pn ])[pi+1 ]
such that ∃p1 . . . ∃pi ∃pi+2 . . . ∃pn F [G1 . . . Gi+1 pi+2 . . . pn ] ∈ F. From the characteristics of solution it follows that
SUBST(Gi+1 , pi+1 , ∃p1 . . . ∃pi ∃pi+2 . . . ∃pn F [G1 . . . Gi pi+1 . . . pn ]),
which implies (since all members of p with exception of pi+1 are in the quantifier
prefix of the problem formula) that free(Gi+1 ) ∩ p = ∅, hence
free(G1 . . . Gi+1 ) ∩ p = ∅.
Given the induction hypothesis SUBST(G1 . . . Gi , p1 . . . pi , F ), it also implies
SUBST(G1 . . . Gi+1 , p1 . . . pi+1 , F ).
From the characteristics of solution it follows in addition that
|= ∃p1 . . . ∃pi ∃pi+2 . . . ∃pn F [G1 . . . Gi+1 pi+2 . . . pn ],
which, since free(G1 . . . Gi+1 ) ∩ p = ∅, is equivalent to
|= ∃pi+2 . . . ∃pn F [G1 . . . Gi+1 pi+2 . . . pn ].
Finally, we conclude from ∃p1 . . . ∃pi ∃pi+2 . . . ∃pn F [G1 . . . Gi+1 pi+2 . . . pn ] ∈ F,
established above, and the definition of MSE-SOL-witnessed that
∃pi+2 . . . ∃pn F [G1 . . . Gi+1 pi+2 . . . pn ] ∈ F,
which completes the proof of the induction step.

t
u

A sufficient and necessary condition for the existence of a solution of formulas
in MSE-SOL-witnessed classes now follows from Prop. 18 and Prop. 15:

Existence of Solutions

17

Proposition 19 (Existence of a Solution). Let F be a formula class that
is MSE-SOL-witnessed on predicate class P. Then for all F [p] ∈ F where the
members of p are in P the following statements are equivalent:
(a) |= ∃p F .
(b) There exists a solution G of the SP F [p] such that F [G] ∈ F.
Proof. Follows from Prop. 18 and Prop. 15.

t
u

From that proposition it is easy to see that for SPs with propositional formulas
the complexity of determining the existence of a solution is the same as the
complexity of deciding validity of existential QBFs, as proven in [21,22,2], that
is, ΠP
2 -completeness: By Prop. 19, a SP F [p] where F is propositional has a
solution if and only if the existential QBF ∃p F [p] is valid and, vice versa, an
arbitrary existential QBF ∃p F [p] (where F is quantifier-free) is valid if and only
if the SP F [p] has a solution.
5.2

Characterization of SOL-Witnessed in Terms of ELIM-Witness

The following proposition shows that under a minor syntactic precondition on
formula classes, SOL-witnessed can also be characterized in terms of ELIMwitness instead of solution as in Def. 16:
Proposition 20 (SOL-Witnessed in Terms of ELIM-Witness). Let F be
a class of formulas that satisfies the following properties: For all F [p] ∈ F and
predicates q with the same arity of p it holds that F [p] ∨ ¬F [q] ∈ F, and for all
F ∨ G ∈ F it holds that F ∈ F. The class F is SOL-witnessed for a predicate
class P if and only if for all p ∈ P and F [p] ∈ F there exists an ELIM-witness
G of p in F [p] such that F [G] ∈ F.
Proof. Left-to-right: Assume that F is meets the specified closedness conditions
and is SOL-witnessed for P, p ∈ P and F [p] ∈ F. Let q be a fresh predicate with
the arity of p. The obviously true statement |= ∃p F [p] ∨ ¬∃p F [p] is equivalent to
|= ∃p F [p]∨¬F [q] and thus to |= ∃p (F [p]∨¬F [q]). By the closedness properties of
F it holds that F [p] ∨ ¬F [q] ∈ F. Since F is SOL-witnessed for P it thus follows
from Def. 16 that there exists a solution G of the SP (F [p] ∨ ¬F [q])[p] such that
(F [G] ∨ ¬F [q]) ∈ F, and, by the closedness properties, also F [G] ∈ F. From
the definition of solution it follows that |= F [G] ∨ ¬F [q], which is equivalent
to ∃p F [p] ≡ F [G], and also that SUBST(G, p, F [G] ∨ ¬F [q]), which implies
SUBST(G, p, F [G]). Thus G is an SO-witness of p in F [p] such that F [G] ∈ F.
Right-to-left: Easy to see from Prop. 8.ii.
t
u
5.3

The Elimination Result as Precondition of Solution Existence

Proposition 19 makes an interesting relationship between the existence of a solution and second-order quantifier elimination apparent that has been pointed
out by Schröder [34, vol. 1, § 21] and Behmann [6], and is briefly reflected in

18

Section 6

[30, p. 62]: The formula ∃p F is valid if and only if the result of eliminating the
existential second-order prefix (called Resultante by Schröder [34, vol. 1, § 21]) is
valid. If it is not valid, then, by Prop. 19, the SP F [p] has no solution, however,
in that case the elimination result represents the unique (modulo equivalence)
weakest precondition under which the SP would have a solution. The following
proposition shows a way to make this precise:
Proposition 21 (The Elimination Result is the Unique Weakest Precondition of Solution Existence). Let F be a formula class and let P be a
predicate class such that F is MSE-SOL-witnessed on P. Let F [p] be a solution
problem where F ∈ F and all members of p are in P. Let A be a formula such
that (A → F ) ∈ F, A ≡ ∃p F , and no member of p does occur in A. Then
(i) The SP (A → F )[p] has a solution.
(ii) If B is a formula such that (B → F ) ∈ F, no member of p occurs in B,
and the SP (B → F )[p] has a solution, then B |= A.
Proof. (21.i) From the specification of A it follows that |= A → ∃pF and thus
|= ∃p (A → F ). Hence, by Prop. 19, the SP (A → F )[p] has a solution. (21.ii)
Let B be a formula such that the left side of holds. With Prop. 19 it follows that
|= B → ∃pF . Hence B |= ∃pF . Hence B |= A.
t
u
The following example illustrates Prop. 21:
Example 22 (Elimination Result as Precondition for Solvability). Consider the SP F [p1 p2 ] where
F = ∀x (p1 (x ) → p2 (x )) ∧ ∀x (a(x ) → p2 (x )) ∧ ∀x (p2 (x ) → b(x )).
Its formula is the consequent of the SP considered in Examp. 6. Since ∃p1 ∃p2 F ≡
∀x (a(x ) → b(x )) 6≡ >, from Prop. 19 it follows that F [p1 p2 ] has no solution.
If, however, the elimination result ∀x (a(x ) → b(x )) is added as an antecedent
to F , then the resulting SP, which is the SP of Examp. 6, has a solution.

6

Reproductive Solutions as Most General Solutions

Traditionally, concise representations of all particular solutions have been central to investigations of the solution problem. This section presents adaptions of
classic material to this end, due in particular to Schröder and Löwenheim, and
presented in a modern algebraic formalization by Rudeanu [30]. The idea is that
a general solution G[t] has parameter predicates t such that each instantiation
G[T ] with a sequence T of formulas is a particular solution and that for all particular solutions H there exists a sequence T of formulas such that H ≡ G[T ].
In this way, a general solution represents all solutions. A remaining difficulty is
to determine for a given particular solution H the associated T . This is remedied
with so-called reproductive solutions, for which H itself can be taken as T , that
is, it holds that G[H] ≡ H.

Reproductive Solutions as Most General Solutions

19

We give formal adaptions in the framework of predicate logic that center
around the notion of reproductive solution. This includes precise specifications
of reproductive solution and two further auxiliary types of solution. A technique
to construct a reproductive solution from a given particular solution, known
as Schröder’s rigorous solution or Löwenheim’s theorem and a construction of
reproductive solutions due to Schröder, which succeeds on propositional formulas
in general, is adapted. Finally, a way to express reproductive solutions of n-ary
SPs in terms of reproductive solutions of 1-SPs in the manner of the method of
successive eliminations is shown.
6.1

Parametric, General and Reproductive Solutions

The following definitions give adaptions of the notions of parametric, general and
reproductive solution for predicate logic, based on the modern algebraic notions
in [30,14] as starting point.
Definition 23 (Parametric and Reproductive Solution Problem (PSP,
RSP, 1-RSP)). A parametric solution problem (PSP) F [p]:t is a pair of a
solution problem F [p] and a sequence t of distinct predicates such that (free(F )∪
p) ∩ t = ∅. The members of t are called the solution parameters of the PSP.
If the sequences of predicates p and t are matching, then the PSP is called a
reproductive solution problem (RSP). A RSP with arity 1 is also called unary
reproductive solution problem (1-RSP).
Definition 24 (Parametric, General and Reproductive Solution). Define the following notions:
(i) A parametric solution of a PSP F [p]:t is a sequence G[t] of formulas such
that CLEAN(G), SUBST(G, p, F ) and for all sequences of formulas H such that
SUBST(H, t, G) and SUBST(H, p, F ) it holds that if there exists a sequence T
of formulas such that SUBST(T , t, G), SUBST(G[T ], p, F ) and
H ≡ G[T ],
then
|= F [H].
(ii) A general solution of a PSP F [p]:t is a sequence G[t] of formulas such that
the characterization of parametric solution (Def. 24.i) applies, with the if-then
implication supplemented by its converse.
(iii) A reproductive solution of a RSP F [p]:t is a sequence G[t] of formulas
such that
1. G is a parametric solution of F [p]:t and
2. For all sequences H of formulas such that SUBST(H, t, G) and
SUBST(H, p, F ) it holds that if
|= F [H],
then
H ≡ G[H].

20

Section 6

Parametric solution can be characterized more concisely than in Def. 24.i, but
not showing the syntactic correspondence to the characterization of general solution in Def. 24.ii:
Proposition 25 (Compacted Characterization of Parametric Solution).
A parametric solution of a PSP F [p]:t is a sequence G[t] of formulas such
that CLEAN(G), SUBST(G, p, F ) and for all sequences T of formulas such that
SUBST(T , t, G), SUBST(G[T ], p, F ) it holds that
|= F [G[T ]].
Proof. The left side of the proposition can be expressed as:
(1) CLEAN(G),
(2) SUBST(G, p, F ),
and for all sequences H, T of formulas it holds that
if
(3) SUBST(H, t, G), (III)
(4) SUBST(H, p, F ),
(5) SUBST(T , t, G),
(6) SUBST(G[T ], p, F ) and
(7) H ≡ G[T ],
then
(8) |= F [H].
The right side of the proposition can be expressed as:
(9) CLEAN(G),
(10) SUBST(G, p, F ),
and for all sequences T of formulas it holds that
if
(11) SUBST(T , t, G) and
(12) SUBST(G[T ], p, F ),
then
(13) |= F [G[T ]].
Left-to-right: If H = G[T ], then H ≡ G[T ]. Thus, this direction of the proposition follows if statements (9)–(12) imply (1)–(6), with H instantiated to G[T ].
Statements (1), (2), (5) and (6) are (9), (10), (11) and (12), respectively. The
instantiation of (3), that is, SUBST(G[T ], t, G), follows from (10) and (11). The
instantiation of (4) is SUBST(G[T ], p, F ), which is, like (6), identical to (12).
Right-to-left: Statements (1)–(7) imply (9)–(12). This holds since (1), (2), (5)
and (6) are (9), (10), (11) and (12), respectively. Hence, assuming the right side
of the proposition, statements (1)–(7) then imply (13), that is, |= F [G[T ]]. Statement (13), (7) and (6) imply (8), that is |= F [H], which concludes the proof. t
u
The essential relationships between particular, parametric, general and reproductive solutions, as well as an alternate characterization of reproductive solution
implied by these, are gathered in the following proposition:

Reproductive Solutions as Most General Solutions

21

Proposition 26 (Relationships Between the Solution Types). Let G =
G[t] be a sequence of formulas. Then:
(i) G is a parametric solution of the PSP F [p]:t if and only if CLEAN(G)
and G is a particular solution of the SP F [p].
(ii) If G is a parametric solution of the PSP F [p]:t and T is sequence of formulas such that SUBST(T , t, G), SUBST(G[T ], p, F ), then G[T ] is a particular
solution of the SP F [p].
(iii) A general solution of a PSP is also a parametric solution of that PSP.
(iv) If G is a general solution of the PSP F [p]:t and H is a particular solution
of the SP F [p] such that SUBST(H, t, G), then there exists a sequence T of
formulas such that SUBST(T , t, G), SUBST(G[T ], p, F ) and
H ≡ G[T ].
(v) A reproductive solution of a RSP is also a general solution of that RSP.
(vi) If G is a parametric solution of the RSP F [p]:t, then for all sequences H
of formulas such that SUBST(H, t, G) and SUBST(H, p, F ) it holds that if
H ≡ G[H],
then
|= F [H].
(vii) G is a reproductive solution of the RSP F [p]:t if and only if
1. G is a parametric solution of F [p]:t and
2. For all sequences H of formulas such that SUBST(H, t, G) and
SUBST(H, p, F ) it holds that
|= F [H]
if and only if
H ≡ G[H].
Before we come to the proof of Prop. 26, let us observe that the conclusion
of Prop. 26.vi is item (2.) of the definiens of reproductive solution (Def. 24.iii)
after replacing the if-then implication there by its converse, and that Prop. 26.vii
characterizes reproductive solution like its definition (Def. 24.iii), except that the
definiens is strengthened by turning the if-then implication in item (2.) into an
equivalence.
Proof (Proposition 26).
(26.i) Left-to-right: Let q be a sequence of fresh predicates that matches t and
assume that G[t] is a parametric solution of F [p]:t. Hence SUBST(G, p, F ) and
|= F [G[q]], which implies |= F [G]. Thus G is a particular solution of F [p]. Note
that this direction of the proposition requires the availability of fresh predicates

22

Section 6

in the vocabulary. Right-to-left: Can be derived in the following steps explained
below:
(1) G[t] is a particular solution of F [p].
(2) CLEAN(G)
(3) SUBST(G, p, F )
(4) |= F [G].
(5) SUBST(T , t, G).
(6) SUBST(G[T ], p, F ).
(7) SUBST(T , t, F [G]).
(8) |= ∀t F [G].
(9) |= F [G[T ]].
(10) G is a parametric solution of F [p]:t.
Step (1) and (2), where t is some sequence of distinct predicates such that
(free(F ) ∪ p) ∩ t = ∅, form the left side of the proposition. Steps (3) and (4)
follow from (1) and the characteristics of particular solution. Let T be a sequence
of formulas such that (5) and (6) hold, conditions on the left side of Prop. 25.
Step (7) follows from (5) and (6). Step (8) follows from (4). Step (9) follows from
(7) and (8) by Prop. 2.ii. Finally, step (10), the right side of the proposition,
follows from Prop. 25 with (9), (2) and (3).
(26.ii) The left side of the proposition includes SUBST(G[T ], p, F ) and, by
Prop. 25, implies |= F [G[T ]], from which the right side follows.
(26.iii) Immediate from the definition of general solution (Def. 24.ii).
(26.iv) The left side of the proposition implies SUBST(H, t, G),
SUBST(H, p, F ) and |= F [H]. The right side then follows from the definition
of general solution (Def. 24.ii).
(26.v) By definition, a reproductive solution is also a parametric solution.
Let G be a reproductive solution of F [p]:t. Let COND stand for the following
conjunction of three statements:
SUBST(H, t, G), SUBST(H, p, F ) and |= F [H].
From the definition of reproductive solution it immediately follows that for all
sequences H of formulas such that COND it holds that H ≡ G[H]. From this
it follows that for all sequences H of formulas such that COND it holds that
SUBST(H, t, G), SUBST(G[H], p, F ) and H ≡ G[H], which can be derived as
follows: The first of the statements on the right, SUBST(H, t, G), is included
directly in the left side, that is, COND. The second one, SUBST(G[H], p, F ), follows from SUBST(H, t, G) and SUBST(H, p, F ) that are in COND together with
SUBST(G, p, F ), which holds since G is a parametric solution. The above implication also holds if H on its right side is replaced by a supposedly existing T .
It then forms the remaining requirement to show that G is a general solution:
For all sequences H of formulas such that COND there exists a sequence T of
formulas such that SUBST(T , t, G), SUBST(G[T ], p, F ) and H ≡ G[T ].

Reproductive Solutions as Most General Solutions

23

(26.vi) Can be shown in the following steps, explained below:
(1)
(2)
(3)
(4)
(5)
(6)
(7)

SUBST(G, p, F ).
SUBST(H, t, G).
SUBST(H, p, F ).
H ≡ G[H].
SUBST(G[H], p, F ).
F [G[H]] |= ⊥.
F [H] |= ⊥.

Assume that G is a parametric solution of the RSP F [p]:t, which implies (1).
Let H be a sequence of formulas such that (2) and (3), the preconditions of the
converse of (as well as the unmodified) item (2.) in the definition of reproductive
solution (Def. 24.iii), hold. Further assume (4), the right side of item (2.). We
prove the proposition by deriving the left side of item (2.). Step (5) follows
from (1), (2) and (3). Step (6) follows from (2) and (5) by Prop. 25 since G is a
parametric solution. Finally, step (7), the left side of item (2.), follows from (6)
and (4) with (3) and (5).
(26.vii) Follows from Prop. 26.vi.
t
u
Rudeanu [30] notes that the concept of reproductive solution seems to have
been introduced by Schröder [34], while the term reproductive is due to Löwenheim [25]. Schröder calls the additional requirement that a reproductive solution
must satisfy in comparison with general solution Adventivforderung (adventitious requirement) and discusses it at length in [34, vol. 3, § 12], describing it
with reproduzirt. [34, vol. 3, p. 171].
6.2

The Rigorous Solution

From any given particular solution G, a reproductive solution can be constructed, called here, following Schröder’s terminology [34, vol. 3, § 12], the
rigorous solution associated with G. In the framework of Boolean algebra, the
analogous construction is [30, Theorem 2.11].
Proposition 27 (The Rigorous Solution). Let F [p]:t = t1 . . . tn be a RSP.
For i ∈ {1, . . . , n} let xi stand for x1 . . . xarity(ti ) . Assume free(F ) ∩ X = ∅,
SUBST(t1 (x1 ) . . . tn (xn ), p, F ) and SUBST(F [t], p, F ). If G = G1 . . . Gn is a
particular solution of that RSP , then the sequence R = R1 . . . Rn of formulas
defined as follows is a reproductive solution of that RSP:
Ri is the clean variant of (Gi (x) ∧ ¬F [t]) ∨ (ti (xi ) ∧ F [t]).
In the specification of Ri the formula Gi is written as Gi (x) to indicate that members of X may occur there literally without being replaced. In the unsatisfiabilitybased setting, the Ri would be characterized as the clean variant of
(Gi (x) ∧ F [t]) ∨ (ti (xi ) ∧ ¬F [t]).

(v)

24

Section 6

The proof of this proposition is based on the following lemma, a predicate logic
analog to [30, Lemma 2.3] for the special case n = 1, which is sufficient to prove
Prop. 27: The effect of the lemma for arbitrary n is achieved by an application
of Prop. 27 within an induction.
Proposition 28 (Subformula Distribution Lemma). Let p be a predicate
(with arbitrary arity ≥ 0), let F [p] be a formula and let V, W, A be formulas
such that SUBST(V, p, F ), SUBST(W, p, F ), SUBST(A, p, F ) and, in addition,
free(A) ∩ X = ∅. It then holds that
F [(A ∧ V ) ∨ (¬A ∧ W )] ≡ (A ∧ F [V ]) ∨ (¬A ∧ F [W ]).
Proof. Assume the preconditions of the proposition. It follows that SUBST((A ∧
V ) ∨ (¬A ∧ W ), p, F ). Making use of Prop. 2.i, the conclusion of the proposition
can be then be shown in the following steps:
Left side
≡ ∃p (F [p] ∧ (p ⇔ ((A ∧ V ) ∨ (¬A ∧ W ))))
≡ (A ∧ ∃p (F [p] ∧ (p ⇔ ((A ∧ V ) ∨ (¬A ∧ W ))))) ∨
(¬A ∧ ∃p (F [p] ∧ (p ⇔ ((A ∧ V ) ∨ (¬A ∧ W )))))
≡ (A ∧ ∃p (F [p] ∧ (p ⇔ ((> ∧ V ) ∨ (⊥ ∧ W ))))) ∨
(¬A ∧ ∃p (F [p] ∧ (p ⇔ ((⊥ ∧ V ) ∨ (> ∧ W )))))
≡ (A ∧ ∃p (F [p] ∧ (p ⇔ V ))) ∨ (¬A ∧ ∃p (F [p] ∧ (p ⇔ W )))
≡ Right side.
t
u
The preconditions in Prop. 28 permit that x1 , . . . , xarity(p) may occur free in V
and W , whereas in A no member of X is allowed to occur free. We are now ready
to prove Prop. 27:
Proof (Proposition 27). By item (1.) of the definition of reproductive solution
(Def. 24.iii), R[t] = R1 [t] . . . Rn [t] is required to be a parametric solution for
which by Prop. 25 three properties have to be shown: The first one, CLEAN(R),
is immediate since each member of R is the clean variant of some formula. The
second one, SUBST(R, p, F ), is easy to derive from the preconditions and the
definition of R. The third one is an implication that can be shown in the following
steps, explained below:
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)

SUBST(T , t, R).
SUBST(R[T ], p, F ).
SUBST(G, p, F ).
|= F [G].
¬F [T ] ∧ ¬F [R[T ]] |= ¬F [G].
F [T ] ∧ ¬F [R[T ]] |= ¬F [T ].
F [G] |= F [R[T ]].
|= F [R[T ]].

Let T be a sequence of formulas such that statements (1) and (2), which are on
the left side of the implication to show, do hold. We derive the right side of the

Reproductive Solutions as Most General Solutions

25

implication, that is |= F [R[T ]]. Steps (3) and (4) hold since G is a particular solution. Steps (5) and (6) can be shown by induction based on the equivalences (9)
and (10), respectively, below, which hold for all i ∈ {0, . . . , n − 1} and follow
from Prop. 28:
(9)

¬F [G1 . . . Gi Ri+1 [T ] . . . Rn [T ]]
≡ ¬F [G1 . . . Gi ((Gi+1 ∧ ¬F [T ]) ∨ (Ti+1 ∧ F [T ])) Ri+2 [T ] . . . Rn [T ]]
≡ (¬F [T ] ∧ ¬F [G1 . . . Gi+1 Ri+2 [T ] . . . Rn [T ]]) ∨
(F [T ] ∧ ¬F [G1 . . . Gi Ti+1 Ri+2 [T ] . . . Rn [T ]]).

(10)

¬F [T1 . . . Ti Ri+1 [T ] . . . Rn [T ]]
≡ ¬F [T1 . . . Ti ((Gi+1 ∧ ¬F [T ]) ∨ (Ti+1 ∧ F [T ])) Ri+2 [T ] . . . Rn [T ]]
≡ (¬F [T ] ∧ ¬F [T1 . . . Ti Gi+1 Ri+2 [T ] . . . Rn [T ]]) ∨
(F [T ] ∧ F [T1 . . . Ti+1 Ri+2 [T ] . . . Rn [T ]]).

The required preconditions of Prop. 28 are justified there as follows, where F 0
stands for F after the substitutions indicated in (9) or (10), that is, the formula
matched with the left side of Prop. 28:
– SUBST(Gi+1 , pi+1 , ¬F 0 ): Follows from (3).
– SUBST(Ti+1 , pi+1 , ¬F 0 ): Follows from (1) and (2).
– SUBST(F [T ], pi+1 , ¬F 0 ): Follows from (1), (2) and the precondition
SUBST(F [t], p, F ).
– free(F [T ]) ∩ X = ∅:
Follows from (1), (2) and the precondition
free(F ) ∩ X = ∅.
Step (7) follows from (6) and (5) and, finally, step (8) follows from (7) and (4).
Item (2.) of the definition of reproductive solution follows since for all sequences of formulas H such that SUBST(H, t, R) and SUBST(H, p, F ) (note
that SUBST(H, t, G) is implied by SUBST(H, t, R)) it holds that if |= F [H],
then H ≡ R[H], or, equivalently, but more explicated, it holds for all i ∈
{1, . . . , n} that
Ri [H]
≡ (Gi [H] ∧ ¬F [H]) ∨ (Hi ∧ F [H])
≡ (Gi [H] ∧ ⊥) ∨ (Hi ∧ >)
≡ Hi .
t
u
The algebraic version [30, Theorem 2.11] is attributed there and in most of
the later literature to Löwenheim [24,25], thus known as Löwenheim’s theorem
for Boolean equations. However, at least the construction for unary problems
appears to be in essence Schröder’s rigorose Lösung [34, vol. 3, § 12]. (Löwenheim
remarks in [24] that the rigorose Lösung can be derived as a special case of his
theorem.) Behmann comments that Schröder’s discussion of rigorose Lösung
starts only in a late chapter of Algebra der Logik mainly for the reason that only
then suitable notation was available [6, Footnotes on p. 22f]. Schröder [34, vol. 3,
p. 168] explains his term rigoros as adaption of à la rigueur, that is, if need be,
because he does not consider the rigorous solution as a satisfying representation

26

Section 6

of all particular solutions. He notes that to detect all particular solutions on the
basis of the rigorose Lösung, one would have to test all possible formulas T as
parameter value. As remarked in [27, p. 382], Löwenheim’s theorem has been
rediscovered many times, for example in [26].
6.3

Schröder’s Reproductive Interpolant

For 1-RSPs of the form
((A ⇒ p) ∧ (p ⇒ B))[p]:t,

(vi)

A ∨ (B ∧ t(x)),

(vii)

the formula
where xs = x1 . . . xarity(p) , is a reproductive solution. This construction has been
shown by Schröder and is also discussed in [6]. For the notion of solution based on
unsatisfiability instead of validity, the analogous construction applies to 1-RSPs
of the form
((A ∧ p) ∨ (B ∧ ¬p))[p]:t
(viii)
and yields
B ∨ (¬A ∧ t).

(ix)

We call the solution interpolant because with the validity-based notion of solution assumed here the unknown p, and thus also the solution, is “between” A and
B, that is, implied by A and implying B. The following proposition makes the
construction precise and shows its justification. The proposition is an adaption
of [30, Lemma 2.2], where [34, vol. 1, § 21] is given as source.
Proposition 29 (Schröder’s Reproductive Interpolant). Let
(F = ∀y (A(y) → p(y)) ∧ ∀y (p(y) → B(y)))[p]:t,
where y is a sequence with the arity of p as length of distinct individual symbols not in X , be a 1-RSP that has a solution. Let x = x1 . . . xarity(p) . Assume
SUBST(A(x), p, F ), SUBST(B(x), p, F ) and SUBST(t(x), p, F ). Then the clean
variant of following formula is a reproductive solution of that 1-RSP:
A(x) ∨ (B(x) ∧ t(x)).
That p does not occur free in A or in B is ensured by the preconditions
SUBST(A, p, F ) and SUBST(B, p, F ). The symbols y for the quantified variables
indicate that these are independent from the special meaning of the symbols
in X .
Proof (Proposition 29). Assume the preconditions of the proposition and let
G[t] stand for the clean variant of A(x) ∨ (B(x) ∧ t(x)). By item (1.) of the
definition of reproductive solution (Def. 24.iii), G is required to be a parametric
solution for which by Prop. 25 three properties have to be shown: The first one,

Reproductive Solutions as Most General Solutions

27

CLEAN(G), is immediate since G is a clean variant of some formula. The second
one, SUBST(G, p, F ), easily follows from the preconditions. The third one is an
implication that can be shown in the following steps, explained below:
SUBST(A(x) ∨ (B(x) ∧ T (x)), p, F ).
|= ∃p (∀y (A(y) → p(y)) ∧ ∀y (p(y) → B(y))).
|= ∀y (A(y) → B(y)).
|= ∀y (A(y) → (A(y) ∨ (B(y) ∧ T (y)))) ∧
∀y ((A(y) ∨ (B(y) ∧ T (y))) → B(y)).
(4) |= F [A(x) ∨ (B(x) ∧ T (x))].

(1)
(2)
(3)
(4)

Let T (x) be a formula such that statement (1), which is on the left side of the
implication to show, does hold. We derive the right side of the implication, that is,
|= F [B(x) ∨ (A(x) ∧ T (x))]: Step (2) follows with Prop. 15 from the precondition
that the considered 1-RSP has a solution. Step (3) follows from (2) by secondorder quantifier elimination, for example with Ackermann’s lemma (Prop. 3).
The formulas to the right of |= in both statements are equivalent. Step (4) follows
from (3) by logic. Justified by (1), we can express (4) as (5), the right side of the
implication to show. Item (2.) of the definition of reproductive solution follows
since for all formulas H(x) such that SUBST(H(x), t, G), SUBST(H(x), p, F ),
it holds that |= F [H(x)] implies H(x) ≡ G[H(x)], which can be derived in the
following steps:
iff
iff
implies
implies
iff

|= F [H(x)]
|= ∀y (A(y) → H(y)) ∧ ∀y (H(y) → B(y))
|= ∀y (H(y) ↔ (A(y) ∨ H(y))) and
|= ∀y (H(y) ↔ (B(y) ∧ H(y)))
H(x) ≡ A(x) ∨ H(x) and H(x) ≡ B(x) ∧ H(x)
H(x) ≡ A(x) ∨ (B(x) ∧ H(x))
H(x) ≡ G[H(x)].
t
u

As shown by Schröder, the (clean variants of the) following two formulas are
further reproductive solutions in the setting of Prop. 29:
B(x) ∧ (A(x) ∨ t(x))

(x)

(A(x) ∧ t(x)) ∨ (B(x) ∧ ¬t(x)).

(xi)

and
These two formulas and the solution according to Prop. 29 are all equivalent
under the assumption that a solution exists, that is, |= ∃p F , which, by secondorder quantifier elimination, is equivalent to
|= ∀y (A(y) → B(y)).

(xii)

Any 1-RSP F [p]:t where F is a propositional formula or, more generally,
where the unknown p is nullary, can be brought into the form matching Prop. 29

28

Section 6

by systematically renaming bound symbols and rewriting F [p] with the equivalence
F [p] ≡ (¬F [⊥] → p) ∧ (p → F [>]).
(xiii)
For the notion of solution based on unsatisfiability, the required form can be
obtained with the Shannon expansion
F [p] ≡ (F [>] ∧ p) ∨ (F [⊥] ∧ ¬p).
6.4

(xiv)

From Unary to n-ary Reproductive Solutions

If the solution of a RSP is composed as suggested by Prop. 10 from reproductive
solutions of unary solution problems, then it is itself a reproductive solution:
Proposition 30 (Composing a Reproductive Solution from Unary Reproductive Solutions). Let F [p = p1 . . . pn ]:t = t1 . . . tn be a RSP. If G[t] =
G1 [t] . . . Gn [t] is a sequence of formulas such that for all i ∈ {1, . . . , n} it holds
that Gi is a reproductive solution of the 1-RSP
(∃pi+1 . . . ∃pn F [G1 . . . Gi−1 pi . . . pn ])[pi ]:ti
and free(Gi ) ∩ (p ∪ ti+1 . . . tn ) = ∅, then G is a reproductive solution of the
considered RSP F [p]:t.
Proof. Assume the preconditions and the left side of the proposition. We show
the two items of the definition of reproductive solution (Def. 24.iii) for G. Item (1.),
that is, G is a parametric solution of F [p]:t, can be derived as follows: Each Gi ,
for i ∈ {1, . . . , n}, is a reproductive solution of the associated 1-RSP. Hence, by
Prop. 26 it is a general, hence parametric, hence particular solution. By Prop. 10
it follows that G is a particular solution of F [p]. By Prop. 26.i it is then also a
parametric solution of F [p]:t. Item (2.) of the definition of reproductive solution
can be shown as follows: First we note the following statement that was given
as precondition:
(1)

For i ∈ {1, . . . , n} it holds that free(Gi ) ∩ ti+1 . . . tn = ∅.

For i ∈ {1, . . . , n} let
Fi [pi t] def
= ∃pi+1 . . . ∃pn F [G1 [t] . . . Gi−1 [t]pi . . . pn ],
that is, Fi is the formula of the 1-SP of which Gi is a reproductive solution. By
the definition of reproductive solution and the left side of the proposition it holds
for all formulas Hi that if
(2) SUBST(Hi , ti , Gi )
SUBST(Hi , pi , Fi [pi t]), and
|= Fi [Hi t],
then
(3) Hi ≡ Gi [t1 . . . ti−1 Hi ti+1 . . . tn ].

Approaching Constructive Solution Techniques

29

From this and (1) it follows that all for all sequences of formulas H1 . . . Hi it
holds that if
(4) SUBST(Hi , ti , Gi )
SUBST(Hi , pi , Fi [pi H1 . . . Hi−1 ti . . . tn ]), and
|= Fi [Hi H1 . . . Hi−1 ti . . . tn ],
then
(5) Hi ≡ Gi [H1 . . . Hi ti+1 . . . tn ].
Now let H ≡ H1 . . . Hn be a sequence of formulas such that
(6) SUBST(H, t, G)
SUBST(H, p, F ), and
|= F [H].
We prove the item (2) of Def. 24.iii by showing H ≡ G[H], which is equivalent to the statement that for all i ∈ {1, . . . , n} it holds that Hi ≡ Gi [H],
and, because of (1), to the statement that for all i ∈ {1, . . . , n} it holds that
Hi ≡ Gi [H1 . . . Hi ti+1 . . . tn ], which matches (5). We thus can prove H ≡
G[H] by showing that (4), which implies (5), holds for all i ∈ {1, . . . , n}.
The substitutivity conditions in (4) follow from the substitutivity conditions
in (6). The remaining condition |= Fi [Hi H1 . . . Hi−1 ti . . . tn ] can be proven by
induction. As induction hypothesis assume that for all j ∈ {1, . . . i − 1} it
holds that Hj ≡ Gj [H]. From |= F [H] in (6) it follows by Prop. 2.ii that
|= ∃pi+1 . . . ∃pn F [H1 . . . Hi pi+1 . . . pn ]. With the induction hypothesis it follows
that
|= ∃pi+1 . . . ∃pn F [G1 [H] . . . Gi−1 [H]Hi pi+1 . . . pn ],
which, given the substitutivity conditions of (6) and SUBST(G, p, F ), which
holds since G is a parametric solution, can be expressed as
|= Fi [Hi H1 . . . Hi−1 ti . . . tn ],
such that all conditions of (4) are satisfied and Hi ≡ Gi [H] can be concluded.
t
u
This suggests to compute reproductive solutions of propositional formulas for
a n-ary SP by constructing Schröder interpolants for 1-SPs. Since second-order
quantifier elimination on propositional formulas succeeds in general, the construction of the Schröder interpolant can there be performed on the basis of
formulas that are just propositional, without second-order quantifiers.

7

Approaching Constructive Solution Techniques

On the basis of first-order logic it seems that so far there is no general constructive method for the computation of solutions. We discuss various special
cases where a construction is possible. Some of these relate to applications of
Craig interpolation. Recent work by Eberhard, Hetzl and Weller [16] shows a constructive method for quantifier-free first-order formulas. A generalization of their
technique to relational monadic formulas is shown, which, however, produces solutions that would be acceptable only under a relaxed notion of substitutibility.

30
7.1

Section 7

Background: Craig Interpolation, Definability and Independence

By Craig’s interpolation theorem [13], if F and G are first-order formulas such
that F |= G, then there exists an a Craig interpolant of F and G, that is, a
first-order formula H such that
free(H) ⊆ free(F ) ∩ free(G)

(xv)

F |= H |= G.

(xvi)

and
Craig interpolants can be constructed from proofs of |= F → G, as, for example, shown for tableaux in [36,17]. Lyndon’s interpolation theorem strengthens
Craig’s theorem by considering in addition that predicates in the interpolant H
occur only in polarities in which they occur in both side formulas, F and G. In
fact, practical methods for the construction of interpolants from proofs typically
compute such Craig-Lyndon interpolants.
One of the many applications of Craig interpolation is the construction of
a definiens for a given predicate: Let F [pq1 . . . qk ] be a first-order formula such
that free(F ) ∩ X = ∅ and pq1 , . . . qk is a sequence of distinct predicates and let
x stand for x1 . . . xarity(p) . Then p is definable in terms of (free(F ) \ {q1 , . . . , qk })
within F , that is, there exists a first-order formula G such that
free(G) ⊆ (free(F ) \ {p, q1 , . . . qk }) ∪ x

(xvii)

F |= p ⇔ G,

(xviii)

∃p∃q1 . . . ∃qk (F ∧ p(x)) |= ¬∃p∃q1 . . . ∃qk (F ∧ ¬p(x)).

(xix)

and
if and only if

That entailment holds if and only if the following first-order formula is valid:
F ∧ p(x) → ¬(F [p0 q10 . . . qk0 ] ∧ ¬p0 (x)),

(xx)

where p0 q 0 . . . qk0 is a sequence of fresh predicates that matches pq . . . qk . The
definientia G of p with the stated characteristics are exactly the Craig interpolants of the two sides of that implication. Substitutibility SUBST(G, p, F ) can
be ensured by presupposing CLEAN(F ) and that no members of X are bound
by a quantifier occurrence in F .
Another application of Craig interpolation concerns the independence of formulas from given predicates: Second-order quantification allows to express that
a formula F [p] is semantically independent from the set of the predicates in p
as
∃p F ≡ F,
(xxi)
which is equivalent to ∃p F |= F , and thus, if q is a sequence of fresh predicates
that matches p, also equivalent to
|= F [q] → F.

(xxii)

31

Approaching Constructive Solution Techniques

As observed in [29], any interpolant of F [q] and F is then equivalent to F but its
free symbols do not contain members of p, that is, it is syntactically independent
of p. Thus, for a given first-order formula semantic independence from a set of
predicates can be expressed as first-order validity and, if it holds, an equivalent
formula that is also syntactically independent can be constructed by Craig interpolation. With Craig-Lyndon interpolation this technique can be generalized
to take also polarity into account, based on encoding of polarity sensitive independence as shown here for negative polarity: That F [p] is independent from
predicate p in negative polarity but may well depend on p in positive polarity
can be expressed as
∃q (F [q] ∧ ∀x (q(x) → p(x))),
(xxiii)
where x = x1 . . . xarity(p) and q is a fresh predicate with the same arity as p.
7.2

Cases Related to Definability and Interpolation

The following list shows cases where for an n-ary SP F [p = p1 . . . pn ] with firstorder F and which has a solution a particular solution can be constructed. Each
of the properties that characterize these cases is “semantic” in the sense that if
it holds for F , then it also holds for any first-order formula equivalent to F . In
addition, each property is at least “semi-decidable”, that is, the set of first-order
formulas with the property is recursively enumerable. Actually in the considered
cases, for each property a first-order formula can be constructed from F that is
valid if and only if F has the property. For two of the listed cases, (3.) and (5.),
the characterizing property implies the existence of a solution.
1. Each unknown occurs free in F only with a single polarity. A sequence of
> and ⊥, depending on whether the respective unknown occurs positively
or negatively, is then a solution. That F is semantically independent of unknowns in certain polarities, that is, is equivalent to a formula in which the
unknowns do not occur in these polarities, can be expressed as first-order
validity and a corresponding formula that is syntactically independent can
be constructed by Craig-Lyndon interpolation.
2. Each unknown is definable in the formula. A sequence of definientia, which
can be constructed with Craig interpolation, is then a solution. Rationale:
Let G1 . . . Gn be definientia of p1 . . . pn , respectively, in F . Under the assumption that there exists a solution H of F [p] it holds that
> |= F [H] |= ∃p F [p] ≡ ∃p (F [p] ∧

n
^

(pi ⇔ Gi )) ≡ F [G].

i=1

3. Each unknown is definable in the negated formula. The sequence of negated
definientia, which can be constructed with Craig interpolation, is then a
solution. Rationale: It holds in general that p ⇔ G |= p 6⇔ ¬G. Hence,
if G1 . . . Gn are definientia of p1 . . . pn , respectively, in ¬F , then ¬F |=

32

Section 7

Vn

i=1 (pi

⇔ Gi ) |=

Wn

i=1 (pi

⇔ Gi ) ≡
n
^

Wn

i=1 (pi

6⇔ ¬Gi ). Thus

(pi ⇔ ¬Gi ) |= F,

i=1

matching the characterization of solution in Prop. 9.
4. Each unknown is nullary. This specializes case (3.): If a solution exists, then a
nullary unknown is definable in the negated formula: For nullary predicates p
it holds in general that
p ⇔ ¬G ≡ p 6⇔ G.
Thus p ⇔ ¬G |= F (which matches Prop. 9) holds if and only if ¬F |= p ⇔
G.
5. Each unknown has a ground instance that is definable in the negated formula.
The sequence of negated definientia is a solution. If p1 (t1 ) . . . pn (tn ) are the
definable ground instances, then optionally in each solution component Gi ,
under the assumption CLEAN(Gi ), each member tij of ti = ti1 . . . tiarity(pi )
can be replaced by xj . The construction of the definientia can be performed
with Craig interpolation, as described above for predicate definientia, except
that an instance p(t) takes the place of p(x). The difficulty is to find suitable
instantiations t1 . . . tn . A way to avoid guessing might be to let the formula
whose proof serves as basis for interpolant extraction follow the schema
∃y (F ∧ p(y) → ¬(F [p0 ] ∧ ¬p0 (y))),
where y = y1 . . . yarity(p) and take the instantiation of y found by the prover. If
the proof involves different instantiations of y it has to be rejected. Rationale:
Similar to the case (4.) since for ground atoms p(t) it holds in general that
p(t) ↔ G ≡ ¬(p(t) ↔ ¬G).
These cases suggest to compute particular solutions based on Prop. 10 by computing solutions for 1-SPs for each unknown, which is inspected for matching the
listed cases or other types of solvable cases, for example the forms required by
Schröder’s interpolant or by Ackermann’s lemma. If that fails for an unknown,
an attempt with the unknowns re-ordered is made. For propositional problems,
an interpolating QBF solver would be a candidate to compute solutions. Encodings of QBF into predicate logic, e.g., [35], could possibly be applied for general
first-order formulas with nullary unknowns.
7.3

The EHW-Combination of ELIM-Witnesses for Disjuncts

Eberhard, Hetzl and Weller show in [16] that determining the existence of a
Boolean unifier (or, in, our terms, particular solution) for quantifier-free predicate logic is ΠP
2 -complete, as for propositional logic [2]. Their proof rests on the
existence of an EXPTIME function wit from quantifier-free formulas to quantifierfree formulas such that ∃pF [p] ≡ F [wit(F [p])]. The specification of wit(F [p])

33

Approaching Constructive Solution Techniques

is presented there as a variant of the DLS algorithm [15,11] for second-order
quantifier elimination: The input is converted to disjunctive normal form and
a specialization of Ackermann’s lemma is applied separately to each disjunct.
The results for each disjunct are then combined in a specific way to yield the
overall witness formula. The following proposition states a generalized variant
of this technique that is applicable also to other classes of inputs, beyond the
quantifier-free case.
Proposition
Wn31 (EHW-Combination of ELIM-Witnesses for Disjuncts).
Let F [p] = i=1 Fi be a formula and let G1 , . . . , Gn be formulas such that for
i ∈ {1, . . . n} it holds that SUBST(Gi , pi , Fi ) and ∃p Fi [p] ≡ Fi [Gi ]. Assume
that there are no free occurrences of X in F and, w.l.o.g, that no members of
free(F ) ∪ X are bound by a quantifier occurrence in F . Let
G(x) def
=

n
^

((

i=1

i−1
^

¬Fj [Gj ]) ∧ Fi [Gi ] → Gi (x)).

j=1

Then it holds that SUBST(G, p, F ) and ∃p F [p] ≡ F [G].
Formulas G and Gi are written as Gi (x) and G(x) where they occur as formula
constituents instead of substituents to emphasize that x may occur free in them.
Proof (Proposition 31). This proof is an adaption of the proof of Theorem 2 in
[16]. We write here I is a model of F symbolically as I |= F . That SUBST(G, p, F )
follows from the preconditions of the proposition and the construction of G. The
right-to-left direction of the stated equivalence, that is,
n
_
i=1

Fi [G] |= ∃p

n
_

Fi [p],

i=1

then follows from Prop. 2.ii. The left-to-right direction of the equivalence can be
show in the following steps, explained below.
Wn
(1) I |= ∃p
Wn i=1 Fi [p].
(2) I |= Wi=1 ∃p Fi [p].
n
(3) I |= i=1 Fi [Gi ].
Vk−1
(4) I |= ( j=1 ¬Fj [Gj ]) ∧ Fk [Gk ].
(5) I |= ∀x (G(x) ↔ Gk (x)).
(6) I |= F
Wkn[G].
(7) I |= i=1 Fi [G].
Let I be an interpretation such that (1) holds. Step (2) is equivalent to (1).
Assume the precondition
of the proposition that for all i ∈ {1, . . . n} it holds
Wn
that ∃p Fi [p] ≡ i=1 Fi [Gi ]. Step (3) follows from this and (1). By (3) there
is a smallest member k of {1, . . . , n} such that I |= Fk [Gk ]. This implies (4).
The left-to-right direction of the equivalence in (5) follows since if I |= G(x)
then by (4) and the definition of G(x) it is immediate that I |= Gk (x). The

34

Section 7

right-to-left direction of the equivalence in (5) can be shown as follows: Assume
I |= Gk (x). Then I is a model of the kth conjunct of G(x) since Gk (x) is in the
conclusion of that conjunct, and I is a model of each jth conjunct of G(x) with
j 6= k, because the antecedent of such a conjunct contradicts with (4). Step (6)
follows from (4) and (5). Step (7) follows from (6).
t
u
The following proposition is another variant of the EHW-combination of
witnesses for disjuncts. It can be proven similarly to Prop. 31.
Proposition 32 (Alternate Variant of EHW-Combination). Let F [p] be
a 1-SP and let G1 , . . . , Gn be formulas such
Wn that for i ∈ {1, . . . , n} it holds that
SUBST(Gi , p, F ) and such that ∃p F ≡ i=1 F [Gi ]. Assume that there are no
free occurrences of {xi | i ≥ 1} in F and, w.l.o.g, that no members of free(F ) ∪ x
are bound in by a quantifier occurrence in F . Let
G def
=

n
^
i=1

((

i−1
^

¬F [Gj ]) ∧ F [Gi ] → Gi ).

j=1

Then SUBST(G, p, F ) and ∃p F ≡ F [G].
Proposition 32 is also applicable to 1-SPs of the form handled by Prop. 31,
but for this case leads to a more clumsy result G: Assume the additional
preWn
condition
that
for
all
j
∈
{1,
.
.
.
,
n}
it
holds
that
SUBST(G
,
p,
F
).
Let
j
i=1 i
Wn
F [p] def
F
[p].
Then
∃pF
[p]
≡
F
[G
]
∨
.
.
.
∨
F
[G
]
≡
F
[G
]
∨
.
.
.
∨
F
[G
= i=1 i
1
1
n
n
1
n ].
7.4

Relational Monadic Formulas and Relaxed Substitutibility

The class of relational monadic formulas with equality, called here MON= , is the
class of first-order formulas with equality, with unary predicates and with individual constants but no other functions (without equality it is the Löwenheim
class). It is decidable and permits second-order quantifier elimination, that is,
each formula in MON= extended by predicate quantification is equivalent to a
formula in MON= . As shown in [39] it has interesting relationships with ALC.
Behmann [5] gave a decision method for MON= that performs second-order
quantifier elimination by equivalence preserving formula rewriting [39,38]. Almost three decades later he published an adaption of these techniques to the
solution problem for Klassenlogik [6,7], which in essence seems to be MON= .
It still remains open to assess this and apparently related works by Löwenheim
[25].
Under a relaxed notion of substitutibility the construction of ELIM-witnesses
for MON= is possible by joining Behmann’s rewriting technique [5] with the
EHW-combination (Prop. 31). Let F [p] be a MON= formula and let p be a
unary predicate. Assume that free(F ) ∩ X = ∅. The reconstruction of Behmann’s
normalization shown in the proofs of LemmaW14 and Lemma 16 of [38] can be
n
slightly modified to construct a formula F 0 = i=1 Fi00 that is equivalent to ∃p F
and such that each Fi00 is of the form
Fi00 = Ci ∧∃ui (Di (ui )∧∃p (∀y (Ai (ui y) → p(y))∧∀y (p(y) → Bi (ui y)))), (xxiv)

35

Solutions in Restricted Vocabularies

where ui is a sequence of individual symbols such that ui ∩ free(Ci ) = ∅, predicate p has only the two indicated occurrences and free(Fi0 ) ⊆ free(∃p F ). Let
Fi000 [p] = Ci ∧ Di (ui ) ∧ ∀y (Ai (ui y) → p(y)) ∧ ∀y (p(y) → Bi (ui y)).

(xxv)

Then Fi00 ≡ ∃ui ∃p Fi000 ≡ ∃ui Fi00 [A(ui x1 )], where the last equivalence follows
from Ackermann’s lemma (Prop. 3). It holds that SUBST(Fi00 , p, A(ui x1 )) but,
since the quantified symbols u may occur in A(ui x1 ), the substitutibility condition SUBST(∃u Fi00 , p, A(ui x1 )) does not hold in general. The variables ui can
be gathered to a single global prefix u (assuming w.l.o.g. that noneWof them ocn
curs free in any of the Ci ) such that F ≡ ∃u F 0000 [p] where F 0000 = i=1 Fi000 . By
Prop. 31 we can construct a formula G(u) such that SUBST(G(u), p, F 0000 ) and
∃p F 0000 [p] ≡ F 0000 [G(u)]. This implies ∃p F [p] ≡ F [G(u)]. However, substitutibility of G(u) holds only with respect to F 0000 , while SUBST(G(u), p, F ) does not
hold in general. Thus, under a relaxed notion of substitutibility that permits the
existentially quantified u in the witness the EHW-combination can be applied
to construct witnesses for MON= formulas.

8

Solutions in Restricted Vocabularies

8.1

An Example: Synthesizing Definitional Equivalence

In some applications it is useful to restrict the allowed vocabulary of the solution
components. Consider for example the task of finding a mapping that establishes
a definitional equivalence [20] between two formulas A and B where the predicates occurring free in A are in a set VA = {a1 , . . . , an } and those occurring in
B are in another set VB = {b1 , . . . , bm }, disjoint with VA . The objective is then
to find a solution GH of the SP F [pq] where G = G1 . . . Gm , H = H1 . . . Hn ,
p = p1 . . . pm , q = q1 . . . qn ,
F = (A ∧

m
^
i=1

∀y i (bi (y i ) ↔ pi (y i ))) ↔ (B ∧

n
^

∀z i (ai (z i ) ↔ qi (z i ))), (xxvi)

i=1

y i = y1 . . . yarity(bi ) , z i = z1 . . . zarity(ai ) , and the restriction is satisfied that all
predicates in free(G) are in VA and all predicates in free(H) are in VB .
8.2

Modeling with Two Consecutive Solution Problems

This can be achieved by solving consecutively two SPs followed by interpolant
computation: First, compute a reproductive solution R[t] of F [pq]:t. Since it is
a most general solution, if there is a particular solution, say GH, that meets the
vocabulary restrictions, there must be a sequence T of “instantiation formulas”
such that R[T ] ≡ GH. Each member of R[T ] is then “semantically” in the
required predicate vocabulary, that is, equivalent to a formula in which all free
predicates are members of the given set of predicates. Craig-Lyndon interpolation
can be applied on each of these formulas, if they are first-order, to construct

36

Section 9

equivalent formulas that are also syntactically in the required vocabulary as
explained in Sect. 7.1.
The remaining issue is to find suitable instantiation formulas T . These can
again be determined as solutions of a SP: Consider, for example, the case where
for a formula R[tb] a sequence T of formulas should be found such that Ri [T b]
is semantically independent from the members of b, that is, it should hold that
∃b R[T b] ≡ R[T b]. This is equivalent to R[T c] |= R[T b], where c is a sequence
of fresh predicates matching b, and hence also equivalent to |= R[T c] → R[T b].
Thus, suitable T can be obtained as solutions of the SP
(R[tc] → R[tb])[t].

(xxvii)

For an n-ary solution problem where R1 [tb1 ] . . . Rn [tbn ] is given and the requirement is that for all i ∈ {1, . . . , n} it holds that ∃bi Ri [T bi ] ≡ Ri [T bi ], a single
SP that combines the requirements can be used:
(

n
^

(Ri [tci ] → Ri [tbi ]))[t],

(xxviii)

i=1

where, for i ∈ {1, . . . , n}, ci is a sequence of fresh predicates that matches bi .
In fact, if m, n ≥ 1 the first SP of this method can be trivially solved: As
reproductive solution take the rigorous solution based on a particular solution
where G1 = ¬b1 (x1 . . . xarity(p1 ) ), H1 = ¬q1 (x1 . . . xarity(q1 ) ), and G2 . . . Gm and
H2 . . . Hn have arbitrary values, for example >. The actual effort to construct
the vocabulary restricted solution is then required for the second SP.
8.3

Expressing a Vocabulary Restriction on all Unknowns

A different technique applies to solution problems where there is only a single set
of predicates, say the set of members of the sequence b of predicates, that are not
permitted to occur free in the solution components: The vocabulary restriction
can then be directly encoded into the solution problem by means of secondorder quantification, justified by the equivalence of the following statements,
which follows from the requirement of substitutibility for solutions:

9

G is a solution of the SP F [p] and free(G) ∩ b = ∅.

(xxix)

G is a solution of the SP (∀b F )[p].

(xxx)

A Herbrand View on the Solution Problem

The characterization of solution in Prop. 9 is by an entailment of F . In presence
of the result of [16] for quantifier free predicate logic this brings up the question
whether Skolemization and Herbrand’s theorem justify some “instance-based”
technique for computing solutions that succeed on large enough quantifier expansions. The following is a formal account of that scenario which, so far, shows
no positive result but might be useful as a basis for further investigations.

Conclusion

37

Consider a 1-SP F [p] that has a solution G. By Prop. 9 it then holds that
p ⇔ G |= F . Let D stand for p ⇔ G. By Herbrand’s theorem we know that
there are formulas D0 , F 0 , Dh and F h and sequences of fresh functions d and f
such that
p ⇔ G = D ≡ ∀f ∃d D0 |= ∀f ∃d Dh |= ∀f ∃d F h |= ∀f ∃d F 0 ≡ F,

(xxxi)

and Dh |= F h . The functions d and f are the functions introduced by Skolemizing D (w.r.t. ∃) and F (w.r.t. ∀), respectively (this is the only place in the paper
where we consider second-order quantification upon functions). Formulas D0
and F 0 are the universal and existential, resp., first-order formulas, obtained
from Skolemizing D0 and F 0 , respectively. Formulas Dh and F h are quantifier free, obtained from D0 and F 0 , resp., by instantiating their matrices with
terms constructed from d, f and the free individual symbols in D or F (it is
assumed w.l.o.g. that at least one individual symbol is among the symbols available for term construction). We thus know p ⇔ G |= ∀f ∃d F h , or, equivalently,
p ⇔ G |= ∃ d F h . Thus G must be the solution to the 1-SP (∀f ∃d F h )[p], where
F h is quantifier-free and ∀f ∃d is a second-order prefix with quantifiers upon
functions.
As a sufficient condition for solutions it can be derived from this setting that
a solution H of the quantifier-free formula F h in which no member of f occurs
free is, under the assumption CLEAN(F ), also a solution of F , which follows
since p ⇔ H |= F h |= ∃dF h |= ∀f ∃dF h |= F .

10

Conclusion

The solution problem and second-order quantifier elimination were interrelated
tools in the early mathematical logic. Today elimination has entered automatization with applications in the computation of circumscription, in modal logics,
and for semantic forgetting and modularizing knowledge bases, in particular for
description logics. Since the solution problem on the basis of first-order logic is,
like first-order validity, recursively enumerable there seems some hope to adapt
techniques from first-order theorem proving.
The paper makes the relevant scenario accessible from the perspective of
predicate logic and theorem proving. It shows that a wealth of classical material
on Boolean equation solving can be transferred to predicate logic and only few
essential diverging points crystallize, like the constructability of witness formulas
for quantified predicates, and “Schröder’s reproductive interpolant” that does not
apply in general to first-order logic. An abstracted version of the core property
underlying the classical method of successive eliminations provides a foundation
for systematizing and generalizing algorithms that reduce n-ary solution problems to unary solution problems. Special cases based on Craig interpolation have
been identified as first steps towards methods for solution construction.
Beyond the presented core framework there seem to be many results from different communities that are potentially relevant for further investigation. This includes the vast amount of techniques for equation solving on the basis of Boolean

38

Section 10

algebra and its variants, developed over the last 150 years. For description logics
there are several results on concept unification, e.g., [4,3]. Variants of Craig interpolation such as disjunctive interpolation [32] share with the solution problem
at least the objective to find substitution formulas such that the overall formula
becomes valid (or, dually, unsatisfiable).
Among the issues that immediately suggest themselves for further research
are the parallel between nondeterministic methods with execution paths for each
particular solution and methods that compute a most general solution, the exploration of formula simplifications and techniques such as definitional normal forms
to make constructions like rigorous solution and reproductive interpolant feasible, and the investigation of the relaxed notion of substitutibility under which
solutions for relational monadic formulas can be constructed. The possible characterization of solution by an entailment also brings up the question whether
Skolemization and Herbrand’s theorem justify some “instance-based” technique
for computing solutions that succeeds on large enough quantifier expansions.
Acknowledgments
The author thanks anonymous reviewers for their helpful comments. This work
was supported by DFG grant WE 5641/1-1.

References

39

References
1. Ackermann, W.: Untersuchungen über das Eliminationsproblem der mathematischen Logik. Math. Ann. 110, 390–413 (1935)
2. Baader, F.: On the complexity of Boolean unification. Inf. Process. Lett. 67(4),
215–220 (Aug 1998)
3. Baader, F., Morawska, B.: Unification in the description logic EL. Logical Methods
in Computer Science 6(3), 1–31 (2010)
4. Baader, F., Narendran, P.: Unification of concept terms in description logics. J.
Symb. Comput. 31, 277–305 (2001)
5. Behmann, H.: Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem. Math. Ann. 86(3–4), 163–229 (1922)
6. Behmann, H.: Das Auflösungsproblem in der Klassenlogik. Archiv für Philosophie
4(1), 97–109 (1950), (First of two parts, also published in Archiv für mathematische
Logik und Grundlagenforschung, 1.1 (1950), pp. 17-29)
7. Behmann, H.: Das Auflösungsproblem in der Klassenlogik. Archiv für Philosophie
4(2), 193–211 (1951), (Second of two parts, also published in Archiv für mathematische Logik und Grundlagenforschung, 1.2 (1951), pp. 33-51)
8. Brown, F.M.: Boolean Reasoning. Dover Publications, second edn. (2003)
9. Büttner, W., Simonis, H.: Embedding Boolean expressions into logic programming.
J. Symb. Comput. 4(2), 191–205 (1987)
10. Carlsson, M.: Boolean constraints in SICStus Prolog. Tech. Rep. SICS T91:09,
Swedish Institute of Computer Science, Kista (1991)
11. Conradie, W.: On the strength and scope of DLS. J. Applied Non-Classical Logic
16(3–4), 279–296 (2006)
12. Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA. LMCS 2(1:5), 1–26 (2006)
13. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J.
Symb. Log. 22(3), 250–268 (1957)
14. Deschamps, J.P.: Parametric solutions of Boolean equations. Discrete Mathematics
3, 333–342 (1972)
15. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited: A
reduction algorithm. J. Autom. Reasoning 18(3), 297–338 (1997)
16. Eberhard, S., Hetzl, S., Weller, D.: Boolean unification with predicates. J. Logic
and Computation 27(1), 109–128 (2017)
17. Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, 2nd
edn. (1995)
18. Gabbay, D.M., Schmidt, R.A., Szałas, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications
(2008)
19. Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic.
In: KR’92. pp. 425–435. Morgan Kaufmann (1992)
20. Hodges, W.: A Shorter Model Theory. Cambridge University Press (1997)
21. Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. In:
PODS’90. pp. 299–313. ACM Press (1990)
22. Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. J. Comput. Syst. Sci. 51(1), 26–52 (1995)
23. Koopmann, P., Schmidt, R.A.: Uniform interpolation of ALC-ontologies using fixpoints. In: FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 87–102. Springer (2013)

40
24. Löwenheim, L.: Über das Auflösungsproblem im logischen Klassenkalkül. In:
Sitzungsberichte der Berliner Mathematischen Gesellschaft. vol. 7, pp. 89–94. Teubner (1908)
25. Löwenheim, L.: Über die Auflösung von Gleichungen im logischen Gebietekalkül.
Math. Ann. 68, 169–207 (1910)
26. Martin, U., Nipkow, T.: Unification in Boolean rings. In: CADE-8. LNCS (LNAI),
vol. 230, pp. 506–513. Springer (1986)
27. Martin, U., Nipkow, T.: Unification in Boolean rings. J. Autom. Reasoning 4(4),
381–396 (1988)
28. Martin, U., Nipkow, T.: Boolean unification – The story so far. J. Symb. Comput.
7, 275–293 (1989)
29. Otto, M.: An interpolation theorem. Bulletin of Symbolic Logic 6, 447–462 (2000)
30. Rudeanu, S.: Boolean Functions and Equations. Elsevier (1974)
31. Rudeanu, S.: Lattice Functions and Equations. Springer (2001)
32. Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for Horn-clause verification. In: CAV 2013. LNCS, vol. 8044, pp. 347–363. Springer (2013)
33. Schmidt, R.A.: The Ackermann approach for modal logic, correspondence theory
and second-order reduction. J. Applied Logic 10(1), 52–74 (2012)
34. Schröder, E.: Vorlesungen über die Algebra der Logik. Teubner (vol. 1, 1890; vol. 2,
pt. 1, 1891; vol. 2, pt. 2, 1905; vol. 3, 1895)
35. Seidl, M., Lonsing, F., Biere, A.: bf2epr: A tool for generating EPR formulas from
QBF. In: PAAR-2012. EPiC, vol. 21, pp. 139–148 (2012)
36. Smullyan, R.M.: First-Order Logic. Springer, New York (1968), also republished
with corrections by Dover publications, New York, 1995
37. Sofronie, V.: Formula-handling computer solution of Boolean equations. I. Ring
equations. Bull. of the EATCS 37, 181–186 (1989)
38. Wernhard, C.: Heinrich Behmann’s contributions to second-order quantifier elimination. Tech. Rep. KRR 15–05, TU Dresden (2015)
39. 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. 253–269. Springer (2015)
40. Wernhard, C.: The Boolean solution problem from the perspective of predicate
logic. In: FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 333–350 (2017)
41. Zhao, Y., Schmidt, R.A.: Concept forgetting in ALCOI-ontologies using an Ackermann approach. In: ISWC 2015. LNCS, vol. 9366, pp. 587–602. Springer (2015)

