Computer-supported exploration of a categorical axiomatization of modeloids

DOI10.1007/978-3-030-43520-2_19OpenAlexW3013127010MaRDI QIDQ5098730FDOQ5098730

Authors: Lucca Tiemens, Christoph Benzmüller, Miroslav Benda, Dana Scott 

Publication date: 30 August 2022

Published in: Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1910.12863

Recommendations

• scientific article; zbMATH DE number 3934440
• Model theory in additive categories
• scientific article; zbMATH DE number 1924507
• Morphism axioms
• The pebbling comonad in finite model theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Basic properties of first-order languages and structures (03C07) Formalization of mathematics in connection with theorem provers (68V20) Inverse semigroups (20M18) Foundations, relations to logic and deductive systems (18A15) Model theory (03C99)

Cites Work

• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Free Logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Elements of finite model theory.
• Extending Sledgehammer with SMT solvers
• Title not available (Why is that?)
• Title not available (Why is that?)
• On inverse categories and transfer in cohomology
• Automating free logic in HOL, with an experimental application in category theory
• Modeloids. I

Cited In (2)

• Relational calculus as a formal system
• Category theory in Isabelle/HOL as a basis for meta-logical investigation

Uses Software

• Nitpick
• Isabelle/HOL
• Sledgehammer

This page was built for publication: Computer-supported exploration of a categorical axiomatization of modeloids

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5098730)