• ATBR

  • Referenced in 1 article [sw28615]
  • arbitrary Kleene algebra. The decision procedure goes through standard finite automata constructions. Note that ... library to be superseded by the Relation Algebra library, which is based on derivatives rather ... found in the paper Deciding Kleene Algebras...
  • Relation Algebra

  • Referenced in 6 articles [sw32202]
  • standard textbooks of Maddux and Schmidt and Ströhlein. This includes relation-algebraic concepts such ... 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...
  • Codatatype

  • Referenced in 1 article [sw28678]
  • standard definitions). As an exercise in coinduction we also prove the axioms of Kleene algebra...
  • ACL2

  • Referenced in 291 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

  • Referenced in 1906 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Isabelle

  • Referenced in 719 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Maple

  • Referenced in 5403 articles [sw00545]
  • The result of over 30 years of cutting...
  • PRISM

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

  • Referenced in 524 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • Kronos

  • Referenced in 274 articles [sw01270]
  • KRONOS is a tool developed with the aim...
  • OTTER

  • Referenced in 320 articles [sw02904]
  • Our current automated deduction system Otter is designed...
  • VAMPIRE

  • Referenced in 264 articles [sw02918]
  • Vampire 8.0, [RV02,Vor05] is an automatic theorem...
  • RODAS

  • Referenced in 1757 articles [sw04112]
  • Rosenbrock method of order 4(3), for problems...
  • HyTech

  • Referenced in 333 articles [sw04125]
  • HyTech is an automatic tool for the analysis...
  • TPTP

  • Referenced in 401 articles [sw04143]
  • The TPTP (Thousands of Problems for Theorem Provers...
  • Metis_

  • Referenced in 56 articles [sw04439]
  • Metis is an automatic theorem prover for first...
  • Uppaal

  • Referenced in 658 articles [sw04702]
  • Uppaal is an integrated tool environment for modeling...
  • Mizar

  • Referenced in 506 articles [sw04704]
  • The Mizar System is the only implementation of...
  • KELLEY

  • Referenced in 643 articles [sw04829]
  • Iterative methods for optimization This book gives an...