Formalising basic topology for computational logic in simple type theory

DOI10.1007/978-3-031-16681-5_4MaRDI QIDQ6159367OpenAlexFDO

Authors David Fuenmayor, Fabián Fernando Serrano Suárez

Publication date 2 June 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-16681-5_4

zbMATH Keywords

topologyIsabelle/HOLsimple type theoryclosure algebras

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Recommendations

• Toposes and intuitionistic theories of types
• scientific article; zbMATH DE number 810107
• Topological interpretations of provability logic
• Simple Type Theory
• Formalising Mathematics in Simple Type Theory
• Formalizing simplicial topology in Isabelle/HOL and Coq
• scientific article; zbMATH DE number 1537947
• scientific article; zbMATH DE number 2154581
• scientific article; zbMATH DE number 1498598
• Combining logics in simple type theory

Cites work

• scientific article; zbMATH DE number 949397 (Why is no real title available?)
• scientific article; zbMATH DE number 936267 (Why is no real title available?)
• scientific article; zbMATH DE number 3255438 (Why is no real title available?)
• Computational logic: its origins and applications
• Continuous Lattices and Domains
• Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
• Duality Theories for Boolean Algebras with Operators
• Hammering towards QED
• Handbook of Spatial Logics
• Homotopy type theory. Univalent foundations of mathematics
• Intuitionistic logic and modality via topology
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Quantified multimodal logics in simple type theory
• The algebra of topology

Cited in

(2)

• Formalising Mathematics in Simple Type Theory
• Types for Proofs and Programs

This page was built for publication: Formalising basic topology for computational logic in simple type theory

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