Computer-supported exploration of a categorical axiomatization of modeloids

DOI10.1007/978-3-030-43520-2_19MaRDI QIDQ5098730zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 3665176 (Why is no real title available?)
• scientific article; zbMATH DE number 1761434 (Why is no real title available?)
• scientific article; zbMATH DE number 789816 (Why is no real title available?)
• scientific article; zbMATH DE number 803291 (Why is no real title available?)
• Automating free logic in HOL, with an experimental application in category theory
• Elements of finite model theory.
• Extending Sledgehammer with SMT solvers
• Free Logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Modeloids. I
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• On inverse categories and transfer in cohomology

Cited in

(3)

• Computer-supported Exploration of a Categorical Axiomatization of Modeloids
• Relational calculus as a formal system
• Category theory in Isabelle/HOL as a basis for meta-logical investigation

Describes a project that uses

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)