Cargando…
Combining Higher-Order Logic with Set Theory Formalizations
The Isabelle Higher-order Tarski–Grothendieck object logic includes in its foundations both higher-order logic and set theory, which allows importing the libraries of Isabelle/HOL and Isabelle/Mizar. The two libraries, however, define all the basic concepts independently, which means that the result...
Autores principales: | Kaliszyk, Cezary, Pąk, Karol |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
Springer Netherlands
2023
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC10209288/ https://www.ncbi.nlm.nih.gov/pubmed/37252035 http://dx.doi.org/10.1007/s10817-023-09663-5 |
Ejemplares similares
-
A Formalization of the Smith Normal Form in Higher-Order Logic
por: Divasón, Jose, et al.
Publicado: (2022) -
Hammer for Coq: Automation for Dependent Type Theory
por: Czajka, Łukasz, et al.
Publicado: (2018) -
Well-quasi orders in computation, logic, language and reasoning: a unifying concept of proof theory, automata theory, formal languages and descriptive set theory
por: Schuster, Peter, et al.
Publicado: (2020) -
A Combinator-Based Superposition Calculus for Higher-Order Logic
por: Bhayat, Ahmed, et al.
Publicado: (2020) -
ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science and Formal Methods
por: Geleßus, David, et al.
Publicado: (2020)