Skip to main content
SpringerLink
Log in

Connecting Many-Sorted Theories

  • Conference paper
Automated Deduction – CADE-20 (CADE 2005)

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

Included in the following conference series:

Abstract

Basically, the connection of two many-sorted theories is obtained by taking their disjoint union, and then connecting the two parts through connection functions that must behave like homomorphisms on the shared signature. We determine conditions under which decidability of the validity of universal formulae in the component theories transfers to their connection. In addition, we consider variants of the basic connection scheme.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ajili, F., Kirchner, C.: A modular framework for the combination of symbolic and built-in constraints. In: Proceedings of Fourteenth International Conference on Logic Programming, Leuven, Belgium, pp. 331–345. The MIT Press, Cambridge (1997)

    Google Scholar 

  2. Baader, F., Ghilardi, S.: Connecting many-sorted theories. LTCS-Report LTCS-05-04, TU Dresden, Germany, See (2005), http://lat.inf.tu-dresden.de/research/reports.html

  3. Baader, F., Ghilardi, S., Tinelli, C.: A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 183–197. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Baader, F., Lutz, C., Sturm, H., Wolter, F.: Fusions of description logics and abstract description systems. Journal of Artificial Intelligence Research 16, 1–58 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  5. Baader, F., Tinelli, C.: A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method. In: Proceedings of the 14th International Conference on Automated Deduction, Townsville (Australia). LNCS (LNAI), vol. 1249, pp. 19–33. Springer, Heidelberg (1997)

    Google Scholar 

  6. Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Information and Computation 178(2), 346–390 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  7. Chang, C.-C., Keisler, H.J.: Model Theory, 3rd edn. North-Holland, Amsterdam (1990)

    MATH  Google Scholar 

  8. Domenjoud, E., Klay, F., Ringeissen, C.: Combination techniques for non-disjoint equational theories. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 267–281. Springer, Heidelberg (1994)

    Google Scholar 

  9. Fiorentini, C., Ghilardi, S.: Combining word problems through rewriting in categories with products. Theoretical Computer Science 294, 103–149 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  10. Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, New York (1986)

    MATH  Google Scholar 

  11. Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning 33(3–4), 221–249 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  12. Kracht, M., Wolter, F.: Properties of independently axiomatizable bimodal logics. The Journal of Symbolic Logic 56(4), 1469–1485 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  13. Kutz, O., Lutz, C., Wolter, F., Zakharyaschev, M.: \(\mathcal{E}\)-connections of abstract description systems. Artificial Intelligence 156, 1–73 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  14. Makkai, M., Reyes, G.E.: First-Order Categorical Logic. Lecture Notes in Mathematics, vol. 611. Springer, Berlin (1977)

    MATH  Google Scholar 

  15. Nelson, G.: Combining satisfiability procedures by equality-sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automated Theorem Proving: After 25 Years. Contemporary Mathematics, vol. 29, pp. 201–211. American Mathematical Society, Providence (1984)

    Google Scholar 

  16. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. on Programming Languages and Systems 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  17. Nipkow, T.: Combining matching algorithms: The regular case. Journal of Symbolic Computation 12, 633–653 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  18. Oppen, D.C.: Complexity, convexity and combinations of theories. Theoretical Computer Science 12, 291–302 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  19. Pigozzi, D.: The join of equational theories. Colloquium Mathematicum 30(1), 15–25 (1974)

    MATH  MathSciNet  Google Scholar 

  20. Spaan, E.: Complexity of Modal Logics. PhD thesis, Department of Mathematics and Computer Science, University of Amsterdam, The Netherlands (1993)

    Google Scholar 

  21. Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. Journal of Automated Reasoning 30(1), 1–31 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  22. Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoretical Computer Science 290(1), 291–353 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  23. Wolter, F.: Fusions of modal logics revisited. In: Advances in Modal Logic. CSLI, Stanford, CA (1998)

    Google Scholar 

  24. Zarba, C.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 363–376. Springer, Heidelberg (2002)

    Google Scholar 

  25. Zawadowski, M.W.: Descent and duality. Ann. Pure Appl. Logic 71(2), 131–188 (1995)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Theoretische Informatik, TU Dresden,  

    Franz Baader

  2. Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano,  

    Silvio Ghilardi

Authors
  1. Franz Baader
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Silvio Ghilardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technical University of Catalonia, Barcelona

    Robert Nieuwenhuis

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baader, F., Ghilardi, S. (2005). Connecting Many-Sorted Theories. In: Nieuwenhuis, R. (eds) Automated Deduction – CADE-20. CADE 2005. Lecture Notes in Computer Science(), vol 3632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11532231_21

Download citation

  • DOI: https://doi.org/10.1007/11532231_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28005-7

  • Online ISBN: 978-3-540-31864-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation