Object Specification Logic

Publisher Website
Google Scholar
Abstract
A logic for specifying and reasoning about object classes and their instances (aspects) is presented and illustrated. This logic is an extension of a rather standard linear temporal, many-sorted, first-order predicate logic with equality. The extensions were designed to be as simple as possible while supporting the envisaged locality of arguments, object specialization and object aggregation. Objects are specified through their aspects. Each aspect establishes a local vocabulary (signature). The logic works at two levels: first, we can specify and prove assertions about a given object aspect in isolation (local reasoning), e.g. persons, patients or cars; second, we can specify interaction constraints and make inferences between aspects within the same community of objects (global reasoning), e.g. carry the theorems of persons onto patients (specialization inheritance) or carry the theorems of persons onto the aggregations of persons and cars (incorporation inheritance). Some reflection mechanisms are also shown to be sound: for instance what becomes true of persons because of the interactions between persons and cars. The proposed logic is given in an axiomatic style.
Keywords

This publication has 0 references indexed in Scilit: