A Calculus for Type Predicates and Type Coercion

We extend classical first-order logic with subtyping by type predicates and type coercion. Type predicates assert that the value of a term belongs to a more special type than the signature guarantees, while type coercion allows using terms of a more general type where the signature calls for a more special one. These operations are important e.g. in the specification and verification of object-oriented programs. We present a tableau calculus for this logic and prove its completeness.

• Type: Conference
• Year: 2005
• Where: TABLEAUX
• Authors: Martin Giese
• Keywords: Artificial Intelligence, TABLEAUX 2005, Type Coercion, Type Predicates, Type Predicates Assert