Zobrazeno 1 - 10
of 37
pro vyhledávání: '"Terraf, Pedro Sánchez"'
We present an exposition of the *Chain Bounding Lemma*, which is a common generalization of both Zorn's Lemma and the Bourbaki-Witt fixed point theorem. The proofs of these results through the use of Chain Bounding are amongst the simplest ones that
Externí odkaz:
http://arxiv.org/abs/2404.11638
The idempotent semigroups (bands) that give rise to partial orders by defining $a \leq b \iff a \cdot b = a$ are the "right-regular" bands (RRB), which are axiomatized by $x\cdot y \cdot x = y \cdot x$. In this work we consider the class of "associat
Externí odkaz:
http://arxiv.org/abs/2404.07877
We provide a fine classification of bisimilarities between states of possibly different labelled Markov processes (LMP). We show that a bisimilarity relation proposed by Panangaden that uses direct sums coincides with "event bisimilarity" from his jo
Externí odkaz:
http://arxiv.org/abs/2401.09273
We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model $M$ of $\mathit{ZFC}$, of generic extensions satisfying $\mathit{ZFC}+\neg\mathit{CH}$ and $\mathit{ZFC}+\mathit{CH}$. Moreover, let
Externí odkaz:
http://arxiv.org/abs/2210.15609
There exist two notions of equivalence of behavior between states of a Labelled Markov Process (LMP): state bisimilarity and event bisimilarity. The first one can be considered as an appropriate generalization to continuous spaces of Larsen and Skou'
Externí odkaz:
http://arxiv.org/abs/2005.03630
We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC. In doing
Externí odkaz:
http://arxiv.org/abs/2001.09715
We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing. We also formalize the satisfaction of the axioms of Extensionality, F
Externí odkaz:
http://arxiv.org/abs/1901.03313
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
We lay the ground for an Isabelle/ZF formalization of Cohen's technique of forcing. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize the definition of forcing notions as preorders
Externí odkaz:
http://arxiv.org/abs/1807.05174
Autor:
Pachl, Jan, Terraf, Pedro Sánchez
Publikováno v:
Logical Methods in Computer Science, Volume 17, Issue 2 (April 14, 2021) lmcs:5886
A labelled Markov process (LMP) consists of a measurable space $S$ together with an indexed family of Markov kernels from $S$ to itself. This structure has been used to model probabilistic computations in Computer Science, and one of the main problem
Externí odkaz:
http://arxiv.org/abs/1706.02801