• QMT

  • Referenced in 19 articles [sw07137]
  • query language for formal mathematical libraries. One of the most promising applications of mathematical knowledge ... tiny fragment of mathematics that has been formalized, the amount exceeds the comprehension ... generic representation language MMT, we introduce the mathematical query language QMT: It combines simplicity, expressivity ... avoiding a commitment to a particular logical formalism. QMT can integrate various search paradigms such...
  • TPS

  • Referenced in 71 articles [sw00973]
  • partial automation of various mathematical activities, promoting development of formal theories in a wide variety...
  • UniMath

  • Referenced in 9 articles [sw15140]
  • UniMath - a library of mathematics formalized in the univalent style. he univalent style of formalization ... level 3 one can efficiently formalize mathematics at the level of categories etc. Univalent style ... allows to directly formalize constructive mathematics and to formalize classical mathematics by adding the excluded ... growing library of constructive mathematics formalized in the univalent style using a small subset...
  • CalcCheck

  • Referenced in 37 articles [sw09760]
  • particular compromise between full formality and customary, more informal, mathematical practises, and thus teaches aspects...
  • OMRS

  • Referenced in 39 articles [sw03359]
  • first ideas for formalizing a communication protocol for mathematical services based on KQML (Knowledge Query...
  • OpenTheory

  • Referenced in 14 articles [sw32625]
  • build a standard library of formalized mathematics and verified software...
  • Isabelle/PIDE

  • Referenced in 12 articles [sw07185]
  • question of math education tools with fully-formal background theories has often been answered negatively ... exist. This shall ultimately lead to combined mathematical assistants, where the logical engine ... view on applications of formal methods, formalized mathematics, and math education in particular...
  • Proviola

  • Referenced in 10 articles [sw00737]
  • stored in an encyclopedia of formalized mathematics, based on our experience in filming...
  • TRIC

  • Referenced in 46 articles [sw02165]
  • finite element method formalized through appropriate geometrical, trigonometrical and enigneering mathematical relations and it involves...
  • TLA

  • Referenced in 25 articles [sw04442]
  • best way to describe things formally is with simple mathematics, and that a specification language...
  • HOLyHammer

  • Referenced in 20 articles [sw11553]
  • online AI/ATP service for formal (computer-understandable) mathematics encoded in the HOL Light system ... upload and automatically process an arbitrary formal development (project) based on HOL Light...
  • booleannet

  • Referenced in 7 articles [sw22019]
  • biological observations and hypotheses into a mathematical formalism. The conceptual underpinnings of Boolean modeling...
  • Coquelicot

  • Referenced in 11 articles [sw11552]
  • users have a way to formally verify mathematical theorems and correctness of critical systems...
  • Ginsim

  • Referenced in 27 articles [sw09090]
  • genetic regulatory networks. Formally, our approach leans on discrete mathematical and graph-theoretical concepts. GINsim...
  • Z

  • Referenced in 274 articles [sw10291]
  • this adquate for promoting a discipline of formal specification and reasoning? Another disappointment is that ... with a certain amount of mathematical inclination...
  • Naproche

  • Referenced in 10 articles [sw28307]
  • Proof Checking) studies the semi-formal language of mathematics from a linguistic, philosophical and mathematical ... ordinary mathematical language including TeX-style typeset formulas and transforms them into formal statements. Linguistic ... common grammatical constructs and to extract mathematically relevant implicit information about hypotheses and conclusions. Finally...
  • RRL

  • Referenced in 55 articles [sw28904]
  • been used to solve hard and challenging mathematical problems in automated reasoning literature as well ... research tool for investigating the use of formal methods in hardware and software design...
  • CompCert

  • Referenced in 42 articles [sw09737]
  • CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such ... verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves ... guarantees that can be obtained by applying formal methods to source programs. The main result...
  • SAD

  • Referenced in 14 articles [sw09796]
  • presented. SAD deals with mathematical texts that are formalized in the ForTheL language (a brief...
  • ForMaRE

  • Referenced in 3 articles [sw08774]
  • formare project -- formal mathematical reasoning in economics. The ForMaRE project applies formal mathematical reasoning ... results, and to foster interest in formal methods, i.e. computer-aided reasoning, within economics...