
HOL Light
 Referenced in 308 articles
[sw06580]
 overview. HOL Light is an interactive proof assistant for classical higherorder logic, intended ... both the implementation and interaction language; in HOL Light’s case this is Objective CAML ... logical kernel. Despite this, it provides powerful proof tools and has been applied to some...

Isar
 Referenced in 144 articles
[sw04599]
 generic (X)Emacs interface for interactive proof assistants, we arrive at a reasonable environment...

Agda
 Referenced in 205 articles
[sw09689]
 characters, and an interactive Emacs interface (the type checker can assist in the development ... Agda is also a proof assistant: It is an interactive system for writing and checking ... many similarities with other proof assistants based on dependent types, such as Coq, Epigram...

Proof General
 Referenced in 53 articles
[sw04901]
 developing machine proofs with an interactive proof assistant. Interaction is based around a proof script ... target of a proof development. Proof General provides a powerful userinterface with relatively little ... effort, alleviating the need for a proof assistant to provide its own GUI, and providing ... uniform appearance for diverse proof assistants. par Proof General has a growing user base...

LEGO
 Referenced in 107 articles
[sw09685]
 LEGO is an interactive proof development system (proof assistant) designed and implemented by Randy Pollack ... LEGO is a powerful tool for interactive proof development in the natural deduction style...

JProver
 Referenced in 13 articles
[sw09978]
 Integrating connectionbased theorem proving into interactive proof assistants. JProver is a firstorder intuitionistic ... serve as a proof engine in interactive proof assistants with expressive constructive logics. This paper...

GeoProof
 Referenced in 17 articles
[sw05737]
 interactive proof software for geometry. GeoProof can communicate with the Coq proof assistant to perform...

Tac
 Referenced in 7 articles
[sw09455]
 these ideas, we have developed an interactive proof assistant, called Tac, for this logic...

ALF
 Referenced in 67 articles
[sw08603]
 implementation of ALF, which is an interactive proof editor based on MartinLöf’s type ... substitutions. ALF is a general purpose proof assistant, in which different logics can be represented...

Proviola
 Referenced in 10 articles
[sw00737]
 improve on existing models of interaction with a proof assistant (PA), in particular for storage ... introduce three related concepts, those of: a proof movie, consisting of frames which record both ... camera, which films a user’s interactive session with a PA as a movie...

FOL_Harrison
 Referenced in 2 articles
[sw32220]
 within Isabelle as a very simple interactive proof assistant. As examples we consider Pelletier...

jsCoq
 Referenced in 1 article
[sw40703]
 user environment for the Coq interactive proof assistant. The jsCoq system targets the HTML5ECMAScript ... jsCoq allows the user to start interaction with proof scripts right away, thanks ... serializationbased protocol for interaction with the proof assistant, as well as a new package...

CFML
 Referenced in 8 articles
[sw13287]
 specification by reasoning interactively about the characteristic formula using a proof assistant such...

Imandra
 Referenced in 1 article
[sw37911]
 BoyerMoore family like ACL2, and interactive proof assistants for typed higherorder logics. Imandra ... control. Imandra’s user interfaces include an interactive toplevel, Jupyter notebooks and asynchronous documentbased...

Isabelle/PIDE
 Referenced in 13 articles
[sw07185]
 Isabelle/PIDE platform addresses the question whether proof assistants of the LCF family are suitable ... inaccessible interaction via the TTY (or minor variations like the wellknown Proof General / Emacs ... negatively due to accidental weaknesses of existing proof engines. The idea of “PIDE” (which means ... tools. We use Scala to expose the proof engine in ML to the JVM world...

F*
 Referenced in 20 articles
[sw27563]
 with the expressive power of a proof assistant based on dependent types. After verification ... combination of SMT solving and interactive proofs...

RALL
 Referenced in 9 articles
[sw08505]
 other hand, a quite mature proof assistant for research on the relational calculus. RALL ... formulas involved. It offers both an interactive proof facility, with special support for substitutions...

PlatOmega
 Referenced in 3 articles
[sw19624]
 corresponding formal representation for a proof assistant, in our case Ωmega. The primary task ... consistent formal and informal representations during the interactive development of the document...

Kelloy
 Referenced in 1 article
[sw09963]
 proof assistant for alloy specifications. Alloy is a specification language based on a relational first ... counterexamples, it cannot, in general, provide correctness proofs. This paper presents Kelloy, a tool ... translation, and reports on our automatic and interactive experiments...

Proofwatch
 Referenced in 4 articles
[sw28654]
 that allows related proofs to guide a proof search for a new conjecture. This mechanism ... theorem provers, both for interactive formalizations and for humanassisted proving of open conjectures ... system, and (ii) develop new proof guiding algorithms that load many previous proofs inside...