A Reasoning System for Satisfiability of Diagrammatic Specifications

Diagrammatic modelling is the foundation of many popular knowledge representation and software development techniques. In Model Driven Software Engineering, domain specific modelling languages are represented as metamodels and domain specific specifications are represented as models. The (meta-)models are represented by graphs and (models) instances are represented by graphs typed by the (meta)model. The typing relation is formalised by graph homomorphisms. Constraints are used to further specify the semantics of models. The state of the art modelling techniques of today have limited support for expressing and reasoning about diagrammatic constraints; constraints are usually expressed in an external textual language, not fully integrated in the metamodelling process. The diagram predicate framework, DPF is a fully diagrammatic meta modelling technique where one can express arbitrary diagrammatic constraints in the form of predicates on graphs. In this paper we build on ideas, successfuly exploited in a variety of logical systems by Orłowska and collaborators, to build a logical reasoning system for diagrammatic specifications. We enrich the expressiveness of DPF specifications to include semantic dependencies between DPF constraints and present a sound and complete reasoning system using a dual tableaux deduction system to determine if DPF specifications are satisfiable. We briefly discuss an extension of the reasoning system which uses the relational approach to encode the existence of certain graph homomorphisms and provide deduction rules to account for necessary properties of these homomorphisms.