A TYPE SYSTEM FOR THE OBJECT ORIENTED LOGIC LANGUAGE LKO

The ordered type system based on type declaration and type inference is presented for the object oriented logic language LKO. The types in predicate declarations are built by ordered constructors, which results in natural subtyping relationship. The types of variables in clauses are inferred by the system. Objects are classified in terms of method declarations, so inheritance is independent of subtyping. As base types, classes may be applied in complex type construction.