Structure sharing for quantified terms: Fundamentals

Staples J. and Robinson P.J. (1990) Structure sharing for quantified terms: Fundamentals. Journal of Automated Reasoning, 6 2: 115-145. doi:10.1007/BF00245815

Author Staples J.
Robinson P.J.
Title Structure sharing for quantified terms: Fundamentals
Journal name Journal of Automated Reasoning   Check publisher's open access policy
ISSN 0168-7433
Publication date 1990-01-01
Sub-type Article (original research)
DOI 10.1007/BF00245815
Open Access Status Not yet assessed
Volume 6
Issue 2
Start page 115
End page 145
Total pages 31
Publisher Kluwer Academic Publishers
Language eng
Subject 1702 Cognitive Sciences
Abstract Structure sharing is used in symbolic computation to share a common top level between terms with different lower levels. It is widely used in the implementation of Prolog interpreters and is of interest for the implementation of automatic theorem provers, interactive proof editors and verification systems. Previously, structure sharing has been applied only to free-variable terms. In this paper we extend the structure sharing technique to quantified terms. We give an efficient unification algorithm of our structure sharing representation of quantified terms, and we prove the correctness of the algorithm.
Keyword logic programming
quantified terms
Structure sharing
theorem proving
verification systems
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status Unknown

Document type: Journal Article
Sub-type: Article (original research)
Collection: Scopus Import - Archived
Version Filter Type
Citation counts: Scopus Citation Count Cited 1 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Tue, 26 Jul 2016, 14:17:31 EST by System User