A Visual Interactive Framework for Formal Derivation

We describe a visual interactive framework that supports the computation of syntactic unifiers of expressions with variables. Unification is specified via built-in transformation rules. A user derives a solution to a unification problem by stepwise application of these rules. The software tool provides both a debugger-style presentation of a derivation and its history, and a graphical view of the expressions generated during the unification process. A backtracking facility allows the user to revert to an earlier step in a derivation and proceed with a different strategy.

• Type: Conference
• Year: 2005
• Where: ICCS
• Authors: Paul Agron, Leo Bachmair, Frank Nielsen
• Keywords: Built-in Transformation Rules, ICCS 2005, Syntactic Unifiers, Visual Interactive Framework