• 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...
  • KAT-ML

  • Referenced in 10 articles [sw08506]
  • interactive theorem prover for Kleene algebra with tests. We describe KAT-ML, 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...
  • RATH-Agda

  • Referenced in 3 articles [sw13303]
  • RATH-Agda: Relation-Algebraic 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 step-wise 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]
  • Stone-Kleene Relation Algebras. We develop Stone-Kleene 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...
  • KeY-C

  • Referenced in 5 articles [sw00486]
  • We present KeY-C, a tool for deductive...
  • LEO-II

  • Referenced in 51 articles [sw00512]
  • LEO-II is a standalone, resolution-based 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 RelView-System 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 general-purpose functional...