Top

Published in:

2018 | OriginalPaper | Chapter

FORT 2.0

Authors : Franziska Rapp, Aart Middeldorp

Published in: Automated Reasoning

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter A Tableaux Calculus for Reducing Proof Size

next chapter Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

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

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

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

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

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

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

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

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.003MathSciNetCrossRefMATH

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_49CrossRef

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

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

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_8CrossRef

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)

Title: FORT 2.0
Authors: Franziska Rapp
Aart Middeldorp
Publisher: Springer International Publishing
Book: Automated Reasoning
Print ISBN: 978-3-319-94204-9

Electronic ISBN: 978-3-319-94205-6

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-94205-6_6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner