Related papers: A concise proof of Commoner's theorem
We consider a generalization of the classic Sperner lemma. This lemma states that every Sperner coloring of a triangulation of a simplex contains a fully colored simplex. We found a weaker assumption than Sperner's coloring. It is also…
We survey 25 years of research on decidability issues for Petri nets. We collect results on the decidability of important properties, equivalence notions, and temporal logics.
Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking $\vec{m}_\text{src}$ cannot reach a marking $\vec{m}_\text{tgt}$, then there is a formula $\varphi$ of Presburger arithmetic…
We identify the (filter representation of the) logic behind the recent theory of coherent sets of desirable (sets of) things, which generalise coherent sets of desirable (sets of) gambles as well as coherent choice functions, and show that…
We investigate bisimulation equivalence on Petri nets under durational semantics. Our motivation was to verify the conjecture that in durational setting, the bisimulation equivalence checking problem becomes more tractable than in ordinary…
Event structures are a well-accepted model of concurrency. In a seminal paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge between the theory of domains and the approach to concurrency proposed by Petri. A basic role…
This document demonstrates that the efficient approach for diagnosis of Petri nets via integer linear programming may be unable to detect a fault even if the system is diagnosable.
We prove Barth-type connectedness results for low-codimension smooth subvarieties with good numerical properties inside certain "easy" ambient spaces (such as homogeneous varieties, or spherical varieties). The argument employs some basics…
We review the PCT-theorem and problems connected with its demonstration. We add a new proof of the PCT-theorem in the theory of local observables which is similar to that one of Jost in Wightman quantum field theory. We also look at…
We review some of the endeavors in trying to connect Petri nets with free symmetric monoidal categories. We give a list of requirement such connections should respect if they are meant to be useful for practical/implementation purposes. We…
We provide a type theoretic treatment of the paper "On Tarski's fixed point theorem" by Giovanni Curi. There are benefits to having a type theoretic formulation apart from routine implementation in a proof assistant. By taking advantage of…
This expository note presents a constructive proof of Wigner's theorem using only a few basic facts about Hilbert spaces, such as the existence of orthonormal bases and the Fourier decomposition of a vector. Our proof is based on a proof by…
We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer…
In this oaper, we prove some fixed point theorems in metric vector spaces, in which the continuity is not required for the considered mappings to satisfy. We provide some concrete examples to demonstrate these theorems. We also give some…
Student's theorem is an important result in statistics which states that for normal population, the sample variance is independent from the sample mean and has a chi-square distribution. The existing proofs of this theorem either overly…
This expository paper, aimed at the reader without much background in set theory or logic, gives an overview of Cohen's proof (via forcing) of the independence of the continuum hypothesis. It emphasizes the broad outlines and the intuitive…
We give a short and self-contained proof of Levi's Extension Lemma for pseudoline arrangements.
A class of nets in constructive (in A.A.Markov's sense) topological space for which the convergence is equivalent to convergence of all subsequences, is described. B.A.Kushner's theorem about coincidence of strong and weak constructive…
A short and simple proof of necessity in the McCullough-Quiggin characterization of positive semi-definite kernels with the complete Pick property is presented.
We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem…