The E-Unification problem appears in important application areas, e.g. automated deduction and cryptographic protocol analysis. As E-Unification is undecidable in general, there is an active search for decidable and, ideally, tractable instances of the problem.
In this dissertation we investigate a class of equational theories, which we call LM-Systems, that give rise to E-Unification problems solvable in polynomial time. This remarkable class of theories was first discovered by Dr. Christopher Lynch and Dr. Barbara Morawska in their paper ``Basic Syntactic Mutation". We adapt their definitions to convergent and forward-closed term-rewriting systems, and show that LM-Systems are highly restrictive. However, we also prove that the Cap Problem, a known undecidable problem from the field of cryptographic protocol analysis, remains undecidable when restricted to LM-Systems.
Motivated by the definition of LM-Systems, we next investigate the case of forward-closed and convergent string-rewriting systems. We show that the Subterm Collapse problem, which is undecidable for general convergent term-rewriting systems, becomes decidable when restricted to these systems. In particular, there is an algorithm to determine if such a string-rewriting system is an LM-System.
Finally, we show that the Finiteness of Forward-Closure problem, which is undecidable in general, is decidable for convergent and monadic string-rewriting systems.
|Commitee:||Lynch, Christopher, Murray, Neil|
|School:||State University of New York at Albany|
|School Location:||United States -- New York|
|Source:||DAI-B 79/10(E), Dissertation Abstracts International|
|Keywords:||LM-systems, Term rewriting, Unification|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be