FORT 2.0

Franziska Rapp, Aart Middeldorp

Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 81 – 88, 2018.


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.


  PDF |    doi:10.1007/978-3-319-94205-6_6  |  © Springer International Publishing AG  


author = "Franziska Rapp and Aart Middeldorp",
title = "{FORT} 2.0",
booktitle = "Proceedings of the 9th International Joint Conference on
Automated Reasoning (IJCAR 2019)",
editor = "Didier Galmiche and Stephan Schulz and Roberto Sebastiani",
series = "Lecture Notes in Artificial Intelligence",
volume = 10900,
pages = "81--88",
year = 2018,
doi = "10.1007/978-3-319-94205-6_6"
Nach oben scrollen