Skip to main content
SpringerLink
Log in

On Hierarchical Reasoning in Combinations of Theories

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2010)

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

Included in the following conference series:

Abstract

In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense also have a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Information and Computation 178(2), 346–390 (2002)

    Article  MathSciNet  Google Scholar 

  2. Basin, D.A., Ganzinger, H.: Automated complexity analysis based on ordered resolution. Journal of the ACM 48(1), 70–109 (2001)

    Article  MathSciNet  Google Scholar 

  3. Bradley, A.R., Manna, Z., Sipma, H.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Burris, S.: Polynomial time uniform word problems. Mathematical Logic Quarterly 41, 173–182 (1995)

    Article  MathSciNet  Google Scholar 

  5. Chang, C.C., Keisler, J.J.: Model Theory. North-Holland, Amsterdam (1990)

    MATH  Google Scholar 

  6. Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Harcourt Academic Press, London (2002)

    MATH  Google Scholar 

  7. Ganzinger, H.: Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems. In: Logic in Computer Science, LICS’01, pp. 81–92. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  8. Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with weak equality. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 168–182. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  10. Givan, R., McAllester, D.A.: New results on local inference relations. In: Nebel, B., Rich, C., Swartout, W.R. (eds.) Knowledge Representation and Reasoning, KR’92, pp. 403–412 (1992)

    Google Scholar 

  11. Givan, R., McAllester, D.A.: Polynomial-time computation via local inference relations. ACM Transactions on Comp. Logic 3(4), 521–541 (2002)

    Article  MathSciNet  Google Scholar 

  12. Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge (1997)

    MATH  Google Scholar 

  13. Ihlemann, C., Sofronie-Stokkermans, V.: System description: H-PILoT. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 131–139. Springer, Heidelberg (2009)

    Google Scholar 

  14. Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Jacobs, S.: Hierarchic Decision Procedures for Verification. PhD. Thesis, Univ. des Saarlandes (2010)

    Google Scholar 

  16. Mal’cev, A.I.: Axiomatizable classes of locally free algebras of various types. The Metamathematics of Algebraic Systems. In: Collected Papers: 1936-1967, Studies in Logic and the Foundation of Mathematics, ch. 23, vol. 66. North-Holland, Amsterdam (1971)

    Google Scholar 

  17. McAllester, D.A.: Automatic recognition of tractability in inference relations. Journal of the ACM 40(2), 284–303 (1993)

    Article  MathSciNet  Google Scholar 

  18. McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 476–490. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  20. Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du Premier Congrès des Mathématiciens des Pays Slaves, 92–101 (1929)

    Google Scholar 

  21. Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 219–234. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  22. Sofronie-Stokkermans, V.: On combinations of local theory extensions. In: Proceedings of the Workshop on Programming Logics in memory of Harald Ganzinger, WPLHG’05 (to appear, 2005), http://arxiv.org/abs/0810.2653

  23. Sofronie-Stokkermans, V.: Hierarchical and modular reasoning in complex theories: The case of local theory extensions. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 47–71. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Sofronie-Stokkermans, V., Ihlemann, C.: Automated reasoning in some local extensions of ordered structures. Journal of Multiple-Valued Logics and Soft Computing 13(4-6), 397–414 (2007)

    MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  26. Tinelli, C., Zarba, C.: Combining non-stably infinite theories. Journal of Automated Reasoning 34(3), 209–238 (2005)

    Article  MathSciNet  Google Scholar 

  27. Weispfenning, V.: The complexity of linear problems in fields. Journal of Symbolic Computation 5(1/2), 3–27 (1988)

    Article  MathSciNet  Google Scholar 

  28. Wheeler, W.H.: Model-companions and definability in existentially complete structures. Israel Journal of Mathematics 25, 305–330 (1976)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max-Planck-Institut für Informatik, Campus E1 4, Saarbrücken, Germany

    Carsten Ihlemann & Viorica Sofronie-Stokkermans

Authors
  1. Carsten Ihlemann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Viorica Sofronie-Stokkermans
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. RWTH Aachen, LuFG Informatik, 2, Ahornstr. 55, 52074, Aachen, Germany

    Jürgen Giesl

  2. Department of Computer Science, Chalmers University of Technology, 41296, Gothenburg, Sweden

    Reiner Hähnle

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ihlemann, C., Sofronie-Stokkermans, V. (2010). On Hierarchical Reasoning in Combinations of Theories. In: Giesl, J., Hähnle, R. (eds) Automated Reasoning. IJCAR 2010. Lecture Notes in Computer Science(), vol 6173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14203-1_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14203-1_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14202-4

  • Online ISBN: 978-3-642-14203-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation