
ETPS
 Referenced in 150 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 134 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 69 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 10 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 38 articles
[sw19619]
 turn the interactive proof editor into a fully automatic theorem proving system...

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

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

IsaPlanner
 Referenced in 28 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...

Abella
 Referenced in 45 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...

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

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

FACTum
 Referenced in 1 article
[sw30951]
 based systems combining model checking and interactive theorem proving. In FACTum, the verification of overall ... interaction. Thus, in FACTum, we use interactive theorem proving to reason about the combination...