• Isar

  • Referenced in 138 articles [sw04599]
  • steps, so basically the interpreter has a proof text debugger already built-in. The Isar ... into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures etc. may be used interchangeably...
  • ETPS

  • Referenced in 153 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 178 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 Martin-Löf’s Monomorphic Type Theory with Explicit Substitution. This thesis ... interactive proof editor based on Martin-Lö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 49 articles [sw09143]
  • proof system. IMPS is an interactive mathematical proof system intended as a general-purpose 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 ... higher-order power of its underlying type theories, and the support of specifying new inductive...
  • CoCasl

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

  • Referenced in 274 articles [sw10291]
  • Using Z. Specification, refinement, and proof. The book is an in-depth 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...
  • Locales

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

  • Referenced in 14 articles [sw01812]
  • language has a denotational semantics and proof theory...
  • Isabelle/ZF

  • Referenced in 61 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...
  • Bedwyr

  • Referenced in 21 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...
  • OTTER

  • Referenced in 310 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...
  • 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...
  • LPL software

  • Referenced in 18 articles [sw04860]
  • boolean connectives, formal proof techniques, quantifiers, basic set theory, and induction. Advanced chapters include proofs...
  • HipSpec

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

  • Referenced in 42 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...
  • 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...