Description

FORT is a decision and synthesis tool for the first-order theory of rewriting with respect to left-linear right-ground term rewrite systems.

News

• 26 June 2020   FORT-h released
• 19 April 2019   Version 2.1 released
• 20 August 2018   Version 2.0 corrected (bug in synthesis).
• 29 January 2018   Version 2.0 released (correction on 7 March 2018).
• 30 August 2016   Version 1.0 released (correction on 10 May 2017).
• 29 June 2016   Version 0.2 released.
• 28 April 2016   Version 0.1 released (correction on 18 June 2016).

Download

FORT-h is available as statically linked precompiled binary for Linux. FORT 1.0, 2.0 and 2.1 are available as executable JAR file. FORT 0.1 and 0.2 are available as statically linked precompiled binaries for Linux, MacOS, and Windows.

• FORT-h 0.9

  • executable binary file
  • the usage is explained in description.txt

• FORT 2.1

  • executable JAR file

  FORT 2.0

  • executable JAR file
  • the usage is explained in description.txt

• FORT 1.0

  • executable JAR file
  • the usage is explained in description.txt

• FORT 0.2

  • binaries for Linux, MacOS, and Windows
  • the usage is explained in description.txt

• FORT 0.1

  • binaries for Linux, MacOS, and Windows
  • the usage is explained in description.txt

• Database

  • The 121 left-linear right-ground rewrite systems extracted from version 765 of the Confluence Problems database (COPS) with function symbols consistently renamed.
  • A text file with formulas in FORT syntax corresponding to synthesis tasks solved by Carpa(+).
  • A collection of 65 left-linear right-ground rewrite systems, extracted from the Confluence Problems database (COPS) and the Termination Problems database (TPDB, version 10.3).

Experiments

• FORT 2.0 vs AGCP v0.03
• FORT 2.0 vs CoLL 1.2

Publications

• F. Rapp and A. Middeldorp
  FORT 2.0
  Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018)
  LNAI 10900, pp. 81 – 88, 2018
  
• F. Rapp and A. Middeldorp
  Confluence Properties on Open Terms in the First-Order Theory of Rewriting
  Proceedings of the 5th International Workshop on Confluence (IWC 2016)
  pp. 26 – 30, 2016
• F. Rapp and A. Middeldorp
  Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
  Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
  LIPIcs 52, pp. 36:1 – 36:12, 2016

Contact

For questions or feedback please contact Franziska Rapp or Aart Middeldorp.