
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 theoremprover for firstorder logic and type theory. The latter ... software verification, partial automation of various mathematical activities, promoting development of formal theories ... prove theorems of first and higherorder 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 logicneutral representation format that ... represent the metatheoretic foundations of mathematical and logical systems together with the represented knowledge ... defines logicindependent notions of wellformedness 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]
 objectoriented 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 wellsuited 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 wellbounded...

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 higherorder 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 theoremprover for firstorder logic and type theory. The latter ... software verification, partial automation of various mathematical activities, promoting development of formal theories ... prove theorems of first and higherorder logic interactively, automatically, or in a mixture...