
Maude
 Referenced in 537 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/HOL
 Referenced in 626 articles
[sw01569]
 tools for proving those formulas in a logical calculus. The main application is the formalization...

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

OTTER
 Referenced in 236 articles
[sw02904]
 prove theorems stated in firstorder 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...

Datalog
 Referenced in 235 articles
[sw20023]
 Datalog is a declarative logic programming language that syntactically is a subset of Prolog ... origins date back to the beginning of logic programming, but it became prominent ... Jack Minker organized a workshop on logic and databases.[2] David Maier is credited with...

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

Smodels
 Referenced in 215 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...

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

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

HOL Light
 Referenced in 199 articles
[sw06580]
 interactive proof assistant for classical higherorder logic, intended as a clean and simplified version ... clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof...

ETPS
 Referenced in 134 articles
[sw06302]
 automated theoremprover for firstorder logic and type theory. The latter ... prove theorems of first and higherorder logic interactively, automatically, or in a mixture ... solving unification problems in higherorder logic. It has a formula editor which facilitates constructing ... been used under the name ETPS in logic courses at Carnegie Mellon for a number...

VAMPIRE
 Referenced in 177 articles
[sw02918]
 automatic theorem prover for firstorder classical logic. It consists of a shell ... problem in the full firstorder logic syntax, clausifies it and performs a number...

Kronos
 Referenced in 234 articles
[sw01270]
 expressed in the realtime temporal logic TCTL...

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

ASSAT
 Referenced in 147 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...

E Theorem Prover
 Referenced in 137 articles
[sw10187]
 theorem prover for full firstorder logic with equality. It accepts a problem specification, typically ... friendly reasoning systems for firstorder logic. The prover has successfully participated in many competitions...

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

LCF
 Referenced in 109 articles
[sw08360]
 Edinburgh LCF. A mechanized logic of computation. From LCF to HOL: a short history ... proof assistant for higher order logic originally developed for reasoning about hardware.2 The multifaceted ... logics. Code Milner wrote is still in use today, and the design of the hardware...

NQTHM
 Referenced in 88 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...

Isar
 Referenced in 107 articles
[sw04599]
 quite independent of the underlying logic, and integrates a broad range of automated proof methods ... tightly integrated into the Isabelle/Pure metalogic implementation. Theories, theorems, proof procedures ... support a wide range of objectlogics. The current enduser setup is mainly...