On streams that are finitely red

Autor: Marc Bezem, Keiko Nakata, Tarmo Uustalu

Publikováno v: Logical Methods in Computer Science, Vol Volume 8, Issue 4 (2012)

Mixing induction and coinduction, we study alternative definitions of streams being finitely red. We organize our definitions into a hierarchy including also some well-known alternatives in intuitionistic analysis. The hierarchy collapses classically

Externí odkaz: https://doaj.org/article/549d3152b9b14ce78b74c60f5d8c0a34

Syntactic forcing models for coherent logic

Autor: Ulrik Buchholtz, Marc Bezem, Thierry Coquand

Publikováno v: Indagationes Mathematicae. 29:1441-1464

We present three syntactic forcing models for coherent logic. These are based on sites whose underlying category only depends on the signature of the coherent theory, and they do not presuppose that the logic has equality. As an application we give a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::1a46f710c854248ccfe880eeab00b7ff
https://doi.org/10.1016/j.indag.2018.06.004

Construction of the circle in UniMath

Autor: Marc Bezem, Ulrik Buchholtz, Daniel R. Grayson, Michael Shulman

Publikováno v: Journal of Pure and Applied Algebra

We show that the type $\mathrm{T}\mathbb{Z}$ of $\mathbb{Z}$-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence Axiom and propositional

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::edf393482b86895132edb0f8a4ca4a4a
https://doi.org/10.1016/j.jpaa.2021.106687

Skolem Machines

Autor: John Fisher, Marc Bezem

Publikováno v: Fundamenta Informaticae. 91:79-103

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::3977762bc03bb081371b433434e417ca
https://doi.org/10.3233/fi-2009-0034

On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic

Autor: Dimitri Hendriks, Marc Bezem

Publikováno v: Bezem, M & Hendriks, R D A 2008, ' On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic ', Journal of Automated Reasoning, vol. 40, no. 1, pp. 61-85 . https://doi.org/10.1007/s10817-007-9086-x
Journal of Automated Reasoning, 40(1), 61-85. Springer Netherlands

We propose to combine interactive proof construction with proof automation for a fragment of first-order logic called Coherent Logic (CL). CL allows enough existential quantification to make Skolemization unnecessary. Moreover, CL has a constructive

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8352926d6e9b3dcf68e33a12d98303b0
https://hdl.handle.net/1871/11418