June 1, 2017: FWF project “FORTissimo: Automating the First-Order Theory of Rewriting” approved

In its 63rd board meeting the Austrian Science Fund (FWF) approved Aart Middeldorp’s project proposal. The 3-year project will start on September 1 and has a grant amount of EUR 345K.

FORTissimo is about the first-order theory of rewriting, which is a decidable theory for left-linear right-ground rewrite systems in which well-known properties like confluence, normalization and termination are expressible. The decision procedure for this theory is based on tree automata techniques and a first implementation was conducted by Franziska Rapp. The resulting tool FORT is equipped with a synthesis mode to generate rewrite systems that satisfy properties expressible in the first-order theory of rewriting.

The aim of FORTissimo is to formalize the decision procedure in the proof assistant Isabelle/HOL such that the output of FORT can be certified. Moreover, the expressiveness and the performance of FORT will be increased, and its limitations better understood.