Room 327

Towards a verified tool for the first-order theory of left-linear and right-ground term rewriting systems

T V H Prathamesh

University of Innsbruck, Austria

*** NOTE -- 2 pm in room 327; change in schedule due to public lecture at 4 pm *** Rewriting is the theory of step-wise transformation of objects such as terms. Studying rewriting in the context of terms, has deep origins and applications that range from word problem in group theory to termination of functional programs. An interesting result that connects term writing to decision problems in logic is the decidability of the first-order theory of a class of term rewrite systems (called left-linear right-ground), by Dauchet-Tison Et Al in 1990. The decision procedure based on tree-automata techniques forms the basis for an automated tool FORT <cl-informatik.uibk.ac.at/software/FORT/>, written by Franziska Rapp, which can be used to decide many interesting properties expressible in first-order theory. The correctness of the output of FORT, however, remains a matter of trust in the large java code. In this talk, we shall describe the ongoing process and challenges of 'verifying' this automated tool, through means of formalizing the underlying theory in an interactive theorem prover called Isabelle/HOL. No prerequisites in term-writing, interactive theorem proving or tree automata theory shall be assumed.