Meyer, Gregor On types and type consistency in logic programming (Diss., FernUniv. Hagen, 1999). (English) Zbl 0978.68036 DISKI - Dissertationen zur Künstlichen Intelligenz. 235. Amsterdam: IOS Press. Berlin: Akademische Verlags-Gesellschaft Aka/ infix. 176 p. (2000). The objective of this thesis is to add a type system to logic programming that allows a compiler to find automatically as many programming errors as possible by static analysis, fits well with the declarative and non-procedural nature of logic programs, is expressive enough to support rich modelling and various programming techniques, and, additionally, is applicable to standard Prolog, incl. its non-logical features. A summary from the back cover: “This thesis investigates various aspects of using types in logic programming. These are classified into three dimensions: types for proving partial correctness, types as constraints, and types as approximations. Type checking for languages with hierarchies of both features types and constructor types is presented. Based on the notion of type consistency, a general method for the detection of useless expressions is developed. It is implemented in the Typical system that supports expressive type annotations including subtypes and parametric polymorphism. Type checking and type inferencing algorithms for Typical are defined, which, for example, implement automatic detection of type errors in standard Prolog programs enriched with type annotations.” The content of the thesis, briefly: Ch. 1 is a brief introduction. Ch. 2 discusses three dimentions of typing in logic programming. Ch. 3 presents polymorphic feature types. Ch. 4 reconsiders type constraints. Ch. 5 discusses types as approximations and consistency annotations. Ch.6 studies type consistency with subtypes and parametric polymorphisms. Ch. 7 is devoted to type inferencing. The last ch. 8 contains conclusions and summary. The thesis ends with appendices with basic definitions and terminology and presents the grammar for type definitions in LOT syntax. Reviewer: Valentin F.Goranko (Johannesburg) MSC: 68N17 Logic programming 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 03B70 Logic in computer science 68-02 Research exposition (monographs, survey articles) pertaining to computer science Keywords:logic programming; types; type errors; type consistency; type constraints; type inference; parametric polymorphism; standard Prolog PDFBibTeX XMLCite \textit{G. Meyer}, On types and type consistency in logic programming (Diss., FernUniv. Hagen, 1999). Amsterdam: IOS Press; Berlin: Akademische Verlags-Gesellschaft Aka/ infix (2000; Zbl 0978.68036)