The Boolean Solution Problem from the Perspective of Predicate Logic (Abstract)

Abstract

Copyright c 2017 by the paper's authors In: P. Koopmann, S. Rudolph, R. Schmidt, C. Wernhard (eds.): SOQE 2017 { Proceedings of the Workshop on Second-Order Quanti er Elimination and Related Topics, Dresden, Germany, December 6{8, 2017, published at http://ceur-ws.org.

-

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 Π2P -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 ]. 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 mathematische 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. Comput. 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 . Teubner ( 1908 )

13. Löwenheim , L. : Über die Auflösung von Gleichungen im logischen Gebietekalkül . Math. Ann. 68 , 169 - 207 ( 1910 )

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