Title :
Subtype inequalities
Author_Institution :
Inst. of Inf., Warsaw Univ., Poland
Abstract :
The satisfiability problem for subtype inequalities in simple types is studied. The naive algorithm that solves this problem runs in nondeterministic exponential time for every predefined poset of atomic subtypings the satisfiability problem for subtype inequalities is PSPACE-hard. On the other hand, it is proved that if the poset of atomic subtypings is a disjoint union of lattices, then the satisfiability problem for subtype inequalities is solvable in PTIME. This result covers the important special case of the unification problem that can be obtained when the atomic subtype relation is equality
Keywords :
computability; PSPACE-hard; PTIME; atomic subtype relation; atomic subtypings; nondeterministic exponential time; satisfiability problem; subtype inequalities; unification problem; Calculus; Informatics; Lattices; Polynomials; Upper bound;
Conference_Titel :
Logic in Computer Science, 1992. LICS '92., Proceedings of the Seventh Annual IEEE Symposium on
Conference_Location :
Santa Cruz, CA
Print_ISBN :
0-8186-2735-2
DOI :
10.1109/LICS.1992.185543
