
Kleene Algebra
 Referenced in 7 articles
[sw32203]
 Kleene Algebra: These files contain a formalisation of variants of Kleene algebras and their most ... axiomatic type classes in Isabelle/HOL. Kleene algebras are foundational structures in computing with applications ranging ... relations and formal power series form Kleene algebras, and consider further models based on lattices ... formation of matrices (proofs for Kleene algebras remain to be completed). On the one hand...

KATML
 Referenced in 10 articles
[sw08506]
 interactive theorem prover for Kleene algebra with tests. We describe KATML, an implementation ... interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect...

Relation Algebra
 Referenced in 6 articles
[sw32202]
 various notions associated to functions. Relation algebras are also expanded by a reflexive transitive closure ... operation, and they are linked with Kleene algebras and models of binary relations and Boolean...

Regular_Algebras
 Referenced in 3 articles
[sw32237]
 algebra hierarchy is orthogonal to the Kleene algebra hierarchy in the Archive of Formal Proofs...

RATHAgda
 Referenced in 3 articles
[sw13303]
 RATHAgda: RelationAlgebraic Theories in Agda. The basic category and allegory theory library ... same time Kleene categories (i.e., typed Kleene algebras), including also monoidal categories. These theories...

Algebraic_VCs
 Referenced in 1 article
[sw32217]
 Construction and Verification Components Based on Kleene Algebra. Variants of Kleene algebra support program construction ... component for Hoare logic based on Kleene algebra with tests, verification components for weakest preconditions ... strongest postconditions based on Kleene algebra with domain and a component for stepwise refinement ... based on refinement Kleene algebra with tests. In addition to these components for the partial...

KAD
 Referenced in 1 article
[sw32231]
 Kleene Algebras with Domain. Kleene algebras with domain are Kleene algebras endowed with an operation ... semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations ... domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these...

ATBR
 Referenced in 1 article
[sw28615]
 working with binary relations. This library provides algebraic tools for working with binary relations ... solving (in)equations in an arbitrary Kleene algebra. The decision procedure goes through standard finite ... library to be superseded by the Relation Algebra library, which is based on derivatives rather ... found in the paper Deciding Kleene Algebras...

Stone Kleene
 Referenced in 1 article
[sw28599]
 StoneKleene Relation Algebras. We develop StoneKleene relation algebras, which expand Stone relation algebras...

Codatatype
 Referenced in 1 article
[sw28678]
 also prove the axioms of Kleene algebra for the defined regular operations. Furthermore, a language...

ACL2
 Referenced in 281 articles
[sw00060]
 ACL2 is both a programming language in which...

Coq
 Referenced in 1845 articles
[sw00161]
 Coq is a formal proof management system. It...

Isabelle
 Referenced in 667 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

KeYC
 Referenced in 5 articles
[sw00486]
 We present KeYC, a tool for deductive...

LEOII
 Referenced in 51 articles
[sw00512]
 LEOII is a standalone, resolutionbased higher...

Maple
 Referenced in 5253 articles
[sw00545]
 The result of over 30 years of cutting...

Nitpick
 Referenced in 61 articles
[sw00622]
 Nitpick is a counterexample generator for Isabelle/HOL that...

RelView
 Referenced in 102 articles
[sw00798]
 The RelViewSystem is an interactive tool for...

PRISM
 Referenced in 429 articles
[sw01186]
 PRISM: Probabilistic symbolic model checker. In this paper...

ML
 Referenced in 517 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...