On Rewriting Rules in Mizar
This paper presents some tentative experiments in using a special case of rewriting rules in Mizar (Mizar homepage:http://www.mizar.org/): rewriting a term as its subterm. A similar technique, but based on another Mizar mechanism called functor identification (Kornilowicz 2009) was used by Caminati, in his paper on basic first-order model theory in Mizar (Caminati, J Form Reason 3(1): 49-77, 2010, Form Math 19(3): 157-169, 2011). However for this purpose he was obligated to introduce some artificial functors. The mechanism presented in the present paper looks promising and fits the Mizar paradigm.
mizar proof assistant natural deduction computer algebra system term rewriting