Skip to main content
SpringerLink
Log in

The Boolean Solution Problem from the Perspective of Predicate Logic

  • Conference paper
  • First Online:
Frontiers of Combining Systems (FroCoS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10483))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Ackermann, W.: Untersuchungen über das Eliminationsproblem der mathematischen Logik. Math. Ann. 110, 390–413 (1935)

    Article  MathSciNet  MATH  Google Scholar 

  2. Baader, F.: On the complexity of Boolean unification. Inf. Process. Lett. 67(4), 215–220 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  3. Baader, F., Morawska, B.: Unification in the description logic \(\cal{EL}\). Log. Methods Comput. Sci. 6(3), 1–31 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  4. Baader, F., Narendran, P.: Unification of concept terms in description logics. J. Symb. Comput. 31, 277–305 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  5. 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)

    MathSciNet  MATH  Google Scholar 

  6. 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)

    MATH  Google Scholar 

  7. Brown, F.M.: Boolean Reasoning, 2nd edn. Dover Publications, Mineola (2003)

    MATH  Google Scholar 

  8. Büttner, W., Simonis, H.: Embedding Boolean expressions into logic programming. J. Symb. Comput. 4(2), 191–205 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  9. Carlsson, M.: Boolean constraints in SICStus Prolog. Technical report SICS T91:09, Swedish Institute of Computer Science, Kista (1991)

    Google Scholar 

  10. 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)

    MathSciNet  MATH  Google Scholar 

  11. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited: a reduction algorithm. J. Autom. Reason. 18(3), 297–338 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  12. Eberhard, S., Hetzl, S., Weller, D.: Boolean unification with predicates. J. Log. Comput. 27(1), 109–128 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  13. Gabbay, D.M., Schmidt, R.A., Szałas, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications, London (2008)

    MATH  Google Scholar 

  14. Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: KR 1992, pp. 425–435. Morgan Kaufmann (1992)

    Google Scholar 

  15. Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. In: PODS 1990, pp. 299–313. ACM Press (1990)

    Google Scholar 

  16. Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. J. Comput. Syst. Sci. 51(1), 26–52 (1995)

    Article  MathSciNet  Google Scholar 

  17. 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

    Chapter  Google Scholar 

  18. Löwenheim, L.: Über das Auflösungsproblem im logischen Klassenkalkül. In: Sitzungsberichte der Berliner Mathematischen Gesellschaft, vol. 7, pp. 89–94. Teubner (1908)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  20. 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

    Chapter  Google Scholar 

  21. Martin, U., Nipkow, T.: Unification in Boolean rings. J. Autom. Reason. 4(4), 381–396 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  22. Martin, U., Nipkow, T.: Boolean unification - the story so far. J. Symb. Comput. 7, 275–293 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  23. Rudeanu, S.: Boolean Functions and Equations. Elsevier, Amsterdam (1974)

    MATH  Google Scholar 

  24. Rudeanu, S.: Lattice Functions and Equations. Springer, London (2001). doi:10.1007/978-1-4471-0241-0

    Book  MATH  Google Scholar 

  25. 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

    Chapter  Google Scholar 

  26. Schmidt, R.A.: The Ackermann approach for modal logic, correspondence theory and second-order reduction. J. Appl. Log. 10(1), 52–74 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  27. 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)

    Google Scholar 

  28. 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)

    Google Scholar 

  29. Sofronie, V.: Formula-handling computer solution of Boolean equations. I. Ring equations. Bull. EATCS 37, 181–186 (1989)

    MATH  Google Scholar 

  30. Wernhard, C.: The Boolean solution problem from the perspective of predicate logic - extended version. Technical report KRR 17-01, TU Dresden (2017)

    Google Scholar 

  31. 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

    Chapter  Google Scholar 

Download references

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

  1. Technische Universität Dresden, Dresden, Germany

    Christoph Wernhard

Authors
  1. Christoph Wernhard
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Christoph Wernhard .

Editor information

Editors and Affiliations

  1. University of Liverpool, Liverpool, United Kingdom

    Clare Dixon

  2. University of Sao Paulo, Sao Paulo, Brazil

    Marcelo Finger

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation