• Isabelle/HOL

  • Referenced in 964 articles [sw01569]
  • generic proof assistant. It allows mathematical formulas to be expressed in a formal language ... logical calculus. The main application is the formalization of mathematical proofs and in particular formal...
  • Isabelle

  • Referenced in 611 articles [sw00454]
  • generic proof assistant. It allows mathematical formulas to be expressed in a formal language ... logical calculus. The main application is the formalization of mathematical proofs and in particular formal...
  • ETPS

  • Referenced in 156 articles [sw06302]
  • automated theorem-prover for first-order logic and type theory. The latter ... software verification, partial automation of various mathematical activities, promoting development of formal theories ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof...
  • MMT

  • Referenced in 47 articles [sw07136]
  • Theories. MMT permits to encode mathematical knowledge in a logic-neutral representation format that ... represent the meta-theoretic foundations of mathematical and logical systems together with the represented knowledge ... defines logic-independent notions of well-formedness and equivalence of modular mathematical theories. Thus...
  • HOL Light

  • Referenced in 293 articles [sw06580]
  • clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof ... trivial tasks in the formalization of mathematics and industrial formal verification...
  • Theorema

  • Referenced in 145 articles [sw00961]
  • software system Theorema provides a uniform logic and software technologic frame for proving, solving ... simplifying formulae in all areas of mathematics. Theorema is developed at the Research Institute...
  • IMPS

  • Referenced in 50 articles [sw09143]
  • formulating and applying mathematics in a familiar fashion. The logic of IMPS is based ... type theory with partial functions and subtypes. Mathematical specification and inference are performed relative ... thousand repeatable proofs covers significant portions of logic, algebra, and analysis and provides some support...
  • GraphBase

  • Referenced in 122 articles [sw01555]
  • computational logic circuits, the Mona Lisa, etc. Others are based on regular mathematical constructions such...
  • Isabelle/ZF

  • Referenced in 62 articles [sw04973]
  • generic proof assistant. It allows mathematical formulas to be expressed in a formal language ... logical calculus. The main application is the formalization of mathematical proofs and in particular formal...
  • Orbital library

  • Referenced in 13 articles [sw05562]
  • object-oriented representations and algorithms for logic, mathematics, and computer science. It comprises theorem proving...
  • MBase

  • Referenced in 17 articles [sw08724]
  • analyze its structure. For the logical formulation of mathematical concepts, we propose a methodology ... mathematical knowledge bases. We propose to concretely equip knowledge bases with a hierarchy of logical ... systems that are linked by logic morphisms. These mappings relativize formulae and proofs and thus ... that is well-suited both for formalizing mathematical practice and supporting efficient inference services. This...
  • BABEL

  • Referenced in 71 articles [sw03018]
  • logic programming (as embodied in PROLOG) in a simple, flexible, and mathematically well-bounded...
  • LPL software

  • Referenced in 18 articles [sw04860]
  • courses, from first logic courses for undergraduates (philosophy, mathematics, and computer science) to a first...
  • Isabelle/PIDE

  • Referenced in 13 articles [sw07185]
  • basis for educational tools. The traditionally strong logical foundations of systems like ... shall ultimately lead to combined mathematical assistants, where the logical engine is in the background ... view on applications of formal methods, formalized mathematics, and math education in particular...
  • GEX

  • Referenced in 35 articles [sw09961]
  • various mathematical concepts. As an automated reasoning software, we can build dynamic logic models which...
  • LEGO

  • Referenced in 107 articles [sw09685]
  • implements various related type systems - the Edinburgh Logical Framework (LF), the Calculus of Constructions ... formalization closer to that of informal mathematics. The higher-order power of its underlying type...
  • MoMM

  • Referenced in 33 articles [sw04655]
  • Mizar Mathematical Library (MML), which uses a richer formalism than just pure predicate logic. This...
  • RRL

  • Referenced in 55 articles [sw28904]
  • experimenting with automated reasoning algorithms for equational logic based on rewrite techniques ... been used to solve hard and challenging mathematical problems in automated reasoning literature as well...
  • Gandalf

  • Referenced in 35 articles [sw10133]
  • proves theorems formulated in logic. Since logic is a pretty universal language, ATP systems such ... Gandalf can prove theorems in mathematics and verify complex systems such as digital circuits, software...
  • TPS

  • Referenced in 71 articles [sw00973]
  • automated theorem-prover for first-order logic and type theory. The latter ... software verification, partial automation of various mathematical activities, promoting development of formal theories ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture...