Titlebook: Relational and Algebraic Methods in Computer Science; 18th International C Uli Fahrenberg,Peter Jipsen,Michael Winter Conference proceeding

接触

Hardness of Network Satisfaction for Relation Algebras with Normal Representations, second result, we prove hardness if . has domain size at least three and contains no non-trivial equivalence relations but a symmetric atom . with a forbidden triple (., ., .), that is, .. We illustrate how to apply our conditions on two small relation algebras.

Expiration

Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras,verify the correctness of an array-based implementation of disjoint-set forests with a naive union operation and a find operation with path compression. All results are formally proved in Isabelle/HOL.

保留

Computer-Supported Exploration of a Categorical Axiomatization of Modeloids,t to an inverse semigroup and then to an inverse category using an axiomatic approach to category theory. We then show that this formulation enables a purely algebraic view on Ehrenfeucht-Fraïssé games.

engrossed

Conference proceedings 2020ether with 3 invited abstracts were carefully selected from 29 submissions. Topics covered range from mathematical foundations to applications as conceptual and methodological tools in computer science and beyond..

faddish

Cupidity

thyroid-hormone

Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory,btain tripos-theoretical completeness theorems for a broad variety of higher-order logics. The framework thus developed, moreover, allows us to obtain tripos-theoretical Girard and Kolmogorov translation theorems for higher-order logics.

2否定

A Unary Semigroup Trace Algebra,nn semigroup. Reactive designs specified using it satisfy core laws that have been mechanised so far in Isabelle/UTP. More importantly, our results improve the support for unifying trace models in the UTP.

Erythropoietin

The Involutive Quantaloid of Completely Distributive Lattices,nce . is closed under the monoidal operations of ., we also argue that if . is involutive, then . is completely distributive as well; consequently, any lattice embedding into an involutive quantale of the form . has, as its domain, a distributive lattice.

毗邻