Skip to main content
SpringerLink
Log in

Obtaining Finite Local Theory Axiomatizations via Saturation

  • Conference paper
Frontiers of Combining Systems (FroCoS 2013)

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

Included in the following conference series:

Abstract

In this paper we present a method for obtaining local sets of clauses from possibly non-local ones. For this, we follow the work of Basin and Ganzinger and use saturation under a version of ordered resolution. In order to address the fact that saturation can generate infinite sets of clauses, we use constrained clauses and show that a link can be established between saturation and locality also for constrained clauses: This often allows us to give a finite representation of possibly infinite saturated sets of clauses.

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. Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1) (2009)

    Google Scholar 

  2. Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140–164 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. of Logic and Computation 4(3), 217–247 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  4. Basin, D., Ganzinger, H.: Complexity analysis based on ordered resolution. In: Proc. 11th IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 456–465. IEEE Computer Society Press (1996)

    Google Scholar 

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

  6. Ganzinger, H.: Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems. In: Proc. 16th IEEE Symposium on Logic in Computer Science (LICS 2001), pp. 81–92. IEEE Computer Society Press (2001)

    Google Scholar 

  7. Horbach, M.: Superposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics. PhD thesis, Max Planck Institute for Computer Science and Saarland University (2010)

    Google Scholar 

  8. Horbach, M., Sofronie-Stokkermans, V.: Obtaining finite local theory axiomatizations via saturation. Technical Report ATR 93, Sonderforschungsbereich/Transregio 14 AVACS (2013)

    Google Scholar 

  9. Horbach, M., Weidenbach, C.: Superposition for fixed domains. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 293–307. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  10. Horbach, M., Weidenbach, C.: Decidability results for saturation-based model building. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 404–420. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  11. Horbach, M., Weidenbach, C.: Deciding the inductive validity of ∀∃* queries. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 332–347. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

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

  13. Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 30–45. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  14. Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: On superposition-based satisfiability procedures and their combination. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 594–608. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  15. Lynch, C., Morawska, B.: Automatic decidability. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 7–16. IEEE Comp. Soc. (2002)

    Google Scholar 

  16. Lynch, C., Ranise, S., Ringeissen, C., Tran, D.-K.: Automatic decidability and combinability. Inf. Comput. 209(7), 1026–1047 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  17. Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering constrained clauses. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 477–491. Springer, Heidelberg (1992)

    Google Scholar 

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

  19. Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol. 5663, pp. 67–83. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  20. Tushkanova, E., Ringeissen, C., Giorgetti, A., Kouchnarenko, O.: Automatic decidability: A schematic calculus for theories with counting operators. In: Proceedings the RTA 2013 (to appear, 2013)

    Google Scholar 

  21. Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, ch. 27, pp. 1965–2012. Elsevier (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University Koblenz-Landau and Max-Planck-Institut für Informatik, Saarbrücken, Germany

    Matthias Horbach & Viorica Sofronie-Stokkermans

Authors
  1. Matthias Horbach
    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. LORIA, Inria Nancy Grand Est, Université de Lorraine, 615 rue du Jardin Botanique, 54602, Villers-les-Nancy, France

    Pascal Fontaine

  2. LORIA, Inria Nancy Grand Est, 615 rue du Jardin Botanique, 54602, Villers-lès-Nancy, France

    Christophe Ringeissen

  3. School of Computer Science, The University of Manchester, Oxford Rd, Kilburn Building, M13 9PL, Manchester, UK

    Renate A. Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Horbach, M., Sofronie-Stokkermans, V. (2013). Obtaining Finite Local Theory Axiomatizations via Saturation. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds) Frontiers of Combining Systems. FroCoS 2013. Lecture Notes in Computer Science(), vol 8152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40885-4_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40885-4_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40884-7

  • Online ISBN: 978-3-642-40885-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation