• Isabelle/HOL

  • Referenced in 933 articles [sw01569]
  • Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed...
  • Isabelle

  • Referenced in 604 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed...
  • Isar

  • Referenced in 138 articles [sw04599]
  • reasoning systems include Coq, PVS, HOL, and Isabelle. Despite this success in actually formalizing parts ... development is supported directly as well. The Isabelle system offers Isar as an alternative proof ... procedures etc. may be used interchangeably between Isabelle-classic proof scripts and Isabelle/Isar documents. Isar ... generic as Isabelle, able to support a wide range of object-logics. The current...
  • Archive Formal Proofs

  • Referenced in 145 articles [sw28613]
  • Isabelle’s Archive of Formal Proofs (AFP): Mining the Archive of Formal Proofs. The Archive ... checked proofs developed using the proof assistant Isabelle. We perform an in-depth analysis...
  • Sledgehammer

  • Referenced in 116 articles [sw07047]
  • against first-order ATPs and built-in Isabelle tactics on a variety of benchmarks from ... Isabelle and the TPTP library. Sledgehammer provides an ideal test bench for individual features...
  • Nominal Isabelle

  • Referenced in 68 articles [sw12055]
  • General bindings and alpha-equivalence in Nominal Isabelle. Nominal Isabelle is a definitional extension ... paper we present an extension of Nominal Isabelle for dealing with general bindings, that means...
  • Isabelle/ZF

  • Referenced in 61 articles [sw04973]
  • Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed...
  • CeTA

  • Referenced in 42 articles [sw06584]
  • error message is displayed. Finally, we used Isabelle’s code generation facilities to generate ... certify termination proofs without even having Isabelle installed...
  • Nitpick

  • Referenced in 58 articles [sw00622]
  • card system. Our experimental results on Isabelle theories and the TPTP library indicate that Nitpick...
  • Locales

  • Referenced in 35 articles [sw12448]
  • They are available for the theorem prover Isabelle. In this paper, their semantics is defined ... extended by definitions and theorems. Interpretation to Isabelle’s global theories and proof contexts ... wider audience beyond the users of Isabelle. The discussed mechanisms include ML-style functors, type...
  • IsaPlanner

  • Referenced in 29 articles [sw02047]
  • proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques ... screenshot of IsaPlanner being used with Isabelle and Proof General) It is based ... Isabelle theorem prover and the Isar language. The main proof technique written in IsaPlanner ... based on Rippling. This is applicable within Isabelle”s Higher Order Logic, and can easily...
  • Proof General

  • Referenced in 53 articles [sw04901]
  • interactive proof systems, including Coq, LEGO, and Isabelle. Support for others...
  • Transfer

  • Referenced in 26 articles [sw21009]
  • type. Earlier work on the Isabelle Quotient package has yielded great progress in automation...
  • Lifting

  • Referenced in 26 articles [sw21010]
  • type. Earlier work on the Isabelle Quotient package has yielded great progress in automation...
  • CAVA LTL Modelchecker

  • Referenced in 15 articles [sw28830]
  • code has been completely verified using the Isabelle theorem prover. The checker consists of over ... code. The code is produced using the Isabelle Refinement Framework, which allows us to split...
  • Autoref

  • Referenced in 14 articles [sw12809]
  • structures.par Thanks to its integration with the Isabelle refinement framework and the Isabelle collection framework...
  • HYBRID

  • Referenced in 18 articles [sw00421]
  • package for higher-order syntax in Isabelle...
  • Isabelle/PIDE

  • Referenced in 12 articles [sw07185]
  • foundations of systems like HOL, Coq, or Isabelle have so far been counter-balanced ... integrate existing provers like Isabelle into a larger environment, that facilitates access by end-users...
  • Psi-calculi

  • Referenced in 11 articles [sw28573]
  • calculi in Isabelle. Psi-calculi are extensions of the pi-calculus, accommodating arbitrary nominal datatypes ... calculi in the interactive theorem prover Isabelle using its nominal datatype package. One distinctive feature...