• Maude

  • Referenced in 492 articles [sw06233]
  • system supporting both equational and rewriting logic specification and programming for a wide range ... which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming ... Maude also supports rewriting logic computation...
  • Isabelle

  • Referenced in 375 articles [sw00454]
  • tools for proving those formulas in a logical calculus. The main application is the formalization...
  • Isabelle/HOL

  • Referenced in 359 articles [sw01569]
  • tools for proving those formulas in a logical calculus. The main application is the formalization...
  • OTTER

  • Referenced in 200 articles [sw02904]
  • prove theorems stated in first-order logic with equality. Otter’s inference rules are based ... research in abstract algebra and formal logic. Otter and its predecessors have been used ... areas of finite semigroups, ternary Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory...
  • Smodels

  • Referenced in 211 articles [sw04631]
  • stable model semantics of normal logic programs. The basic idea of ASP is to encode ... constraints of a problem as a logic program such that the answer sets (stable models ... solve the problem by letting a logic program engine to find the answer sets...
  • Z-Tree

  • Referenced in 276 articles [sw11707]
  • flexible both with respect to the logic of interaction and the visual representation, allowing...
  • HOL

  • Referenced in 260 articles [sw05492]
  • Higher Order Logic (HOL) is a programming environment in which theorems can be proved...
  • PRISM

  • Referenced in 251 articles [sw01186]
  • against specifications written in the probabilistic temporal logics PCTL and CSL. The tool features three...
  • ETPS

  • Referenced in 127 articles [sw06302]
  • automated theorem-prover for first-order logic and type theory. The latter ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... solving unification problems in higher-order logic. It has a formula editor which facilitates constructing ... been used under the name ETPS in logic courses at Carnegie Mellon for a number...
  • Kronos

  • Referenced in 226 articles [sw01270]
  • expressed in the real-time temporal logic TCTL...
  • GOLOG

  • Referenced in 153 articles [sw02159]
  • GOLOG: A logic programming language for dynamic domains. This paper proposes a new logic programming...
  • VAMPIRE

  • Referenced in 146 articles [sw02918]
  • automatic theorem prover for first-order classical logic. It consists of a shell ... problem in the full first-order logic syntax, clausifies it and performs a number...
  • ASSAT

  • Referenced in 141 articles [sw02524]
  • system for computing answer sets of a logic program by using SAT solvers. Briefly speaking ... given a ground logic program P, ASSAT(X), depending on the SAT solver X used...
  • HOL Light

  • Referenced in 137 articles [sw06580]
  • interactive proof assistant for classical higher-order logic, intended as a clean and simplified version ... clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof...
  • SATO

  • Referenced in 180 articles [sw04451]
  • satisfiability (SAT) problem of propositional logic. In the last decade, we developed a very efficient...
  • NQTHM

  • Referenced in 85 articles [sw07543]
  • computational logic handbook This book is a continuation of the same authors’ previous book entitled ... computational logic” (1979; Zbl 0448.68020). The truly important changes to the theorem prover since ... theorem prover. The significant changes in the logic itself are the efficient use of functions ... logic as new proof procedures upon the establishment of their soundness and the permission...
  • E Theorem Prover

  • Referenced in 111 articles [sw10187]
  • theorem prover for full first-order logic with equality. It accepts a problem specification, typically ... friendly reasoning systems for first-order logic. The prover has successfully participated in many competitions...
  • LCF

  • Referenced in 104 articles [sw08360]
  • proof assistant for higher order logic originally developed for reasoning about hardware.2 The multi-faceted ... logics. Code Milner wrote is still in use today, and the design of the hardware...
  • ELAN

  • Referenced in 84 articles [sw02179]
  • support the design of theorem provers, logic programming languages, constraints solvers and decision procedures ... support the design of theorem provers, logic programming languages, constraints solvers and decision procedures ... known paradigm of rewriting provides both the logical framework in which deduction systems...
  • Isar

  • Referenced in 83 articles [sw04599]
  • quite independent of the underlying logic, and integrates a broad range of automated proof methods ... tightly integrated into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures ... support a wide range of object-logics. The current end-user setup is mainly...