Skip to main content
SpringerLink
Log in
Book cover

Ewa Orłowska on Relational Methods in Logic and Computer Science pp 371–402Cite as

A Reasoning System for Satisfiability of Diagrammatic Specifications

  • Chapter
  • First Online:

  • 213 Accesses

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 17))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   119.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD   159.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Note that the definition of atomic constraint corresponds to the definition of diagram in category theory (Barr and Wells 1999).

  2. 2.

    Note that \([\![{p}]\!]\) is a subset of graph homomorphisms from the set of graph homomorphisms with any graph O as source and with target \(\alpha ^{\varSigma }(p)\) .

References

  • Alloy Tools. (2017). Alloy Project website. Retrieved March 26, 2018, from http://alloytools.org/.

  • Allwein, G. & MacCaull, W. (2001). A Kripke semantics for the logic of Gelfand quantales. Studia Logica, 68(2), 173–228.

    Article  Google Scholar 

  • Atkinson, C. & Kühne, T. (2001). The essence of multilevel metamodeling. In M. Gogolla & C. Kobryn (Eds.), International Conference on the Unified Modeling Language (Vol. 2185, pp. 19–33). Lecture Notes in Computer Science. New York: Springer.

    Google Scholar 

  • Barr, M. & Wells, C. (1999). Category Theory for Computing Science (3rd ed.). Montreal: Les Publications CRM.

    Google Scholar 

  • Buszkowski, W. & Orłowska, E. (1995). Relational Formalization of Dependencies in Information Systems. Preprint.

    Google Scholar 

  • Calder, T. & Lamo, Y. (2016). A bottom up approach to model based program validation. In D. D. Ruscio, J. de Lara, & A. Pierantonio (Eds.), Proceedings of the \(2^{nd}\)Workshop on Flexible Model Driven Engineering (Vol. 1694, pp. 12–21). CEUR Workshop Proceedings. https://CEUR-WS.org.

  • Chen, P. P. (1976). The entity-relationship model–toward a unified view of data. ACM Transactions on Database Systems, 1(1), 9–36.

    Article  Google Scholar 

  • Courcelle, B. & Engelfriet, J. (2012). Graph Structure and Monadic Second-order Logic: A Language-Theoretic Approach. Cambridge: Cambridge University Press.

    Google Scholar 

  • Diskin, Z. (1997). Generalized Sketches as an Algebraic Graph-based Framework for Semantic Modeling and Database Design. Laboratory for Database Design, University of Latvia: FIS/LDBD-97-03.

    Google Scholar 

  • Diskin, Z. & Wolter, U. (2008). A diagrammatic logic for object-oriented visual modeling. Electronic Notes in Theoretical Computer Science, 203(6), 19–41.

    Article  Google Scholar 

  • Ehrig, H., Ehrig, K., Prange, U., & Taentzer, G. (2006). Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science, an EATCS series. Berlin: Springer.

    Google Scholar 

  • Konikowska, B. & Białasik, M. (1999). Reasoning with first order nondeterministic specifications. Acta Informatica, 36(5), 375–403.

    Article  Google Scholar 

  • Lambers, L. & Orejas, F. (2014). Tableau-based reasoning for graph properties. In H. Giese & B. König (Eds.), Graph Transformation–7th International Conference, ICGT 2014, held as part of STAF 2014, York, UK, July 22–24, 2014. Proceedings (Vol. 8571, pp. 17–32). Lecture Notes in Computer Science. New York: Springer.

    Google Scholar 

  • Lamo, Y. & Walicki, M. (2006). Quantifier-free logic for nondeterministic theories. Theoretical Computer Science, 355(2), 215–227.

    Article  Google Scholar 

  • Lamo, Y., Wang, X., Mantz, F., MacCaull, W., & Rutle, A. (2012). DPF workbench: A diagrammatic multi-layer domain specific (meta-)modelling environment. In R. Lee (Ed.), Computer and Information Science 2012 (Vol. 429, pp. 37–52). Berlin: Springer.

    Chapter  Google Scholar 

  • MacCaull, W. (1997). Relational proof system for linear and other substructural logics. Logic Journal of IGPL, 5(5), 673–697.

    Article  Google Scholar 

  • MacCaull, W. (1998a). Relational semantics and a relational proof system for full Lambek calculus. The Journal of Symbolic Logic, 63(2), 623–637.

    Article  Google Scholar 

  • MacCaull, W. (1998b). Relational tableaux for tree models, language models and information networks. In E. Orłowska (Ed.), Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa. Heidelberg: Physica.

    Google Scholar 

  • MacCaull, W. (2000). A proof system for dependencies for information relations. Fundamenta Informaticae, 42(1), 1–27.

    Google Scholar 

  • MacCaull, W. & Orłowska, E. (2002). Correspondence results for relational proof systems with applications to the Lambek calculus. Studia Logica, 71(3), 389–414.

    Article  Google Scholar 

  • MacCaull, W. & Orłowska, E. (2006). A logic of typed relations and its applications to relational databases. Journal of Logic and Computation, 16(6), 789–815.

    Article  Google Scholar 

  • Makkai, M. (1997). Generalized sketches as a framework for completeness theorems. Part I. Journal of Pure and Applied Algebra, 115(1), 49–79.

    Article  Google Scholar 

  • Orejas, F. (2011). Symbolic graphs for attributed graph constraints. Journal of Symbolic Computation, 46(3), 294–315.

    Article  Google Scholar 

  • Orejas, F., Ehrig, H., & Prange, U. (2010). Reasoning with graph constraints. Formal Aspects of Computing, 22(3–4), 385–422.

    Article  Google Scholar 

  • Orłowska, E. (1992). Relational proof systems for relevant logics. Journal of Symbolic Logic, 57(4), 1425–1440.

    Article  Google Scholar 

  • Orłowska, E. (1994). Relational semantics for non-classical logics: Formulas are relations. In J. Woleński (Ed.), Philosophical Logic in Poland (pp. 167–186). Alphen aan den Rijn: Kluwer.

    Chapter  Google Scholar 

  • Orłowska, E. (1996). Relational proof systems for modal logics. In H. Wansing (Ed.), Proof Theory of Modal Logics (pp. 55–78). Berlin: Kluwer Academic Publishers.

    Google Scholar 

  • Orłowska, E. & Golińska-Pilarek, J. (2011). Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg-London-New York: Springer.

    Book  Google Scholar 

  • Rabbi, F., Lamo, Y., Yu, I. C., & Kristensen, L. M. (2015). A diagrammatic approach to model completion. In J. Dingel, S. Kokaly, L. Lucio, R. Salay, & H. Vangheluwe (Eds.), Proceedings of the \(4^{th}\)Workshop on the Analysis of Model Transformations (Vol. 1500, pp. 56–65). CEUR Workshop Proceedings. http://CEUR-WS.org.

  • Rabbi, F., Lamo, Y., & Yu, I. C. (2016a). Towards a categorical approach for metamodelling epistemic game theory. In Proceedings of the ACM/IEEE \(19^{th}\)International Conference on Model Driven Engineering Languages and Systems (pp. 57–64). New York City: ACM.

    Google Scholar 

  • Rabbi, F., Lamo, Y., Yu, I. C., & Kristensen, L. M. (2016b). Diagrammatic development of domain specific modelling languages with WebDPF. International Journal of Information System Modeling and Design, 7(3), 93–114.

    Article  Google Scholar 

  • Rasiowa, H. & Sikorski, R. (1963). The Mathematics of Metamathematics. Warsaw: Polish Scientific Publishers.

    Google Scholar 

  • Rensink, A. (2004). Representing first-order logic using graphs. In H. Ehrig, G. Engels, F. Parisi-Presicce, & G. Rozenberg (Eds.), International Conference on Graph Transformation (Vol. 3256, pp. 319–335). Lecture Notes in Computer Science. Berlin: Springer.

    Google Scholar 

  • Rossini, A., Rutle, A., Lamo, Y., & Wolter, U. (2010). A formalisation of the copymodify- merge approach to version control in MDE. The Journal of Logic and Algebraic Programming, 79(7), 636–658.

    Article  Google Scholar 

  • Routley, R. & Meyer, R. (1973). The semantics of entailment. In H. Leblanc (Ed.), Truth, Syntax and Modality (Vol. 68, pp. 199–243). Studies in Logic and the Foundations of Mathematics. New York: Elsevier.

    Chapter  Google Scholar 

  • Rumbaugh, J., Jacobson, I., & Booch, G. (2004). The Unified Modeling Language Reference Manual. Pearson Higher Education.

    Google Scholar 

  • Rutle, A. (2010). Diagram Predicate Framework: A Formal Approach to MDE. Doctoral dissertation, Department of Informatics, University of Bergen.

    Google Scholar 

  • Rutle, A., MacCaull,W.,Wang, H., & Lamo, Y. (2012). A metamodelling approach to behavioural modelling. In Proceedings of the\(4^{th}\)Workshop on Behaviour Modelling-foundations and Applications. New York City: ACM.

    Google Scholar 

  • Rutle, A., Rabbi, F., MacCaull, W., & Lamo, Y. (2013). A user-friendly tool for model checking healthcare workflows. Procedia Computer Science, 21, 317–326.

    Article  Google Scholar 

  • Rutle, A., Rossini, A., Lamo, Y., & Wolter, U. (2009). A diagrammatic formalization of MOF-based modelling languages. In M. Oriol & B. Meyer (Eds.), International Conference on Objects, Components, Models and Patterns (Vol. 33, pp. 37–56). Lecture Notes in Business Information Processing. Berlin: Springer.

    Chapter  Google Scholar 

  • Soley, R. (2000, November 20). Model Driven Architecture. Retrieved from https://www.omg.org/~soley/mda.html.

  • Steinberg, D., Budinsky, F., Merks, E., & Paternostro, M. (2008). EMF: Eclipse Modeling Framework. Hoboken: Addison-Wesley Professional.

    Google Scholar 

  • Vaziri, M. & Jackson, D. (2000). Some shortcomings of OCL, the object constraint language of UML. In \(34^{th}\)International Conference on Technology of Object-oriented Languages and Systems (pp. 555–562). IEEE.

    Google Scholar 

  • Wang, X., Büttner, F., & Lamo, Y. (2014). Verification of graph-based model transformations using Alloy. Electronic Communications of the EASST, 67.

    Google Scholar 

  • Wang, X., Rutle, A., & Lamo, Y. (2015). Towards user-friendly and efficient analysis with Alloy. In M. Famelis, D. Ratiu, M. Seidl, & G. M. K. Selim (Eds.), Proceedings of the 12\(^{th}\) Workshop on Model-driven Engineering, Verification and Validation (Vol. 1514, pp. 28–37). CEUR Workshop Proceedings. http://CEUR-WS.org

Download references

Acknowledgements

This paper is the result of discussions initiated when the first author visited StFX in 2013 as “Heaps Chair in Computer Science”. The second author acknowledges support from the Natural Sciences and Engineering Research Council of Canada.

Author information

Authors and Affiliations

  1. Western Norway University of Applied Sciences, Inndalsveien 28, 5063, Bergen, Norway

    Yngve Lamo

  2. St. Francis Xavier University, Antigonish, NS, B2G 2W5, Canada

    Wendy MacCaull

Authors
  1. Yngve Lamo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wendy MacCaull
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yngve Lamo .

Editor information

Editors and Affiliations

  1. Institute of Philosophy, University of Warsaw, Warsaw, Poland

    Joanna Golińska-Pilarek

  2. Department of Logic and Methodology of Science, University of Lodz, Łódź, Poland

    Michał Zawidzki

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Lamo, Y., MacCaull, W. (2018). A Reasoning System for Satisfiability of Diagrammatic Specifications. In: Golińska-Pilarek, J., Zawidzki, M. (eds) Ewa Orłowska on Relational Methods in Logic and Computer Science. Outstanding Contributions to Logic, vol 17. Springer, Cham. https://doi.org/10.1007/978-3-319-97879-6_15

Download citation

Publish with us

Policies and ethics

Search

Navigation