ملخص: In this volume the logical foundations and the computational aspects of a rather general order-sorted logic are investigated. This sorted logic extends first order logic by a partially ordered set of sorts, such that every term is of a particular sort or type and such that only well-sorted substitutions are permitted. Several sorted unification algorithms are described which work for different signatures with or without equational theories. The type and the complexity of sorted unification is determined for different types of signatures. The type can range from unary to infinitary and the time complexity ranges from linear up to undecidable, even without defining equations. Different sorted resolution-based calculi for clause sets with and without equations are described and their refutation-completeness is investigated.

طبعة: Berlin: Springer-Verlag Springer-Verlag
لغة: إنجليزية
الوصف المادي: 171 p. ;24 cm
ISBN: 3540517057