Keyword:rewriting

Papers
A Knuth-Bendix-Like Ordering for Orienting Combinator Equations (Technical Report) Ahmed Bhayat and Giles Reger EasyChair Preprint no. 3191
A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo Guillaume Burel In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Initial Experiments on Deriving a Complete HOL Simplification Set Cezary Kaliszyk and Thomas Sternagel In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving