• MizarMode

  • Referenced in 18 articles [sw01973]
  • tool for the Mizar way of formalizing mathematics. The Emacs authoring environment for Mizar (MizarMode ... maintaining a very large body of formalized mathematics. par Mizar is a non-programmable ... long-term and large-scale formalization effort. MizarMode has been designed with...
  • QMT

  • Referenced in 20 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 73 articles [sw00973]
  • partial automation of various mathematical activities, promoting development of formal theories in a wide variety...
  • CalcCheck

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

  • Referenced in 17 articles [sw32625]
  • build a standard library of formalized mathematics and verified software...
  • OMRS

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

  • Referenced in 13 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...
  • HOLyHammer

  • Referenced in 26 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...
  • TRIC

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

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

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

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

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

  • Referenced in 13 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...
  • Ginsim

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

  • Referenced in 11 articles [sw27551]
  • main bottlenecks in the formalization of mathematics. We propose a two stage approach for this...
  • Z

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

  • Referenced in 49 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 15 articles [sw09796]
  • presented. SAD deals with mathematical texts that are formalized in the ForTheL language (a brief...
  • 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...