
Isar
 Referenced in 144 articles
[sw04599]
 steps, so basically the interpreter has a proof text debugger already builtin. The Isar ... into the Isabelle/Pure metalogic implementation. Theories, theorems, proof procedures etc. may be used interchangeably...

ETPS
 Referenced in 160 articles
[sw06302]
 various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive ... facilities for searching for expansion proofs, translating these into natural deduction proofs, constructing natural deduction ... needed formulas which occur anywhere in the proof, and build new formulas from them ... Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic Publishers...

Agda
 Referenced in 205 articles
[sw09689]
 writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system ... Löf. It has many similarities with other proof assistants based on dependent types, such...

ALF
 Referenced in 67 articles
[sw08603]
 Proof Editor based on MartinLöf’s Monomorphic Type Theory with Explicit Substitution. This thesis ... interactive proof editor based on MartinLöf’s type theory with explicit substitutions ... modular type/proof checking algorithm for complete proof objects is presented, and it is proved sound ... complete assuming some basic meta theory properties of the substitution calculus. The algorithm is extended...

IMPS
 Referenced in 52 articles
[sw09143]
 proof system. IMPS is an interactive mathematical proof system intended as a generalpurpose tool ... based on a version of simple type theory with partial functions and subtypes. Mathematical specification ... related to one another via inclusion and theory interpretation. IMPS provides relatively large primitive inference ... human comprehension of the resulting proofs. An initial theory library contained over a thousand repeatable...

LEGO
 Referenced in 107 articles
[sw09685]
 LEGO is an interactive proof development system (proof assistant) designed and implemented by Randy Pollack ... Unified Theory of Dependent Types (UTT). LEGO is a powerful tool for interactive proof development ... like argument synthesis and universe polymorphism make proof checking more practical by bringing the level ... higherorder power of its underlying type theories, and the support of specifying new inductive...

Locales
 Referenced in 41 articles
[sw12448]
 theorems. Interpretation to Isabelle’s global theories and proof contexts is possible via morphisms. Even...

CoCasl
 Referenced in 26 articles
[sw13076]
 framework for studying the semantics and proof theory of reactive systems...

Z
 Referenced in 282 articles
[sw10291]
 Using Z. Specification, refinement, and proof. The book is an indepth introduction ... primarily directed to the user; the background theory is  with the exception of the natural ... further on in the book. Rather, most proofs are omitted and replaced by an appeal...

Isabelle/ZF
 Referenced in 63 articles
[sw04973]
 main application is the formalization of mathematical proofs and in particular formal verification, which includes ... formalizes the greater part of elementary set theory, including relations, functions, injections, surjections, ordinals...

ArcAngel
 Referenced in 14 articles
[sw01812]
 language has a denotational semantics and proof theory...

Bedwyr
 Referenced in 22 articles
[sw09460]
 recent advances in the theory of proof search. The first is centered on the fact...

GAPT
 Referenced in 9 articles
[sw22200]
 GAPT is a proof theory framework developed primarily at the Vienna University of Technology. GAPT ... parsers and other components common in proof theory and automated deduction. In contrast to automated ... provers whose focus is the construction of proofs, GAPT concentrates on the transformation and further...

HipSpec
 Referenced in 14 articles
[sw07736]
 Automating inductive proofs using theory exploration. HipSpec is a system for automatically deriving and proving...

OTTER
 Referenced in 316 articles
[sw02904]
 strategies for directing and restricting searches for proofs. Otter can also be used ... Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry. Note: Otter/Mace2...

CeTA
 Referenced in 47 articles
[sw06584]
 certify termination proofs. To this end, we first formalized the required theory of term rewriting ... technique as it occurs in the generated proofs. Moreover, if a proof is not accepted...

LPL software
 Referenced in 19 articles
[sw04860]
 boolean connectives, formal proof techniques, quantifiers, basic set theory, and induction. Advanced chapters include proofs...

HR
 Referenced in 29 articles
[sw10392]
 program for theorem generation. Automated theory formation involves the production of objects of interest, concepts ... relating the concepts and proofs of the conjectures. In group theory, for example, the objects...

Hipster
 Referenced in 7 articles
[sw11223]
 Hipster: integrating theory exploration in a proof assistant. This paper describes Hipster, a system ... integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically ... functions in a new theory development. The second is proof mode, used in a particular...