
VAMPIRE
 Referenced in 241 articles
[sw02918]
 automatic theorem prover for firstorder classical logic. It consists of a shell...

HOL Light
 Referenced in 299 articles
[sw06580]
 interactive proof assistant for classical higherorder logic, intended as a clean and simplified version...

Isar
 Referenced in 144 articles
[sw04599]
 logic implementation. Theories, theorems, proof procedures etc. may be used interchangeably between Isabelleclassic proof ... support a wide range of objectlogics. The current enduser setup is mainly...

Zenon
 Referenced in 23 articles
[sw06753]
 automated theorem prover for first order classical logic (with equality), based on the tableau method...

LeoIII
 Referenced in 15 articles
[sw18516]
 agentbased deduction system for classical higherorder logic is developed. LeoIII combines ... support for reasoning in expressive nonclassical logics...

leanCoP
 Referenced in 26 articles
[sw09756]
 very compact theorem prover for classical firstorder logic, based on the connection (tableau) calculus ... connection calculus for intuitionistic logic. leanCoP 2.0 extends the classical prover leanCoP 2.0 by adding...

MaGIC
 Referenced in 14 articles
[sw11872]
 Connectives) is intended as a tool for logical research. It computes small algebras (normally with ... elements) suitable for modelling certain nonclassical logics. Along the way, it eliminates from...

Lparse
 Referenced in 42 articles
[sw04633]
 other semantics (classical negation, partial stable models) by translating them into normal logic programs...

GraphBase
 Referenced in 123 articles
[sw01555]
 letter words of English, the characters in classical works of fiction, highway distances between cities ... economy, college football scores, computational logic circuits, the Mona Lisa, etc. Others are based...

ileanCoP
 Referenced in 17 articles
[sw09757]
 calculus for firstorder intuitionistic logic. It extends the classical connection calculus by adding prefixes ... logic, which we prove correct and complete. The calculus was implemented by extending the classical...

nanoCoP
 Referenced in 6 articles
[sw21547]
 clausal automated theorem prover for classical firstorder logic. It is based ... clausal connection calculus for classical logic. More details about the calculus can be found ... nanoCoP: Theorem prover for classical firstorder logic with equality. Based on the nonclausal...

Tweety
 Referenced in 7 articles
[sw22090]
 comprehensive collection of Java libraries for logical aspects of artificial intelligence and knowledge representation. Tweety ... different knowledge representation formalisms such as classical logics, conditional logics, probabilistic logics, and argumentation. Furthermore...

DeLorean
 Referenced in 15 articles
[sw22920]
 applications. Despite the undisputed success of ontologies, classical ontologies are not suitable to deal with ... uncertainty and, consequently, several extensions with fuzzy logic and rough logic, among other formalisms, have ... translator from fuzzy rough ontology languages into classical ... ontology languages . This allows using classical (widely available) Description Logic inference engines to reason with...

BL2DV2
 Referenced in 37 articles
[sw10378]
 frontal logic, and their connection is realised as in a classical Delaunay approach. Quadrilaterals...

TeMP
 Referenced in 12 articles
[sw09989]
 FOTL, is an extension of classical firstorder logic by temporal operators for a discrete...

MaTest
 Referenced in 10 articles
[sw11873]
 speaking, defined a list of connectives as logical matrices, with a set of designated values ... generation of truthtables in the classical propositional logic. This is, in fact, a special...

Psyche
 Referenced in 5 articles
[sw28518]
 focused sequent calculus for polarised classical logic. Finally, Psyche features the ability to call decision...

Lolliproc
 Referenced in 5 articles
[sw22624]
 Lolliproc: to concurrency from classical linear logic via CurryHoward and control. While many type ... languages of the full power of linear logic  including doublenegation elimination  have remained elusive ... this paper we connect classical linear logic and concurrent functional programming in the language Lolliproc...

HOL2P
 Referenced in 4 articles
[sw21180]
 HOL2P  a system of classical higher order logic with second order polymorphism. This paper introduces ... logical system HOL2P that extends classical higher order logic (HOL) with type operator variables...

aleanTAP
 Referenced in 2 articles
[sw09987]
 declarative theorem prover for firstorder classical logic. We present αleanTAP, a declarative tableaubased ... prove ground theorems in firstorder classical logic. Since it is declarative, αleanTAP generates theorems...