
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 fullyformal 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 (computerunderstandable) 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 graphtheoretical 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 semiformal language of mathematics from a linguistic, philosophical and mathematical ... ordinary mathematical language including TeXstyle 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, machinechecked 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. computeraided reasoning, within economics...