Skip to main content
SpringerLink
Log in

Computer-Supported Exploration of a Categorical Axiomatization of Modeloids

  • Conference paper
  • First Online:
Relational and Algebraic Methods in Computer Science (RAMiCS 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12062))

Abstract

A modeloid, a certain set of partial bijections, emerges from the idea to abstract from a structure to the set of its partial automorphisms. It comes with an operation, called the derivative, which is inspired by Ehrenfeucht-Fraïssé games. In this paper we develop a generalization of a modeloid first to an inverse semigroup and then to an inverse category using an axiomatic approach to category theory. We then show that this formulation enables a purely algebraic view on Ehrenfeucht-Fraïssé games.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

Institutional subscriptions

Notes

  1. 1.

    Sledgehammer [3] is linking interactive proof development in Isabelle/HOL with anonymous calls to various integrated automated theorem proving systems. Among others, the tool converts the higher-order problems given to it into first-order representations for the integrated provers, it calls them and analyses their responses, and it tries to identify minimal sets of dependencies for the theorems it proves this way.

  2. 2.

    See http://christoph-benzmueller.de/papers/RAMICSadditionalMaterial.zip.

  3. 3.

    nitpick [4] is a counterexample generator for higher-order logic integrated with Isabelle/HOL.

References

  1. Benda, M.: Modeloids. I. Trans. Am. Math. Soc. 250, 47–90 (1979). https://doi.org/10.1090/s0002-9947-1979-0530044-4

  2. Benzmüller, C., Scott, D.S.: Automating free logic in HOL, with an experimental application in category theory. J. Autom. Reason. 64(1), 53–72 (2020). https://doi.org/10.1007/s10817-018-09507-7

    Article  MathSciNet  MATH  Google Scholar 

  3. Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reasoning 51(1), 109–128 (2013). https://doi.org/10.1007/s10817-013-9278-5

    Article  MathSciNet  MATH  Google Scholar 

  4. Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_11

    Chapter  Google Scholar 

  5. Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-28788-4

  6. Howie, J.M.: Fundamentals of Semigroup Theory. Oxford University Press, Oxford (1995)

    Google Scholar 

  7. Kastl, J.: Inverse categories. Algebraische Modelle, Kategorien und Gruppoide 7, 51–60 (1979)

    MathSciNet  MATH  Google Scholar 

  8. Lambert, K.: The definition of e! in free logic. In: Abstracts: The International Congress for Logic, Methodology and Philosophy of Science. Stanford University Press, Stanford (1960)

    Google Scholar 

  9. Lambert, K.: Free Logic: Selected Essays. Cambridge University Press, Cambridge (2002)

    Google Scholar 

  10. Lawson, M.V.: Inverse Semigroups. World Scientific (1998). https://doi.org/10.1142/3645

  11. Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2013)

    MATH  Google Scholar 

  12. Linckelmann, M.: On inverse categories and transfer in cohomology. Proc. Edinburgh Math. Soc. 56(1), 187–210 (2012). https://doi.org/10.1017/s0013091512000211

  13. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

  14. Scott, D.: Existence and description in formal logic. In: Schoenman, R. (ed.) Bertrand Russell: Philosopher of the Century, pp. 181–200. George Allen & Unwin, London (1967). Reprinted with additions in: Lambert, K. (ed.) Philosophical Application of Free Logic, pp. 28–48. Oxford Universitry Press (1991)

    Google Scholar 

  15. Tiemens, L.: Computer-supported Exploration of a Categorical Axiomatization of Miroslav Benda’s Modeloids. Bachelor’s thesis, Freie Universität Berlin (2019). https://www.mi.fu-berlin.de/inf/groups/ag-ki/Theses/Completed-theses/Bachelor-theses/2019/Tiemens/BA-Tiemens2.pdf

  16. Tiemens, L., Scott, D.S., Benzmüller, C., Benda, M.: Computer-supported exploration of a categorical axiomatization of modeloids. ArXiv abs/1910.12863 (2019). https://arxiv.org/abs/1910.12863

Download references

Acknowledgment

We wish to thank the anonymous referees for their helpful comments and suggestions.

Author information

Authors and Affiliations

  1. Technische Universität Berlin, Berlin, Germany

    Lucca Tiemens

  2. University of California, Berkeley, CA, USA

    Dana S. Scott

  3. Freie Universität Berlin, Berlin, Germany

    Lucca Tiemens & Christoph Benzmüller

  4. University of Luxembourg, Esch-sur-Alzette, Luxembourg

    Christoph Benzmüller

  5. Formerly at University of Washington, Seattle, USA

    Miroslav Benda

Authors
  1. Lucca Tiemens
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dana S. Scott
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christoph Benzmüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Miroslav Benda
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lucca Tiemens .

Editor information

Editors and Affiliations

  1. Laboratoire d’informatique (LIX), École Polytechnique, Palaiseau, France

    Uli Fahrenberg

  2. Faculty of Mathematics, Chapman University, Orange, CA, USA

    Peter Jipsen

  3. Department of Computer Science, Brock University, St. Catharines, ON, Canada

    Michael Winter

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Tiemens, L., Scott, D.S., Benzmüller, C., Benda, M. (2020). Computer-Supported Exploration of a Categorical Axiomatization of Modeloids. In: Fahrenberg, U., Jipsen, P., Winter, M. (eds) Relational and Algebraic Methods in Computer Science. RAMiCS 2020. Lecture Notes in Computer Science(), vol 12062. Springer, Cham. https://doi.org/10.1007/978-3-030-43520-2_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-43520-2_19

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-43519-6

  • Online ISBN: 978-3-030-43520-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation