Finding solution values for unknowns in Boolean equations was, along with second-order quantifier elimination, a principal reasoning mode in the Algebra of Logic of the 19th century. Schröder [19] 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 [17] 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 [14,6,15,16,10,11]. The Π P 2 -completeness of Boolean unification with constants was proven only later in [10,11] and seemingly independently in [1]. Schröder's results were developed further by Löwenheim [12,13]. A generalization of Boole's method beyond propositional logic to relational monadic formulas has been presented by Behmann in the early 1950s [3,4]. 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 [8]. A brief discussion of Boolean reasoning in comparison with predicate logic can be found in [5].

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.

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 "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 first-order provers, SAT and QBF solving, and second-order quantifier elimination based on resolution [9] and the Ackermann approach [7]. Numerous applications of Boolean equation solving in various fields are summarized in [18,Chap. 14]. Applications in automated theorem proving and proof compression are mentioned in [8,Sect. 7]. The prevention of certain redundancies has been described as application of (concept) unification in description logics [2]. Here the synthesis of definitional equivalences is sketched as an application.

The material underlying the workshop presentation has in part been published as [20] and is described comprehensively in the report [21].