• Isar

  • Referenced in 91 articles [sw04599]
  • examples of this kind of semi-automated reasoning systems include Coq, PVS, HOL, and Isabelle ... Paradoxically, none of the existing semi-automated reasoning systems have an adequate primary notion ... just maintenance). The Intelligible semi-automated reasoning (Isar) approach to readable formal proof documents sets ... logic, and integrates a broad range of automated proof methods. Interactive proof development is supported...
  • LCF

  • Referenced in 110 articles [sw08360]
  • form a thriving paradigm in computer assisted reasoning. Many of the developments of the last ... uence on the ¯eld of automated reasoning has been diverse and profound...
  • NQTHM

  • Referenced in 91 articles [sw07543]
  • logic and its theorem prover” [J. Autom. Reasoning 4, No.2, 117-172 (1988)]. However...
  • MaLARea

  • Referenced in 26 articles [sw10278]
  • MaLARea: a Metasystem for Automated Reasoning in Large Theories. MaLARea (a Machine Learner for Automated ... simple metasystem iteratively combining deductive Automated Reasoning tools (now the E and the SPASS...
  • HR

  • Referenced in 25 articles [sw10392]
  • applications of HR to automated reasoning include the generation of constraints for constraint satisfaction problems ... generation of lemmas for automated theorem proving, and the production of benchmark theorems...
  • GEX

  • Referenced in 23 articles [sw09961]
  • various mathematical concepts. As an automated reasoning software, we can build dynamic logic models which ... most of the effective methods for geometric reasoning introduced in the past twenty years, including ... angle method. With these methods, users may automated prove geometry theorems, to discover new prrperties...
  • MetaPRL

  • Referenced in 22 articles [sw04624]
  • with support for interactive proof and automated reasoning. A primary feature of MetaPRL...
  • MathWeb

  • Referenced in 14 articles [sw10293]
  • MathWeb software bus for distributed mathematical reasoning. Automated reasoning systems have reached a high degree ... last decade. Many reasoning tasks can be delegated to an automated theorem prover ... people other than their own developers. The reasons for this seem to be that...
  • RSat

  • Referenced in 18 articles [sw13117]
  • RSat is developed by the UCLA Automated Reasoning Group...
  • MMP/Geometer

  • Referenced in 14 articles [sw00584]
  • MMP/Geometer – a software package for automated geometric reasoning. We introduce a software package, MMP/Geometer, developed...
  • Sparkle

  • Referenced in 9 articles [sw09803]
  • based on lazy graph-rewriting. This allows reasoning to take place on the program itself ... uses di.erent concepts. Secondly, Sparkle supports automated reasoning. Trivial goals will automatically be discarded...
  • AURA

  • Referenced in 9 articles [sw07015]
  • theorem prover: An incarnation of AURA (AUtomated Reasoning Assistant...
  • ETPS

  • Referenced in 131 articles [sw06302]
  • proving include hardware and software verification, partial automation of various mathematical activities, promoting development ... these disciplines, expert systems which can reason, and certain aspects of artificial intelligence...
  • HOLyHammer

  • Referenced in 5 articles [sw11553]
  • that, the service uses several automated reasoning systems combined with several premise selection methods trained...
  • Jakarta

  • Referenced in 18 articles [sw01269]
  • JaKarTa is a toolset for specifying and reasoning about the JavaCard platform. The main ingredients ... assistants; the JaKarTa Automation Kit (JAK), a toolset to support reasoning about executable specifications within...
  • TPS

  • Referenced in 62 articles [sw00973]
  • proving include hardware and software verification, partial automation of various mathematical activities, promoting development ... these disciplines, expert systems which can reason, and certain aspects of artificial intelligence...
  • Valigator

  • Referenced in 3 articles [sw00994]
  • that efficiently combines symbolic computation and automated reasoning in a uniform framework. The system offers...
  • Equinox

  • Referenced in 1 article [sw09768]
  • anatomy of Equinox -- an extensible automated reasoning tool for first-order logic and beyond. Equinox ... automated reasoning tool for first-order logic. It is also a framework for building highly ... targeted automated reasoning tools for specific domains.par The aim behind Equinox is to obtain ... automated reasoning tool with a modular and extensible architecture. SAT modulo theory (SMT) solvers have...
  • Aximo

  • Referenced in 4 articles [sw15031]
  • Aximo: Automated Axiomatic Reasoning for Information Update. Aximo is a software written in C++ that...
  • FORMULA 2.0

  • Referenced in 2 articles [sw13248]
  • domain-specific abstractions and compilers, (2) efficient reasoning and compilation of input programs, (3) diverse ... easily express rich synthesis / verification problems. Automated reasoning is enabled by efficient symbolic execution...