Abstract
Finding solution values for unknowns in Boolean equations was a principal reasoning mode in the Algebra of Logic of the 19th century. Schröder investigated it as Auflösungsproblem (solution problem). It is closely related to the modern notion of Boolean unification. Today it is commonly presented in an algebraic setting, but seems potentially useful also in knowledge representation based on predicate logic. We show that it can be modeled on the basis of first-order logic extended by second-order quantification. A wealth of classical results transfers, foundations for algorithms unfold, and connections with second-order quantifier elimination and Craig interpolation show up.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Ackermann, W.: Untersuchungen über das Eliminationsproblem der mathematischen Logik. Math. Ann. 110, 390–413 (1935)
Baader, F.: On the complexity of Boolean unification. Inf. Process. Lett. 67(4), 215–220 (1998)
Baader, F., Morawska, B.: Unification in the description logic \(\cal{EL}\). Log. Methods Comput. Sci. 6(3), 1–31 (2010)
Baader, F., Narendran, P.: Unification of concept terms in description logics. J. Symb. Comput. 31, 277–305 (2001)
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)
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)
Brown, F.M.: Boolean Reasoning, 2nd edn. Dover Publications, Mineola (2003)
Büttner, W., Simonis, H.: Embedding Boolean expressions into logic programming. J. Symb. Comput. 4(2), 191–205 (1987)
Carlsson, M.: Boolean constraints in SICStus Prolog. Technical report SICS T91:09, Swedish Institute of Computer Science, Kista (1991)
Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA. LMCS 2(1:5), 1–26 (2006)
Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited: a reduction algorithm. J. Autom. Reason. 18(3), 297–338 (1997)
Eberhard, S., Hetzl, S., Weller, D.: Boolean unification with predicates. J. Log. Comput. 27(1), 109–128 (2017)
Gabbay, D.M., Schmidt, R.A., Szałas, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications, London (2008)
Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: KR 1992, pp. 425–435. Morgan Kaufmann (1992)
Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. In: PODS 1990, pp. 299–313. ACM Press (1990)
Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. J. Comput. Syst. Sci. 51(1), 26–52 (1995)
Koopmann, P., Schmidt, R.A.: Uniform interpolation of \(\cal{ALC}\)-ontologies using fixpoints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 87–102. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40885-4_7
Löwenheim, L.: Über das Auflösungsproblem im logischen Klassenkalkül. In: Sitzungsberichte der Berliner Mathematischen Gesellschaft, vol. 7, pp. 89–94. Teubner (1908)
Löwenheim, L.: Über die Auflösung von Gleichungen im logischen Gebietekalkül. Math. Ann. 68, 169–207 (1910)
Martin, U., Nipkow, T.: Unification in Boolean rings. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 506–513. Springer, Heidelberg (1986). doi:10.1007/3-540-16780-3_115
Martin, U., Nipkow, T.: Unification in Boolean rings. J. Autom. Reason. 4(4), 381–396 (1988)
Martin, U., Nipkow, T.: Boolean unification - the story so far. J. Symb. Comput. 7, 275–293 (1989)
Rudeanu, S.: Boolean Functions and Equations. Elsevier, Amsterdam (1974)
Rudeanu, S.: Lattice Functions and Equations. Springer, London (2001). doi:10.1007/978-1-4471-0241-0
Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for Horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347–363. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_24
Schmidt, R.A.: The Ackermann approach for modal logic, correspondence theory and second-order reduction. J. Appl. Log. 10(1), 52–74 (2012)
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)
Seidl, M., Lonsing, F., Biere, A.: bf2epr: a tool for generating EPR formulas from QBF. In: PAAR-2012. EPiC, vol. 21, pp. 139–148 (2012)
Sofronie, V.: Formula-handling computer solution of Boolean equations. I. Ring equations. Bull. EATCS 37, 181–186 (1989)
Wernhard, C.: The Boolean solution problem from the perspective of predicate logic - extended version. Technical report KRR 17-01, TU Dresden (2017)
Zhao, Y., Schmidt, R.A.: Concept forgetting in \(\cal{ALCOI}\)-ontologies using an Ackermann approach. In: Arenas, M., et al. (eds.) ISWC 2015. LNCS, vol. 9366, pp. 587–602. Springer, Cham (2015). doi:10.1007/978-3-319-25007-6_34
Acknowledgments
The author thanks anonymous reviewers for their helpful comments. This work was supported by DFG grant WE 5641/1-1.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Wernhard, C. (2017). The Boolean Solution Problem from the Perspective of Predicate Logic. In: Dixon, C., Finger, M. (eds) Frontiers of Combining Systems. FroCoS 2017. Lecture Notes in Computer Science(), vol 10483. Springer, Cham. https://doi.org/10.1007/978-3-319-66167-4_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-66167-4_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66166-7
Online ISBN: 978-3-319-66167-4
eBook Packages: Computer ScienceComputer Science (R0)