• Isar

  • Referenced in 144 articles [sw04599]
  • system supporting both interactive proof development and some degree of automation have become quite successful ... existing semi-automated reasoning systems have an adequate primary notion of proof that is amenable ... Intelligible semi-automated 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 computer-checked 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 proof-checking 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 well-typed 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 object-oriented 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 first-order 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 first-order 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, rule-based 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, 117-172 (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 “code-generating”, “code-browsing ... 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 graph-based representation...