• HOL Light

  • Referenced in 308 articles [sw06580]
  • overview. HOL Light is an interactive proof assistant for classical higher-order 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 user-interface 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 connection-based theorem proving into interactive proof assistants. JProver is a first-order 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 Martin-Lö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 HTML5-ECMAScript ... jsCoq allows the user to start interaction with proof scripts right away, thanks ... serialization-based 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]
  • Boyer-Moore family like ACL2, and interactive proof assistants for typed higher-order logics. Imandra ... control. Imandra’s user interfaces include an interactive toplevel, Jupyter notebooks and asynchronous document-based...
  • 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 well-known 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...
  • Plat-Omega

  • 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 human-assisted proving of open conjectures ... system, and (ii) develop new proof guiding algorithms that load many previous proofs inside...