• ETPS

  • Referenced in 145 articles [sw06302]
  • contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... under Windows. Potential applications of automated theorem proving include hardware and software verification, partial automation ... used to prove theorems of first- and higher-order logic interactively, automatically...
  • Isar

  • Referenced in 125 articles [sw04599]
  • Theorem proving system supporting both interactive proof development and some degree of automation have become ... given by state-of-the-art interactive theorem proving systems and an appropriate level ... Isar/VM interpreter. Compared to existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings ... broad range of automated proof methods. Interactive proof development is supported directly as well...
  • TPS

  • Referenced in 67 articles [sw00973]
  • contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... under Windows. Potential applications of automated theorem proving include hardware and software verification, partial automation ... used to prove theorems of first- and higher-order logic interactively, automatically...
  • miz3

  • Referenced in 8 articles [sw18631]
  • procedural and declarative styles of interactive theorem proving. We propose a synthesis ... proof styles of interactive theorem proving: the procedural style (where proofs are scripts of commands ... implemented on top of any procedural interactive theorem prover, regardless of its architecture and logical...
  • CLAM

  • Referenced in 35 articles [sw19619]
  • turn the interactive proof editor into a fully automatic theorem proving system...
  • Athena

  • Referenced in 10 articles [sw09967]
  • programming language and an interactive theorem proving environment rolled in one. As a programming language...
  • Lean

  • Referenced in 17 articles [sw15148]
  • bridge the gap between interactive and automated theorem proving, by situating automated tools and methods...
  • IsaPlanner

  • Referenced in 27 articles [sw02047]
  • framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding ... conjecture and prove theorems automatically. The system provides an interactive tracing tool that allows...
  • JProver

  • Referenced in 11 articles [sw09978]
  • JProver: Integrating connection-based theorem proving into interactive proof assistants. JProver is a first-order...
  • SEPIA

  • Referenced in 6 articles [sw21585]
  • SEPIA combines model inference with interactive theorem proving. Existing proof corpora are modelled using state...
  • Amortized Complexity

  • Referenced in 6 articles [sw28606]
  • proceedings of the conference on Interactive Theorem Proving ITP 2015. An extended version of this...
  • Abella

  • Referenced in 39 articles [sw09461]
  • Abella Interactive Theorem Prover (System Description). Abella [3] is an interactive system for reasoning about ... other things, Abella has been used to prove normalizability properties of the λ-calculus ... foundations of Abella, outlines the style of theorem proving that it supports and finally describes...
  • ProofPeer

  • Referenced in 4 articles [sw30422]
  • collaborative theorem proving. ProofPeer brings together interactive theorem proving technology with the power...
  • Omega-ANTS

  • Referenced in 8 articles [sw19626]
  • open approach at combining interactive and automated theorem proving. We present the $Omega$-ANTS theorem...
  • OMRS

  • Referenced in 39 articles [sw03359]
  • exploratory step towards the definition of the interaction level in OMRS, supplies a concrete syntax ... communication of mathematical services in distributed theorem proving and symbolic computation environments...
  • HOLCF

  • Referenced in 3 articles [sw25266]
  • HOLCF is an interactive theorem proving system that uses the mathematics of domain theory...
  • HOL88

  • Referenced in 2 articles [sw19615]
  • System is an environment for interactive theorem proving in a higher-order logic. Its most...
  • Autosubst

  • Referenced in 2 articles [sw22669]
  • Bruijn terms and parallel substitutions. In Interactive Theorem Proving. Reasoning about syntax with binders plays...
  • LPTP

  • Referenced in 7 articles [sw01822]
  • LPTP is an interactive theorem prover in which one can prove correctness properties of pure...
  • Vellvm

  • Referenced in 6 articles [sw13286]
  • interactive theorem prover. It includes multiple operational semantics and proves relations among them to facilitate...