99 The Boolean Solution Problem from the Perspective of Predicate Logic (Abstract) Christoph Wernhard TU Dresden, Germany 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 unifica- tion. 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 rep- resentations of all solution substitutions. A central technique there is the method of successive eliminations, which traces back to Boole. Schröder investigated re- productive 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 al- gebra. 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 con- straint 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 generaliza- tion 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 ex- tended by second-order quantification. The main thesis of this work is that it is possible and useful to apply second-order quantification consequently through- out the formalization. What otherwise would require meta-level notation is then expressed just with formulas. As will be shown, classical results can be repro- duced 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 Copyright c 2017 by the paper’s authors In: P. Koopmann, S. Rudolph, R. Schmidt, C. Wernhard (eds.): SOQE 2017 – Pro- ceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics, Dresden, Germany, December 6–8, 2017, published at http://ceur-ws.org. 100 like second-order quantifier elimination (or “forgetting”), Craig interpolation and abduction to support the mechanized reasoning about relationships between the- ories 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 de- scription logics [2]. Here the synthesis of definitional equivalences is sketched as an application. The material underlying the workshop presentation has in part been pub- lished as [20] and is described comprehensively in the report [21]. Acknowledgments. The author thanks anonymous reviewers for their helpful comments. This work was supported by DFG grant WE 5641/1-1. References 1. Baader, F.: On the complexity of Boolean unification. Inf. Process. Lett. 67(4), 215–220 (Aug 1998) 2. Baader, F., Narendran, P.: Unification of concept terms in description logics. J. Symb. Comput. 31, 277–305 (2001) 3. 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) 4. 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 mathema- tische Logik und Grundlagenforschung, 1.2 (1951), pp. 33-51) 5. Brown, F.M.: Boolean Reasoning. Dover Publications, second edn. (2003) 6. Büttner, W., Simonis, H.: Embedding Boolean expressions into logic programming. J. Symb. Comput. 4(2), 191–205 (1987) 7. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited: A reduction algorithm. J. Autom. Reasoning 18(3), 297–338 (1997) 8. Eberhard, S., Hetzl, S., Weller, D.: Boolean unification with predicates. J. Logic and Computation 27(1), 109–128 (2017) 9. Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: KR’92. pp. 425–435. Morgan Kaufmann (1992) 10. Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. In: PODS’90. pp. 299–313. ACM Press (1990) 11. Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. J. Com- put. Syst. Sci. 51(1), 26–52 (1995) 12. Löwenheim, L.: Über das Auflösungsproblem im logischen Klassenkalkül. In: Sitzungsberichte der Berliner Mathematischen Gesellschaft. vol. 7, pp. 89–94. Teub- ner (1908) 13. Löwenheim, L.: Über die Auflösung von Gleichungen im logischen Gebietekalkül. Math. Ann. 68, 169–207 (1910) 101 14. Martin, U., Nipkow, T.: Unification in Boolean rings. In: CADE-8. LNCS (LNAI), vol. 230, pp. 506–513. Springer (1986) 15. Martin, U., Nipkow, T.: Unification in Boolean rings. J. Autom. Reasoning 4(4), 381–396 (1988) 16. Martin, U., Nipkow, T.: Boolean unification – The story so far. J. Symb. Comput. 7, 275–293 (1989) 17. Rudeanu, S.: Boolean Functions and Equations. Elsevier (1974) 18. Rudeanu, S.: Lattice Functions and Equations. Springer (2001) 19. 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) 20. Wernhard, C.: The Boolean solution problem from the perspective of predicate logic. In: FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 333–350 (2017) 21. Wernhard, C.: The Boolean solution problem from the perspective of predicate logic – extended version. Tech. Rep. KRR 17–01, TU Dresden (2017), https: //arxiv.org/abs/1706.08329