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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Agron, P., Bachmair, L., & Nielsen, F. (2005). A visual interactive framework for formal derivation. In Lecture Notes in Computer Science (Vol. 3514, pp. 1019–1026). Springer Verlag. https://doi.org/10.1007/11428831_127
Mendeley helps you to discover research relevant for your work.