=Paper=
{{Paper
|id=Vol-2013/paper18
|storemode=property
|title=The Boolean Solution Problem from the Perspective of Predicate Logic (Abstract)
|pdfUrl=https://ceur-ws.org/Vol-2013/paper18.pdf
|volume=Vol-2013
|authors=Christoph Wernhard
|dblpUrl=https://dblp.org/rec/conf/soqe/Wernhard17a
}}
==The Boolean Solution Problem from the Perspective of Predicate Logic (Abstract)==
https://ceur-ws.org/Vol-2013/paper18.pdf
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