Results 1 to 7 of 7
Sort by:

  • ProofPower
  • Referenced in 57 articles [sw06339]
  • ProofPower is a specification and proof tool based on an implementation of Higher Order Logic ... following the LCF paradigm, in Standard ML. ProofPower provides support for specification and proof...

  • OpenTheory
  • Referenced in 17 articles [sw32625]
  • order logic, including HOL Light, HOL4 and ProofPower. It is hoped that OpenTheory packages...

  • ArcAngelC
  • Referenced in 6 articles [sw06338]
  • discuss its mechanisation in a theorem prover, ProofPower...

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

  • ArcAngel
  • Referenced in 14 articles [sw01812]
  • ArcAngel: a tactic language for refinement. Morgan’s...

  • Z
  • Referenced in 286 articles [sw10291]
  • Using Z. Specification, refinement, and proof. The book...

  • Circus
  • Referenced in 90 articles [sw21828]
  • The Semantics of Circus. Circus is a concurrent...