
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 HOLLight. As a result...

Waldmeister
 Referenced in 43 articles
[sw19568]
 space. Within that scope, a complete proof object is constructed at runtime. Read more...

Isar
 Referenced in 138 articles
[sw04599]
 used interchangeably between Isabelleclassic proof scripts and Isabelle/Isar documents. Isar is as generic ... able to support a wide range of objectlogics. The current enduser 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 higherorder 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 sequentstyle 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 machinecheckable proof objects. Unfortunately, large scale proof development in these...

POOL
 Referenced in 14 articles
[sw03332]
 proof system for the parallel objectoriented language POOL. We develop a Hoarestyle proof...

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

Isabelle/UTP
 Referenced in 10 articles
[sw21184]
 typing proof obligations in the objectlanguage. 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...

LambdaClam
 Referenced in 24 articles
[sw19614]
 usefulness and feasibility of applying higherorder proof planning to a number of types ... inability to reason properly about higherorder 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 machinegenerated 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 objectoriented 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...