• ALF

  • Referenced in 67 articles [sw08603]
  • which different logics can be represented. Proof objects are manipulated directly, by the usual editing ... proof is represented as an incomplete proof object, i.e., a proof object containing placeholders ... modular type/proof checking algorithm for complete proof objects is presented, and it is proved sound...
  • CVC Lite

  • Referenced in 54 articles [sw07581]
  • Lite and translates the resulting proof object back to HOL-Light. As a result...
  • Waldmeister

  • Referenced in 43 articles [sw19568]
  • space. Within that scope, a complete proof object is constructed at run-time. Read more...
  • Isar

  • Referenced in 138 articles [sw04599]
  • used interchangeably between Isabelle-classic proof scripts and Isabelle/Isar documents. Isar is as generic ... able to support a wide range of object-logics. The current end-user setup ... Isabelle/HOL. Together with the Isabelle/Isar instantiation of Proof General, a generic (X)Emacs interface...
  • HOL Light

  • Referenced in 285 articles [sw06580]
  • overview. HOL Light is an interactive proof assistant for classical higher-order logic, intended ... Light’s case this is Objective CAML (OCaml). Thanks to its adherence ... logical kernel. Despite this, it provides powerful proof tools and has been applied to some...
  • JProver

  • Referenced in 11 articles [sw09978]
  • theorem prover that creates sequent-style proof objects and can serve as a proof engine ... proof technique, the generation of proof objects, and its integration into the Nuprl proof development...
  • HR

  • Referenced in 29 articles [sw10392]
  • interest, concepts about those objects, conjectures relating the concepts and proofs of the conjectures...
  • VeriML

  • Referenced in 8 articles [sw13522]
  • logic and supply explicit machine-checkable proof objects. Unfortunately, large scale proof development in these...
  • POOL

  • Referenced in 14 articles [sw03332]
  • proof system for the parallel object-oriented language POOL. We develop a Hoare-style proof...
  • Zenon

  • Referenced in 21 articles [sw06753]
  • extensible automated theorem prover producing checkable proofs. We present Zenon, an automated theorem prover ... Focal environment, an object-oriented algebraic specification and proof system, which is able to produce...
  • Isabelle/UTP

  • Referenced in 10 articles [sw21184]
  • typing proof obligations in the object-language. Thirdly, proof tactics that transfer results from well...
  • Teyjus

  • Referenced in 16 articles [sw21364]
  • systems that manipulate formal objects such as formulas, programs, proofs and types. Towards harnessing these...
  • Abella

  • Referenced in 48 articles [sw09461]
  • interactive system for reasoning about aspects of object languages that have been formally presented through ... specification logic and allows the development of proofs of properties about specifications. An important characteristic ... tree syntax approach to treating binding in object languages. Amongst other things, Abella has been...
  • Satallax

  • Referenced in 48 articles [sw06849]
  • much of the search for a proof. Satallax generates propositional clauses corresponding to rules ... these clauses. Satallax is implemented in Objective Caml. You can run Satallax online...
  • Lambda-Clam

  • Referenced in 24 articles [sw19614]
  • usefulness and feasibility of applying higher-order proof planning to a number of types ... inability to reason properly about higher-order objects. λClam is written in λProlog...
  • GCLC

  • Referenced in 29 articles [sw00326]
  • visualizing geometrical (and not only geometrical) objects and notions, for teaching/studying mathematics, and for producing ... information with deductive properties and machine-generated proofs...
  • Timbuk

  • Referenced in 46 articles [sw06351]
  • collection of tools for achieving proofs of reachability over Term Rewriting Systems and for manipulating ... three standalone tools and a bunch of Objective Caml functions for basic manipulation on Tree...
  • Rtac

  • Referenced in 2 articles [sw13124]
  • overhead inherent in constructing large proof objects. However, to date it is significantly more time...
  • MJ

  • Referenced in 12 articles [sw24342]
  • with effects. In order to study rigorously object-oriented languages such as Java ... which are sufficiently small to facilitate formal proofs of key properties. However many ... Whilst compact, MJ models features such as object identity, field assignment, constructor methods and block ... operational semantics of MJ, and give a proof of type safety. In order to demonstrate...
  • Split Packing

  • Referenced in 3 articles [sw29064]
  • results of this type for circular objects. Our proof is constructive: We describe a subdivision...