• VAMPIRE

  • Referenced in 237 articles [sw02918]
  • automatic theorem prover for first-order classical logic. It consists of a shell...
  • HOL Light

  • Referenced in 288 articles [sw06580]
  • interactive proof assistant for classical higher-order logic, intended as a clean and simplified version...
  • Isar

  • Referenced in 140 articles [sw04599]
  • logic implementation. Theories, theorems, proof procedures etc. may be used interchangeably between Isabelle-classic proof ... support a wide range of object-logics. The current end-user setup is mainly...
  • Zenon

  • Referenced in 22 articles [sw06753]
  • automated theorem prover for first order classical logic (with equality), based on the tableau method...
  • Leo-III

  • Referenced in 14 articles [sw18516]
  • agent-based deduction system for classical higher-order logic is developed. Leo-III combines ... support for reasoning in expressive non-classical logics...
  • 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 non-classical logics. Along the way, it eliminates from...
  • leanCoP

  • Referenced in 24 articles [sw09756]
  • very compact theorem prover for classical first-order logic, based on the connection (tableau) calculus ... connection calculus for intuitionistic logic. leanCoP 2.0 extends the classical prover leanCoP 2.0 by adding...
  • Lparse

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

  • Referenced in 122 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 15 articles [sw09757]
  • calculus for first-order 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...
  • 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...
  • TeMP

  • Referenced in 12 articles [sw09989]
  • FOTL, is an extension of classical first-order 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 truth-tables in the classical propositional logic. This is, in fact, a special...
  • nanoCoP

  • Referenced in 4 articles [sw21547]
  • clausal automated theorem prover for classical first-order logic. It is based ... clausal connection calculus for classical logic. More details about the calculus can be found ... nanoCoP: Theorem prover for classical first-order logic with equality. Based on the non-clausal...
  • Psyche

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

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

  • Referenced in 5 articles [sw22624]
  • Lolliproc: to concurrency from classical linear logic via Curry-Howard and control. While many type ... languages of the full power of linear logic -- including double-negation 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...
  • Gen2sat

  • Referenced in 3 articles [sw16745]
  • wide variety of propositional non-classical logics given in terms of a sequent calculus...