Sorting information arises naturally in E-unification problems. This information is used to rule out invalid solutions. We show how to use sorting information to make E-unification procedures more efficient. We illustrate our ideas using Basic Syntactic Mutation. We give classes of problems where E-unification becomes polynomial. We show how E-unification can be separated into a polynomial part and a more complicated part using a specialized algorithm. Our approach is motivated by a real problem arising from Cryptographic Protocol Verification. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Lynch, C., & Morawska, B. (2005). Faster Basic Syntactic Mutation with sorts for some separable equational theories. In Lecture Notes in Computer Science (Vol. 3467, pp. 90–104). Springer Verlag. https://doi.org/10.1007/978-3-540-32033-3_8
Mendeley helps you to discover research relevant for your work.