On Rewriting Rules in Mizar
Artur Korniłowicz · Journal of Automated Reasoning · 2012
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 (Korniłowicz 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.