1 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 [schroeder:all] 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 [rudeanu:74]
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
[martinnipkow:ringsearly, buettner:simonis:87, martinnipkow:ringsjournal, martin:nipkov:boolean:89, kkr:90, kkr:95]. An early implementation based on [rudeanu:74] has been also described in [Sofronie89]. An implementation with BDDs of the algorithm from [buettner:simonis:87] is reported in [carlsson:boolean:91]. The completeness of Boolean unification with constants was proven only later in [kkr:90, kkr:95] and seemingly independently in [baader:boolean:98]. Schröder’s results were developed further by Löwenheim [loewenheim:1908, loewenheim:1910]. A generalization of Boole’s method beyond propositional logic to relational monadic formulas has been presented by Behmann in the early 1950s [beh:50:aufloesungs:phil:1, beh:51:aufloesungs:phil:2]. Recently the complexity of Boolean unification in a predicate logic setting has been investigated for some formula classes, in particular for quantifierfree firstorder formulas [eberhard]. A brief discussion of Boolean reasoning in comparison with predicate logic can be found in [brown:boolean:03].Here we remodel the solution problem formally along with basic classical results and some new generalizations in the framework of firstorder logic extended by secondorder quantification. The main thesis of this work is that it is possible and useful to apply secondorder quantification consequently throughout the formalization. What otherwise would require metalevel 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 secondorder quantifier elimination and Craig interpolation become visible. Of course, methods to solve Boolean equations on firstorder 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 secondorder quantifier elimination (or “semantic forgetting”), Craig interpolation 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 firstorder provers, SAT and QBF solving, and secondorder quantifier elimination based on resolution [scan] and the Ackermann approach [dls]. Numerous applications of Boolean equation solving in various fields are summarized in [rudeanu:01, Chap. 14]. Applications in automated theorem proving and proof compression are mentioned in [eberhard, Sect. 7]. The prevention of certain redundancies has been described as application of (concept) unification in description logics [baader:narendran:01]. 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. LABEL:secconstruction various techniques for solution construction in particular cases are discussed. The solution problem with vocabulary restrictions is discussed in Sect. LABEL:secvocab. The solution problem is displayed in Sect. LABEL:secherbrand as embedded in a setting with Skolemization and Herbrand expansion. Section LABEL:secconclusion closes the paper with concluding remarks.
2 Notation and Preliminaries
2.1 Notational Conventions
We consider formulas in firstorder logic with equality extended by secondorder 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 ary versions of and can be understood as metalevel notation. The operators and bind stronger than , and . The scope of , the quantifiers, and the
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 is denoted by . The set of symbols that occur free in a formula is denoted by . The property that no member of is bound by a quantifier occurrence in is expressed as . Symbols not present in the formulas and other items under discussion are called fresh. The clean variant of a given formula is the formula obtained from by successively replacing all bound symbols with fresh symbols such that . The replacement is done in some way not specified here further such that each formula has a unique clean variant.
We write for entails ; for is valid; and for is equivalent to , that is, and .
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 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 , where is a sequence of terms whose length is the arity of the predicate . Atoms of the form , that is, with a nullary predicate , are written also as . For a sequence of fresh symbols we assume that its members are distinct. A sequence of predicates is said to match another sequence if and only if and for all it holds that . If is a sequence of symbols, then stands for and for .
If is a sequence of formulas, then states for all , and . If is a second sequence of formulas, then stands for and …and .
As explained below, in certain contexts the individual symbols in the set play a special role. For example in the following shorthands for a predicate , a formula and : stands for ; for ; for ; and for .
2.2 Substitution with Terms and Formulas
To express systematic substitution of individual symbols and predicates concisely we use the following notation:

and – Notational Context for Substitution of Individual Symbols. Let be a sequence of distinct individual symbols. We write as to declare that for a sequence of terms the expression denotes with, for , all free occurrences of replaced by .

, and – Notational Context for Substitution of Predicates. Let be a sequence of distinct predicates and let be a formula. We write as to declare the following:

For a sequence of formulas the expression denotes with, for , each atom occurrence where is free in replaced by .

For a sequence of predicates that matches the expression denotes with, for , each free occurrence of replaced by .

The above notation , where is a sequence of formulas or of predicates, is generalized to allow also at the th position of , for example . The formula then denotes with only those predicates with that are not present at the th position in replaced by the th component of as described above (in the example only would be replaced).


– Notational Context for Substitution in a Sequence of Formulas. If is a sequence of formulas, then declares that , where is a sequence with the same length as , is to be understood as the sequence with the meaning of the members as described above.
In the above notation for substitution of predicates by formulas the members of play a special role: can be alternatively considered as obtained by replacing predicates with expressions followed by conversion. The shorthand can be correspondingly considered as . The following property substitutible specifies preconditions for meaningful simultaneous substitution of formulas for predicates: [ – Substitutible Sequence of Formulas] A sequence of formulas is called substitutible for a sequence of distinct predicates in a formula , written , if and only if and for all it holds that No free occurrence of in is in the scope of a quantifier occurrence that binds a member of ; ; and . 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 , which hold if no member of does occur in the terms . Analogously, substitutible subformulas can be “pulled out of” and “pushed in to” formulas: [PullingOut and PushingIn of Subformulas] Let be a sequence of formulas, let be a sequence of distinct predicates and let be a formula such that . Then
proppullout
propfixing Ackermann’s Lemma [ackermann:35] can be applied in certain cases to eliminate secondorder quantifiers, that is, to compute for a given secondorder formula an equivalent firstorder formula. It plays an important role in many modern methods for elimination and semantic forgetting – see, e.g., [dls, sqema, soqe, schmidt:2012:ackermann, ks:2013:frocos, ZhaoSchmidt15b]: [Ackermann’s Lemma, Positive Version] Let be formulas and let be a predicate such that , and all free occurrences of in have negative polarity. Then .
3 The Solution Problem from Different Angles
3.1 Basic Formal Modeling
Our formal modeling of the Boolean solution problem is based on two concepts, solution problem and particular solution: [ – Solution Problem (SP), Unary Solution Problem (1SP)] A solution problem (SP) is a pair of a formula and a sequence of distinct predicates. The members of are called the unknowns of the SP. The length of is called the arity of the SP. A SP with arity is also called unary solution problem (1SP). The notation for solution problems establishes as a “side effect” a context for specifying substitutions of in by formulas as specified in Sect. 2.2. [Particular Solution] A particular solution (briefly solution) of a SP is defined as a sequence of formulas such that and . The property in this definition implies that no member of 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 and . The variant based on validity has been chosen here because then the associated secondorder 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 is a solution of , then all sequences of formulas such that and (that is, if and , then holds for all ) are also solutions of .
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 firstorder 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.
[A Solution Problem and its Particular Solutions] As an example of a solution problem consider where
The intuition is that the antecedent specifies the “background theory”, and w.r.t. that theory the unknown is “stronger” than the other unknown , which, in addition, is “between” and . Examples of solutions are: ; ; ; ; and . No solutions are for example ; ; and all members of . Assuming a countable vocabulary, the set of valid firstorder formulas is recursively enumerable. It follows that for an ary SP where is firstorder the set of those of its particular solutions that are sequences of firstorder formulas is also recursively enumerable: An ary sequence of wellformed firstorder formulas that satisfies the syntactic restriction is a solution of if and only if 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 secondorder quantifier elimination, and as related to determining definientia and interpolants.
3.2 View as Unification
Because if and only if , a particular solution of can be seen as a unifier of the two formulas and modulo logical equivalence as equational theory. From the perspective of unification the two formulas appear as terms, the members of 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 and , which holds for sequences and of formulas and predicates, respectively, and formulas , such that and . This view of formula unification can be generalized to sets with a finite cardinality of equivalences, since for all it holds that can be expressed as .
An exact correspondence between solving a solution problem where is a propositional formula with as logic operators and Eunification with constants in the theory of Boolean algebra (with the mentioned logic operators as signature) applied to can be established: Unknowns correspond to variables and propositional atoms in correspond to constants. A particular solution corresponds to a unifier 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 [eberhard]. The material presented here is largely orthogonal to that work, but a technique from [eberhard] has been adapted to more general cases in Sect. LABEL:secehw.
3.3 View as Construction of Elimination Witnesses
Another view on the solution problem is related to eliminating secondorder quantifiers by replacing the quantified predicates with “witness formulas”. [ELIMWitness] Let be a sequence of distinct predicates. An ELIMwitness of in a formula is defined as a sequence of formulas such that and . The condition in this definition is equivalent to . If and the considered are firstorder, then finding an ELIMwitness is secondorder quantifier elimination on a firstorder argument formula, restricted by the condition that the result is of the form . Differently from the general case of secondorder quantifier elimination on firstorder 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 wellknown elimination methods yield ELIMwitnesses, for example rewriting a formula that matches the left side of Ackermann’s Lemma (Prop. 2.2) with its right side, which becomes evident when considering that the right side is equivalent to . Finding particular solutions and finding ELIMwitnesses can be expressed in terms of each other: [Solutions and ELIMWitnesses] Let be a SP and let be a sequence of formulas. Then:
propwititosol is an ELIMwitness of in if and only if is a solution of the SP , where is a sequence of fresh predicates matching .
propsolitowit is a solution of if and only if is an ELIMwitness of in and it holds that .
Proof (Sketch)
Assume . (LABEL:propwititosol) Follows since iff iff iff . (LABEL:propsolitowit) LeftToRight: Follows since implies and , which implies . Righttoleft: Follows since and together imply . ∎
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: [Solution as Entailed by a Definition] A sequence of formulas is a particular solution of a SP if and only if and .
Proof
Follows from the definition of particular solution and Prop. LABEL:proppullout. ∎
In the special case where is a 1SP with a nullary unknown , the characterization of a solution according to Prop. 3.4 can be expressed with an entailment where a definition of the unknown appears on the right instead of the left side: If is nullary, then . Thus, the statement is for nullary equivalent to
(i) 
The second condition of the characterization of solution according to Prop. 3.4, that is, , holds if it is assumed that is not in , that and that no member of is bound by a quantifier occurrence in . A solution is then characterized as negated definiens of in the negation of . Another way to express (i) along with the condition that is semantically independent from is as follows:
(ii) 
The secondorder quantifiers upon the nullary can be eliminated, yielding the following equivalent statement:
(iii) 
Solutions then appear as the formulas in a range, between and . This view is reflected in [rudeanu:74, Thm. 2.2], which goes back to work by Schröder. If is firstorder, then Craig interpolation can be applied to compute formulas that also meet the requirements and to ensure . Further connections to Craig interpolation are discussed in Sect. LABEL:secconstruction.
4 The Method of Successive Eliminations – Abstracted
4.1 Reducing ary to ary Solution Problems
The method of successive eliminations to solve an 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 [rudeanu:74, Chapter 2, § 4]. It has been rediscovered in the context of Boolean unification in the late 1980s, notably with [buettner:simonis:87]. Rudeanu notes in [rudeanu:74, p. 72] that variants described by several authors in the 19th century are discussed by Schröder [schroeder:all, 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 [rudeanu:74, Chapter 2, § 4], is more abstract in several aspects: Secondorder quantification upon predicates that represent unknowns plays the role of metalevel shorthands that encode expansions; no commitment to a particular formula class is made, thus the proposition applies to secondorder formulas with firstorder 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 secondorder formulas (that occur also for inputs without secondorder quantifiers) are handled. The algorithm descriptions in the following subsections show different possibilities to instantiate these abstracted aspects. [Characterization of Solution Underlying the Method of Successive Eliminations] Let be a SP and let be a sequence of formulas. Then the following statements are equivalent:
is a solution of .
For : is a solution of the 1SP
such that .
Proof
Lefttoright: From 4.1 it follows that . Hence, for all by Prop. LABEL:propfixing it follows that
From 4.1 it also follows that . This implies that for all it holds that
We thus have derived for all the two properties that characterize as a solution of the 1SP as stated in 4.1.
Righttoleft: From 4.1 it follows that is a solution of the 1SP
Hence, by the characteristics of solution it follows that . The property can be derived from and the fact that for all it holds that . The properties and characterize as a solution of the SP . ∎
This proposition states an equivalence between the solutions of an ary SP and the solutions of 1SPs. These 1SPs are on formulas with an existential secondorder prefix. The following gives an example of this decomposition: [Reducing an ary Solution Problem to Unary Solution Problems] Consider the SP of Examp. 3.1. The 1SP with unknown according to Prop. 4.1 is
whose formula is, by secondorder quantifier elimination, equivalent to . Take as solution of that 1SP. The 1SP with unknown according to Prop. 4.1 is
Its formula is then, by replacing in as specified in Examp. 3.1 with and removing the duplicate conjunct obtained then, equivalent to
A solution of that second 1SP is, for example, , yielding the pair as solution of the originally considered SP .
4.2 Solving on the Basis of SecondOrder Formulas
The following algorithm to compute particular solutions is an immediate transfer of Prop. 4.1. Actually, it is more an “algorithm template”, since it is parameterized with a method to compute 1SPs and covers a nondeterministic as well as a deterministic variant: [] Let be a class of formulas and let be a nondeterministic or a deterministic algorithm that outputs for 1SPs of the form with solutions such that and .
Input: A SP , where , that has a solution.
Method: For to do: Assign to an output of applied to the 1SP
Output: The sequence of formulas, which is a particular solution of . The solution components are successively assigned to some solution of the 1SP given in Prop. 4.1, on the basis of the previously assigned components . Even if the formula of the input problem does not involve secondorder quantification, these 1SPs are on secondorder formulas with an existential prefix upon the yet “unprocessed” unknowns.
The algorithm comes in a nondeterministic and a deterministic variant, just depending on whether is instantiated by a nondeterministic or a deterministic algorithm. Thus, in the nondeterministic variant the nondeterminism of is the only source of nondeterminism. With Prop. 4.1 it can be verified that if a nondeterministic is “complete” in the sense that for each solution there is an execution path that leads to the output of that solution, then also based on it enjoys that property, with respect to the ary solutions .
For the deterministic variant, from Prop. 4.1 it follows that if is “complete” in the sense that it outputs some solution whenever a solution exists, then, given that has a solution, which is ensured by the specification of the input, also outputs some solution .
This method applies to existential secondorder formulas, which prompts some issues for future research: As indicated in Sect. 3.4 (and elaborated in Sect. LABEL:secconstruction) Craig interpolation can in certain cases be applied to compute solutions of 1SPs. Can QBF solvers, perhaps those that encode QBF into predicate logic [qbf:pl], be utilized to compute Craig interpolants? Can it be useful to allow secondorder quantifiers in solution formulas because they make these smaller and can be passed between different calls to ?
As shown in Sect. 6, if is a method that outputs socalled reproductive solutions, that is, most general solutions that represent all particular solutions, then also 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 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 [schroeder:all, loewenheim:1910, rudeanu:74] and is modeled in the present framework in Sect. 6. Compared to , the method handles the secondorder quantification by eliminating quantifiers onebyone, insideout, with a specific method and applies a specific method to solve 1SPs, which actually yields reproductive solutions. These incorporated methods apply to propositional input formulas (and to firstorder input formulas if the unknowns are nullary). Secondorder quantifiers are eliminated by rewriting with the equivalence . As solution of an 1SP the formula is taken, where is a fresh nullary predicate that is considered specially. The intuition is that particular solutions are obtained by replacing with arbitrary formulas in which does not occur (see Sect. 6 for a more indepth discussion).
The following algorithm is an iterative presentation of the method of successive eliminations, also called Boole’s method, in the variant due to [buettner:simonis:87]. The presentation in [martin:nipkov:boolean:89, Sect. 3.1], where apparently minor corrections compared to [buettner:simonis:87] have been made, has been taken here as technical basis. We stay in the validitybased setting, whereas [rudeanu:74, buettner:simonis:87, martin:nipkov:boolean:89] use the unsatisfiabilitybased setting. Also differently from [buettner:simonis:87, martin:nipkov:boolean:89] we do not make use of the xor operator. []
Input: A SP , where is propositional, that has a solution and a sequence of fresh nullary predicates.
Method:

Initialize with .

For to do: Assign to the formula .

For to do: Assign to the formula
Output: The sequence of formulas, which is a reproductive solution of with respect to the special predicates . The formula assigned to in step (2.) is the result of eliminating in and the formula assigned to in step (3.) is the reproductive solution of the 1SP , obtained with the respective incorporated methods indicated above. The recursion in the presentations of [buettner:simonis:87, martin:nipkov:boolean:89] is translated here into two iterations that proceed in opposite directions: First, existential quantifiers of are eliminated insideout and the intermediate results, which do not involve secondorder quantifiers, are stored. Solutions of 1SPs 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 plugin 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 1SPs. If the pluggedin method to compute 1SPs outputs particular solutions, then computes particular instead of reproductive solutions.
4.4 Solving by InsideOut Witness Construction
Like , the following algorithm eliminates secondorder quantifiers onebyone, insideout, avoiding intermediate formulas with existential secondorder prefixes of length greater than , which arise with . In contrast to , it performs elimination by the computation of ELIMwitnesses. [] Let be a class of formulas and be an algorithm that computes for formulas and predicates an ELIMwitness of in such that .
Input: A SP , where , that has a solution.
Method: For to do:

Assign to the output of applied to

For to do: Reassign to the formula .
Output: : The sequence of formulas, which provides a particular solution of . Step (2.) in the algorithm expresses that a new value is assigned to and that can be designated by , justified because the new value does not contain free occurrences of . In step (1.) the respective current values of are used to instantiate . It is not hard to see from the specification of the algorithm that for input and output it holds that and that . By Prop. LABEL:propsolitowit, is then a solution if . This holds indeed if has a solution, as shown below with Prop. 5.1.
If is “complete” in the sense that it computes an elimination witness for all input formulas in , then outputs a solution. Whether all solutions of the input SP can be obtained as outputs for different execution paths of a nondeterministic version of obtained through a nondeterministic , in analogy to the nondeterministic variant of , appears to be an open problem.
5 Existence of Solutions
5.1 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 [rudeanu:74], the SP is consistent. A necessary condition is easy to see: [Necessary Condition for the Existence of a Solution] If a SP has a solution, then it holds that .
Proof
Follows from the definition of particular solution and Prop. LABEL:propfixing. ∎
Under certain presumptions that hold for propositional logic this condition is also sufficient. To express these abstractly we use the following concept:
[SOLWitnessed Formula Class] A formula class is called SOLwitnessed for a predicate class if and only if for all and the following statements are equivalent:
.
There exists a solution of the 1SP such that . Since the righttoleft direction of that equivalence holds in general, the lefttoright direction alone would provide an alternate characterization. The class of propositional formulas is SOLwitnessed (for the class of nullary predicates). This follows since in propositional logic it holds that
(iv) 
which can be derived in the following steps: .
The following definition adds closedness under existential secondorder quantification and dropping of void secondorder quantification to the notion of SOLwitnessed, to allow the application on 1SPs matching with item (b) in Prop. 4.1: [MSESOLWitnessed Formula Class] A formula class is called MSESOLwitnessed for a predicate class if and only if it is SOLwitnessed for , for all predicates in and it holds that , and, if and , then . The class of existential QBFs (formulas of the form where is propositional) is MSESOLwitnessed (like the more general class of QBFs – secondorder formulas with only nullary predicates). Another example is the class of firstorder formulas extended by secondorder quantification upon nullary predicates, which is MSESOLwitnessed 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 MSESOLwitnessed class: [Solution Existence Lemma] Let be a formula class that is MSESOLwitnessed for predicate class . Let with . If , then for all there exists a sequence of formulas such that , , and .
Proof
By induction on the length of the sequence . The conclusion of the proposition holds for the base case : The statement holds trivially, is given as precondition, and follows from . For the induction step, assume that the conclusion of the proposition holds for some . That is, there exists a sequence of formulas such that , , and . Since is MSESOLwitnessed for and it follows that there exists a solution of the 1SP
such that . From the characteristics of solution it follows that
which implies (since all members of with exception of are in the quantifier prefix of the problem formula) that , hence
Given the induction hypothesis , it also implies
From the characteristics of solution it follows in addition that
which, since , is equivalent to
Finally, we conclude from , established above, and the definition of MSESOLwitnessed that
which completes the proof of the induction step. ∎
A sufficient and necessary condition for the existence of a solution of formulas in MSESOLwitnessed classes now follows from Prop. 5.1 and Prop. 5.1: [Existence of a Solution] Let be a formula class that is MSESOLwitnessed on predicate class . Then for all where the members of are in the following statements are equivalent:
.
There exists a solution of the SP such that .
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 [kkr:90, kkr:95, baader:boolean:98], that is, completeness: By Prop. 5.1, a SP where is propositional has a solution if and only if the existential QBF is valid and, vice versa, an arbitrary existential QBF (where is quantifierfree) is valid if and only if the SP has a solution.
5.2 Characterization of SOLWitnessed in Terms of ELIMWitness
The following proposition shows that under a minor syntactic precondition on formula classes, SOLwitnessed can also be characterized in terms of ELIMwitness instead of solution as in Def. 5.1: [SOLWitnessed in Terms of ELIMWitness] Let be a class of formulas that satisfies the following properties: For all and predicates with the same arity of it holds that , and for all it holds that . The class is SOLwitnessed for a predicate class if and only if for all and there exists an ELIMwitness of in such that .
Proof
Lefttoright: Assume that is meets the specified closedness conditions and is SOLwitnessed for , and . Let be a fresh predicate with the arity of . The obviously true statement is equivalent to and thus to By the closedness properties of it holds that . Since is SOLwitnessed for it thus follows from Def. 5.1 that there exists a solution of the SP such that , and, by the closedness properties, also
Comments
There are no comments yet.