
Isar
 Referenced in 144 articles
[sw04599]
 system supporting both interactive proof development and some degree of automation have become quite successful ... existing semiautomated reasoning systems have an adequate primary notion of proof that is amenable ... Intelligible semiautomated reasoning (Isar) approach to readable formal proof documents sets out to bridge ... integrates a broad range of automated proof methods. Interactive proof development is supported directly...

AProVE
 Referenced in 154 articles
[sw07831]
 AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. AProVE ... most powerful systems for automated termination proofs of term rewrite systems (TRSs ... first tool which automates the new dependency pair framework [8] and therefore permits a completely ... flexible combination of different termination proof techniques. Due to this framework, AProVE 1.2 is also...

PROMELA
 Referenced in 30 articles
[sw07635]
 this language, and it can produce automated proofs for each type of property. SPIN either...

Matchbox
 Referenced in 25 articles
[sw10115]
 first program that delivers automated proofs of termination for some difficult string rewriting systems...

Coq/SSReflect
 Referenced in 69 articles
[sw09360]
 proof that evolved from the computerchecked proof of the Four Colour Theorem and which ... logic to provide effective automation for many small, clerical proof steps. This is often accomplished...

LCF
 Referenced in 157 articles
[sw08360]
 history. The original LCF system was a proofchecking program developed at Stanford University ... whose in°uence on the ¯eld of automated reasoning has been diverse and profound ... descendents of LCF is HOL, a proof assistant for higher order logic originally developed...

EasyCrypt
 Referenced in 30 articles
[sw09738]
 present EasyCrypt, an automated tool for elaborating security proofs of cryptographic systems from proof sketches ... solvers and automated theorem provers, and then compiled into verifiable proofs in the CertiCrypt framework...

ML
 Referenced in 517 articles
[sw01218]
 ensures type safety – there is a formal proof that a welltyped ML program does ... formal languages, such as in compiler writing, automated theorem proving and formal verification. (wikipedia...

MetaPRL
 Referenced in 26 articles
[sw04624]
 system implementation with support for interactive proof and automated reasoning. A primary feature of MetaPRL...

Mtac
 Referenced in 14 articles
[sw13075]
 Effective support for custom proof automation is essential for large scale interactive proof development. However...

Zenon
 Referenced in 23 articles
[sw06753]
 Zenon: An extensible automated theorem prover producing checkable proofs. We present Zenon, an automated theorem ... environment, an objectoriented algebraic specification and proof system, which is able to produce OCaml ... directly generate Coq proofs (proof scripts or proof terms), which can be reinserted ... extended, which makes specific (and possibly local) automation possible in Focal...

OTTER
 Referenced in 316 articles
[sw02904]
 current automated deduction system Otter is designed to prove theorems stated in firstorder logic ... strategies for directing and restricting searches for proofs. Otter can also be used...

SPASS
 Referenced in 179 articles
[sw04108]
 SPASS is an automated theorem prover for firstorder logic with equality. So the input ... results in the final output SPASS beiseite: Proof found. if the formula is valid, SPASS...

ETPS
 Referenced in 158 articles
[sw06302]
 proving include hardware and software verification, partial automation of various mathematical activities, promoting development ... facilities for searching for expansion proofs, translating these into natural deduction proofs, constructing natural deduction...

A3PAT
 Referenced in 8 articles
[sw21587]
 A3PAT, an approach for certified automated termination proofs. Software engineering, automated reasoning, rulebased programming ... discover and moreover certify, with full automation, termination proofs for term rewriting systems. It consists...

NQTHM
 Referenced in 149 articles
[sw07543]
 correct and using them efficiently as new proof procedures” [in “The correctness problem in computer ... computational logic and its theorem prover” [J. Autom. Reasoning 4, No.2, 117172 (1988)]. However...

HipSpec
 Referenced in 14 articles
[sw07736]
 Automating inductive proofs using theory exploration. HipSpec is a system for automatically deriving and proving...

MizarMode
 Referenced in 18 articles
[sw01973]
 facilitate this kind of proof development by a number of “codegenerating”, “codebrowsing ... tools now include, e.g., the automated generation of proof skeletons, semantic browsing of the articles...

CoLoR
 Referenced in 38 articles
[sw09806]
 rewrite relations and its application to the automated verifications of termination certificates. Termination ... notably required for programs formulated in proof assistants. It is a very active subject ... proof assistant Coq. We also present its application to the automated verification of termination certificates...

Grail
 Referenced in 7 articles
[sw24229]
 Grail: An automated proof assistant for categorial grammar logics. The Grail system is a tool ... logics. Grail is an automated theorem prover based on proof nets, a graphbased representation...