Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2011: Formal Methods and Software Engineering pp 633–650Cite as

Term Rewriting in Logics of Partial Functions

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6991))

Abstract

We devise a theoretical foundation of directed rewriting, a term rewriting strategy for logics of partial functions, inspired by term rewriting in the Rodin platform. We prove that directed rewriting is sound and show how to supply new rewrite rules in a soundness preserving fashion. In the context of Rodin, we show that directed rewriting makes a significant number of conditional rewrite rules unconditional. Our work not only allows us to point out a number of concrete ways of improving directed rewriting in Rodin, but also has applications in other logics of partial functions. Additionally, we give a semantics for the logic of Event-B.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.R.: Modeling in Event-B, Cambridge (2010)

    Google Scholar 

  2. Abrial, J.R., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447–466 (2010)

    Article  Google Scholar 

  3. Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory. Kluwer, Dordrecht (2002)

    MATH  Google Scholar 

  4. Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Inf. 21, 251–269 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  5. Butler, M., Maamria, I.: Mathematical extension in Event-B through the Rodin theory component (2010), http://deploy-eprints.ecs.soton.ac.uk/251

  6. Darvas, Á., Mehta, F., Rudich, A.: Efficient well-definedness checking. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 100–115. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  7. Dawson, J.E.: Simulating term-rewriting in LPF and in display logic. In: Supplementary Proc. of TPHOLs, pp. 47–62. Australian National University (1998)

    Google Scholar 

  8. Gordon, M.J.C., Melham, T.F.: Introduction to HOL, Cambridge (1993)

    Google Scholar 

  9. Hindley, J.R., Seldin, J.P.: Lambda-Calculus and Combinators, Cambridge (2008)

    Google Scholar 

  10. Jones, C.B., Middelburg, C.A.: A typed logic of partial functions reconstructed classically. Acta Inf. 31(5), 399–430 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  11. Maamria, I., Butler, M.: Rewriting and well-definedness within a proof system. In: PAR. EPTCS, vol. 43, pp. 49–64 (2010)

    Google Scholar 

  12. Mehta, F.: A practical approach to partiality – A proof based approach. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 238–257. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  13. Metayer, C., Voisin, L.: The Event-B mathematical language (2009), http://deploy-eprints.ecs.soton.ac.uk/11

  14. Nipkow, T.: Term rewriting and beyond - theorem proving in isabelle. Formal Asp. Comput. 1(4), 320–338 (1989)

    Article  MATH  Google Scholar 

  15. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  16. Owe, O.: Partial logics reconsidered: A conservative approach. Formal Asp. Comput. 5(3), 208–223 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  17. Owre, S., Shankar, N.: The formal semantics of PVS (1999), http://pvs.csl.sri.com/papers/csl-97-2/csl-97-2.ps

  18. Paulson, L.C.: Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge (1987)

    Google Scholar 

  19. Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reasoning 5(3), 363–397 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  20. Schmalz, M.: The logic of Event-B (2011), ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf

  21. Schmalz, M.: Term rewriting in logics of partial functions (2011), ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/7xx/732.pdf

  22. Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS prover guide (2001), http://pvs.csl.sri.com/doc/pvs-prover-guide.pdf

  23. Silva, R., Butler, M.: Supporting reuse of Event-B developments through generic instantiation. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 466–484. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  24. Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 307–322. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ETH Zurich, Switzerland

    Matthias Schmalz

Authors
  1. Matthias Schmalz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, Teesside University, UK

    Shengchao Qin

  2. LMAM and Department of Informatics, School of Mathematical Sciences,, Peking University, China

    Zongyan Qiu

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schmalz, M. (2011). Term Rewriting in Logics of Partial Functions. In: Qin, S., Qiu, Z. (eds) Formal Methods and Software Engineering. ICFEM 2011. Lecture Notes in Computer Science, vol 6991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24559-6_42

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24559-6_42

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24558-9

  • Online ISBN: 978-3-642-24559-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation