Rewriting properties of combinators for intuitionistic linear logic Export

@misc{citeulike:401390, abstract = {In this paper we investigate the possibility of developing a (semi-)automatic rewriting tool for manipulating and reasoning about combinators for Intuitionistic Linear Logic. In particular, we develop a canonical (i.e. confluent and terminating) term rewriting system associated to a theory of categorical combinators for (rudimentary) Linear Logic. In order to do that, we make use of the Knuth-Bendix completion algorithm [3] to transform the equational theory for the combinators into an equivalent...}, author = {Nesi, M. and de Paiva, V. and Ritter, E.}, citeulike-article-id = {401390}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.9297}, keywords = {combinators, intuitionistic, linear, logic, own}, posted-at = {2005-11-19 17:14:25}, priority = {0}, title = {Rewriting properties of combinators for intuitionistic linear logic}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.9297}, year = {1994} }

TY - GEN ID - citeulike:401390 L3 - citeulike-article-id:401390 N2 - In this paper we investigate the possibility of developing a (semi-)automatic rewriting tool for manipulating and reasoning about combinators for Intuitionistic Linear Logic. In particular, we develop a canonical (i.e. confluent and terminating) term rewriting system associated to a theory of categorical combinators for (rudimentary) Linear Logic. In order to do that, we make use of the Knuth-Bendix completion algorithm [3] to transform the equational theory for the combinators into an equivalent... TI - Rewriting properties of combinators for intuitionistic linear logic KW - combinators KW - intuitionistic KW - linear KW - logic KW - own AU - Nesi, M AU - de Paiva, V AU - Ritter, E PY - 1994/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.9297 ER -