Computer-Supported Exploration of a Categorical Axiomatization of Modeloids

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

Lucca Tiemens, Miroslav Benda, Christoph Benzmüller, Dana S. 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

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

Related Items (1)

Category theory in Isabelle/HOL as a basis for meta-logical investigation

Uses Software

• Sledgehammer
• Unnamed Item
• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Elements of finite model theory.
• Isabelle/HOL. A proof assistant for higher-order logic
• Automating free logic in HOL, with an experimental application in category theory
• Extending Sledgehammer with SMT solvers
• Modeloids. I
• Free Logic
• On inverse categories and transfer in cohomology
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

This page was built for publication: Computer-Supported Exploration of a Categorical Axiomatization of Modeloids