• MMT

  • Referenced in 47 articles [sw07136]
  • MMT Language. We introduce the MMT language, which provides a simple and scalable Module system ... development of Mathematical Theories. MMT permits to encode mathematical knowledge in a logic-neutral representation ... represented knowledge interoperable and thus comparable. Furthermore, MMT defines logic-independent notions of well-formedness...
  • MMT

  • Referenced in 16 articles [sw07905]
  • extension is made. Maude MSOS tool (MMT) is an executable environment for MSOS implemented ... MSDF) is the specification language supported by MMT. MSDF syntax is quite close to MSOS ... several syntactic components to be left implicit. MMT joins the support for modularity with ... Maude engine. We have used MMT in several different examples from programming languages semantics...
  • QMT

  • Referenced in 19 articles [sw07137]
  • human.par Based on the generic representation language MMT, we introduce the mathematical query language ... implemented QMT as a part of the MMT API. This combination provides a scalable indexing...
  • MMTTeX

  • Referenced in 2 articles [sw31595]
  • window for the narrative and Mmt for the content-oriented representation. Formal objects ... written in MMT and imported into Open image in new window documents or written ... window document directly. In the latter case, Mmt parses and checks the formal content during...
  • Coq

  • Referenced in 1784 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Isabelle

  • Referenced in 606 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Beluga

  • Referenced in 25 articles [sw01321]
  • Our main interest in this project is to...
  • PVS

  • Referenced in 614 articles [sw03484]
  • PVS is a verification system: that is, a...
  • Isar

  • Referenced in 140 articles [sw04599]
  • Theorem proving system supporting both interactive proof development...
  • Mizar

  • Referenced in 456 articles [sw04704]
  • The Mizar System is the only implementation of...
  • HOL

  • Referenced in 502 articles [sw05492]
  • Higher Order Logic (HOL) is a programming environment...
  • Nuprl

  • Referenced in 387 articles [sw06751]
  • The Nuprl system is a framework for reasoning...
  • Twelf

  • Referenced in 169 articles [sw06888]
  • Twelf is a language used to specify, implement...
  • OMDoc

  • Referenced in 86 articles [sw07138]
  • OMDOC: Towards an internet standard for the administration...
  • Abella

  • Referenced in 49 articles [sw09461]
  • The Abella Interactive Theorem Prover (System Description). Abella...
  • Agda

  • Referenced in 182 articles [sw09689]
  • Agda is a dependently typed functional programming language...