Ionuţ Ţuţu
Simion Stoilow Institute of Mathematics of the Romanian Academy, Bucharest, Romania

Originally developed by James Slagle (1974) and Dallas Lankford (1975), narrowing has been a staple of equational logic programming for nearly half a century. The method is a refinement of paramodulation, another prominent inference rule for equational reasoning introduced by George Robinson and Lawrence Wos a few years earlier. Both are used for solving queries in first-order logics with equality, and both are known to be sound and complete -- under different assumptions. However, narrowing is often more advantageous in practice because it leads to a much smaller search space.

In this talk, we re-examine narrowing from an algebraic perspective following Virgil Căzănescu's approach to programming via rewriting and we show how the method can be used for computing solutions modulo axioms to equational queries in order-sorted algebra. In this process, we also give a new rewriting-based implementation of narrowing that can be easily adapted to other equational formalisms.