Skip to main content
SpringerLink
Log in

FORT 2.0

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

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

Included in the following conference series:

Abstract

FORT is a tool that implements the first-order theory of rewriting for the decidable class of left-linear right-ground rewrite systems. It can be used to decide properties of a given rewrite system and to synthesize rewrite systems that satisfy arbitrary properties expressible in the first-order theory of rewriting. In this paper we report on the extensions that were incorporated in the latest release (2.0) of FORT. These include witness generation for existentially quantified variables in formulas, support for combinations of rewrite systems, as well as an extension to deal with non-ground terms for properties related to confluence.

This research is supported by FWF (Austrian Science Fund) project P30301.

F. Rapp—Currently at Allgemeines Rechenzentrum Innsbruck.

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 EPUB and 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

Notes

  1. 1.

    http://cl-informatik.uibk.ac.at/software/FORT.

  2. 2.

    https://www.win.tue.nl/~hzantema/carpa.html.

  3. 3.

    http://cops.uibk.ac.at/.

  4. 4.

    Version 1.2 released on January 17, 2018; comparing FORT with version 1.1 of CoLL brought several bugs to light in the latter.

References

  1. Aoto, T., Toyama, Y.: Ground confluence prover based on rewriting induction. In: Proceedings 1st FSCD. LIPIcs, vol. 52, pp. 33:1–33:12 (2016). https://doi.org/10.4230/LIPIcs.FSCD.2016.33

  2. Aoto, T., Toyama, Y., Kimura, Y.: Improving rewriting induction approach for proving ground confluence. In: Proceedings 2nd FSCD. LIPIcs, vol. 84, pp. 7:1–7:18 (2017). https://doi.org/10.4230/LIPIcs.FSCD.2017.7

  3. Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: Proceedings 5th LICS, pp. 242–248 (1990). https://doi.org/10.1109/LICS.1990.113750

  4. Durand, I., Middeldorp, A.: Decidable call-by-need computations in term rewriting. Inf. Comput. 196(2), 95–126 (2005). https://doi.org/10.1016/j.ic.2004.10.003

    Article  MathSciNet  MATH  Google Scholar 

  5. Middeldorp, A.: Approximating dependency graphs using tree automata techniques. In: Proceedings 1st IJCAR. LNAI, vol. 2083, pp. 593–610 (2001). https://doi.org/10.1007/3-540-45744-5_49

    Chapter  Google Scholar 

  6. Rapp, F., Middeldorp, A.: Automating the first-order theory of left-linear right-ground term rewrite systems. In: Proceedings 1st FSCD. LIPIcs, vol. 52, pp. 36:1–36:12 (2016). https://doi.org/10.4230/LIPIcs.FSCD.2016.36

  7. Rapp, F., Middeldorp, A.: Confluence properties on open terms in the first-order theory of rewriting. In: Proceedings 5th IWC, pp. 26–30 (2016)

    Google Scholar 

  8. Shintani, K., Hirokawa, N.: CoLL: a confluence tool for left-linear term rewrite systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 127–136. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_8

    Chapter  Google Scholar 

  9. Sternagel, C., Sternagel, T.: Certifying confluence of almost orthogonal CTRSs via exact tree automata completion. In: Proceedings 1st FSCD. LIPIcs, vol. 52, pp. 29:1–29:16 (2016). https://doi.org/10.4230/LIPIcs.FSCD.2016.29

  10. Zantema, H.: Automatically finding non-confluent examples in term rewriting. In: Proceedings 2nd IWC, pp. 11–15 (2013)

    Google Scholar 

Download references

Acknowledgments

We are grateful to Bertram Felgenhauer, Nao Hirokawa, and Julian Nagele for their support with the experiments. The comments by the anonymous reviewers helped to improve the presentation.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Innsbruck, Innsbruck, Austria

    Franziska Rapp & Aart Middeldorp

Authors
  1. Franziska Rapp
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aart Middeldorp
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Aart Middeldorp .

Editor information

Editors and Affiliations

  1. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Rapp, F., Middeldorp, A. (2018). FORT 2.0. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94204-9

  • Online ISBN: 978-3-319-94205-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation