• Isabelle/HOL

  • Referenced in 921 articles [sw01569]
  • Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...
  • Isabelle

  • Referenced in 594 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...
  • Automath

  • Referenced in 396 articles [sw07127]
  • computer. It’s the direct ancestor of the ”type theoretical” line of proof assistants from...
  • Archive Formal Proofs

  • Referenced in 139 articles [sw28613]
  • vast collection of computer-checked proofs developed using the proof assistant Isabelle. We perform...
  • LCF

  • Referenced in 157 articles [sw08360]
  • history. The original LCF system was a proof-checking program developed at Stanford University ... form a thriving paradigm in computer assisted reasoning. Many of the developments of the last ... descendents of LCF is HOL, a proof assistant for higher order logic originally developed...
  • RedHom

  • Referenced in 12 articles [sw08776]
  • RedHom constitutes a part of CAPD (Computer Assisted Proofs in Dynamics) project. We decided...
  • Coq/SSReflect

  • Referenced in 62 articles [sw09360]
  • proof assistant. The name Ssreflect stands for ”small scale reflection”, a style of proof that ... evolved from the computer-checked proof of the Four Colour Theorem and which leverages...
  • KRAKATOA

  • Referenced in 85 articles [sw03159]
  • distinct components: the WHY tool, which computes proof obligations for a core imperative language annotated ... post-conditions, the CQQ proof assistant for modeling the program semantics and conducting the development...
  • Lorenz-Database

  • Referenced in 5 articles [sw14477]
  • guarantees their existence via computer-assisted proofs methods. The orbits are computed using high-precision...
  • Isabelle/ZF

  • Referenced in 61 articles [sw04973]
  • Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...
  • CoqMT

  • Referenced in 5 articles [sw19139]
  • extension of the Coq proof assistant incorporating, in its computational mechanism, validity entailment for user ... provides more automation during the development of proofs. CoqMT improves over the Calculus of Congruent...
  • MahonianStat

  • Referenced in 11 articles [sw06180]
  • proofs that the distribution is asymptotically normal. The first is computer-assisted, based ... perform experiments and calculations. Our second proof uses characteristic functions. We then take...
  • Isar

  • Referenced in 138 articles [sw04599]
  • proof documents sets out to bridge the semantic gap between internal notions of proof given ... broad range of automated proof methods. Interactive proof development is supported directly as well ... Theories, theorems, proof procedures etc. may be used interchangeably between Isabelle-classic proof scripts ... instantiation of Proof General, a generic (X)Emacs interface for interactive proof assistants, we arrive...
  • Octave Interval

  • Referenced in 1 article [sw13236]
  • Also it can be applied to computer-assisted proofs, constraint programming, and verified computing...
  • MMTTeX

  • Referenced in 2 articles [sw31595]
  • content-oriented ones such as proof assistants and computer algebra systems on the other hand...
  • VeriML

  • Referenced in 8 articles [sw13522]
  • typed computation of logical terms inside a language with effects. Modern proof assistants such ... task. One major weakness of these proof assistants is the lack of a single language ... manner. This limits the scalability of the proof development process, as users avoid developing domain ... design that couples a type-safe effectful computational language with first-class support for manipulating...
  • Ynot

  • Referenced in 35 articles [sw12334]
  • axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher ... call Ynot, is the added support for computations that may have effects such...
  • CFML

  • Referenced in 8 articles [sw13287]
  • about the characteristic formula using a proof assistant such as Coq. Our characteristic formulae improve ... Honda} et al.’s [Lect. Notes Comput. Sci. 4052, 360--371 (2006; Zbl 1133.03333)] total ... practice to verify programs using existing proof assistants. Our technique has been applied to formally...
  • GEX

  • Referenced in 33 articles [sw09961]
  • used to build dynamic visual models to assist teaching and learning of various mathematical concepts ... Geometry Expert (GEX) is a powerful computer program for geometric reasoning. Within its domain ... prrperties of theorems, and to generate readable proofs for mant geometry throerms. 2) By dynamic...
  • TRX

  • Referenced in 9 articles [sw08800]
  • interpreter. Parsing is an important problem in computer science and yet surprisingly little attention ... parser interpreter formally developed in the proof assistant Coq, capable of producing formally correct parsers...