A Typed Hybrid Description Logic Programming Language with Polymorphic Order-Sorted DL-Typed Unification for Semantic Web Type Systems

In the recent years rule-based programming in terms of decla rative logic programming has formed the basis for many Artificial In telligence (AI) applications and is well integrated in the mainstream infor mation technology capturing higher-level decision logics. Typically, the st andard rule systems and rule-based logic programming languages such as Prolog deri vatives are based on the untyped theory of predicate calculus with untyped logic al objects (untyped terms), i.e. the logical reasoning algorithms apply pure sy ntactical reasoning. From a rule engineering perspective this is a serious restri ction which lacks major Software Engineering principles such as data abstracti on or modularization, which become more and more important when rule applications grow larger and more complex. To support such principles in logic programmi ng and capture the rule engineer's intended meaning of a logic program, types a nd typed objects play an important role. Moreover, from a computational poin t of view, the use of types drastically reduces the search space, i.e. proofs c an be kept at a more abstract level and it offers the option to restrict the applic ation of rules and to control the level of generality in queries.