
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 higherorder 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 stateoftheart 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 higherorder 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 connectionbased theorem proving into interactive proof assistants. JProver is a firstorder...

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...

OmegaANTS
 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 higherorder 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...