Thesis icon

Thesis

Parallel algorithms for free and associative-commutative unification

Abstract:

A survey of algorithms for free unification is given, followed by an overview of the computability and complexity of unification problems. Second-order unification is known to be undecidable, and a proof is given that the first-order problem is also undecidable under an arbitrary set of axioms. A new systolic algorithm is introduced for term minimisation or term compaction. This is a general-purpose tool for systems using structure sharing. Apart from time and space savings, its use allows s...

Expand abstract

Actions


Access Document


Files:

Authors


More by this author
Institution:
University of Oxford
Research group:
Programming Research Group
Oxford college:
Wolfson College
Department:
Mathematical,Physical & Life Sciences Division - Computing Laboratory

Contributors

Role:
Supervisor
Publication date:
1989
Type of award:
DPhil
Level of award:
Doctoral
URN:
uuid:84d44899-a98f-4015-8b72-9bde3a8fe426
Local pid:
ora:5627

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP