Title
Unification and Matching in Hierarchical Combinations of Syntactic Theories
Abstract
We investigate a hierarchical combination approach to the unification problem in non-disjoint unions of equational theories. In this approach, the idea is to extend a base theory with some additional axioms given by rewrite rules in such way that the unification algorithm known for the base theory can be reused without loss of completeness. Additional techniques are required to solve a combined problem by reducing it to a problem in the base theory. In this paper we show that the hierarchical combination approach applies successfully to some classes of syntactic theories, such as shallow theories since the required unification algorithms needed for the combination algorithm can always be obtained. We also consider the matching problem in syntactic extensions of a base theory. Due to the more restricted nature of the matching problem, we obtain several improvements over the unification problem.
Year
DOI
Venue
2015
10.1007/978-3-319-24246-0_18
Lecture Notes in Artificial Intelligence
Field
DocType
Volume
Discrete mathematics,Computer science,Axiom,Unification,Algorithm,Rule of inference,Syntax,Completeness (statistics),Equational theory
Conference
9322
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
12
5
Name
Order
Citations
PageRank
Serdar Erbatur1205.35
Deepak Kapur22282235.00
Andrew M. Marshall385.07
Paliath Narendran41100114.99
Christophe Ringeissen565149.35