
MML
 Referenced in 48 articles
[sw06970]
 large corpus of formalised mathematical knowledge. It has been constructed over the course of many ... communities of other libraries of formalised mathematical knowledge might take up the legal and scientific...

CAVA
 Referenced in 2 articles
[sw28570]
 prover Isabelle. The algorithms are formalised on an mathematical, abstract level, using mainly sets...

Isabelle/UTP
 Referenced in 11 articles
[sw21184]
 framework for the study, formalisation, and unification of formal semantics. Our contributions are, firstly ... tactics that transfer results from wellsupported mathematical structures in Isabelle to proofs about...

NUML
 Referenced in 1 article
[sw03463]
 NUML, there is the problem to formalise object oriented programming paradigm which is still open ... with sufficient capability, which provides us a mathematical tool to do the formalization. This paper ... higherorder πcalculus to formalise NUML...

ForMaRE
 Referenced in 3 articles
[sw08774]
 economics. The ForMaRE project applies formal mathematical reasoning to economics. We seek to increase confidence ... where we are building a toolbox of formalisations, and have started to study matching...

ASTRA
 Referenced in 12 articles
[sw00052]
 Fault Tree Analysis (FTA) is a formalised deductive...

ACL2
 Referenced in 281 articles
[sw00060]
 ACL2 is both a programming language in which...

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

Dafny
 Referenced in 66 articles
[sw00183]
 Dafny is an imperative objectbased language with...

GCLC
 Referenced in 30 articles
[sw00326]
 We present GCLC/WinGCLC  a tool for visualizing geometrical...

Isabelle
 Referenced in 638 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

LEOII
 Referenced in 51 articles
[sw00512]
 LEOII is a standalone, resolutionbased higher...

Nitpick
 Referenced in 61 articles
[sw00622]
 Nitpick is a counterexample generator for Isabelle/HOL that...

RelView
 Referenced in 102 articles
[sw00798]
 The RelViewSystem is an interactive tool for...

Theorema
 Referenced in 146 articles
[sw00961]
 The software system Theorema provides a uniform logic...

ML
 Referenced in 517 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

SPIN
 Referenced in 716 articles
[sw03455]
 Spin is a popular opensource software tool...

Why3
 Referenced in 130 articles
[sw04438]
 Why3 is a platform for deductive program verification...

Uppaal
 Referenced in 639 articles
[sw04702]
 Uppaal is an integrated tool environment for modeling...