• LEO-II

  • Referenced in 51 articles [sw00512]
  • higher-order logic. At present LEO-II can cooperate with TPTP compliant first-order automated ... division (automation of higher-order logic) at CASC-J5. At CASC ... also participate in the first-order divisions FOF and CNF and performed reasonably well...
  • ILTP

  • Referenced in 26 articles [sw00437]
  • Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem ... proving (ATP) systems for first-order and propositional intuitionistic logic. It includes two problem collections ... first-order and propositional intuitionistic ATP systems and tools for converting the problems into ... about currently available ATP systems for intuitionistic logic and their performance results on the problems...
  • ICS

  • Referenced in 20 articles [sw21618]
  • decision procedure for a fragment of first-order logic. Terms are built from uninterpreted function...
  • FLOTTER

  • Referenced in 16 articles [sw29685]
  • clause normal form translator for first-order logic and a theorem prover for first-order...
  • MUltlog

  • Referenced in 19 articles [sw06604]
  • specification of a finitely-valued first-order logic and produces a sequent calculus, a natural...
  • CVC4

  • Referenced in 108 articles [sw09485]
  • satisfiability) of first-order formulas in a large number of built-in logical theories...
  • Athena

  • Referenced in 10 articles [sw09967]
  • Athena is based on many-sorted first-order logic. Many-sorted first-order logic ... Maria Manzano in her ”Extensions of first-order logic”) have argued that ... logic. It retains the tractability of first-order logic (completeness, compactness, structural induction over terms...
  • ModLeanTAP

  • Referenced in 18 articles [sw12368]
  • modular labelled tableau calculus for propositional modal logics (where the labels contain free and universal ... lean tableau-based prover for first-order logic leanTAP. ModLeanTAP Version 2.0 includes additional search...
  • TeMP

  • Referenced in 12 articles [sw09989]
  • TeMP: A temporal monodic prover. First-Order Temporal Logic ... FOTL, is an extension of classical first-order logic by temporal operators for a discrete ... used model of time). Formulae of this logic are interpreted over structures that associate with ... representing a moment in time, a first-order structure (D n ,I n ) with...
  • METEOR

  • Referenced in 16 articles [sw26327]
  • reduce redundant search. However, research in logic programming has led to sophisticated architectures giving high ... linear input proof procedure for full first-order logic, similar to but distinct from resolution...
  • FORS

  • Referenced in 16 articles [sw04848]
  • combination of ILP and numerical regression. First-order logic descriptions are induced to carve...
  • PARTHEO

  • Referenced in 15 articles [sw09981]
  • complete or-parallel theorem prover for first-order logic is presented. The proof calculus...
  • CoqHammer

  • Referenced in 15 articles [sw29396]
  • with the translation of problems to the logics of automated systems and the reconstruction ... achieved for statements ”close to” first-order logic and lemmas from the standard library...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • enriched by annotations in first-order logic.\parIts verification conditions -- constructed via a wp calculus...
  • ArgoCLP

  • Referenced in 12 articles [sw07192]
  • Coherent logic is a fragment of first-order logic. The structure of the formulae...
  • FACTORIE

  • Referenced in 13 articles [sw08947]
  • declarative language, such as SQL or first-order logic, we advocate using an imperative language...
  • E-Darvin

  • Referenced in 19 articles [sw06852]
  • automated theorem prover for first-order clausal logic with equality. It accepts problems in tptp...
  • E-KRHyper

  • Referenced in 12 articles [sw21368]
  • model generator and theorem prover for first-order logic with equality. It implements...
  • Zapato

  • Referenced in 11 articles [sw25425]
  • automatic theorem prover for quantifier-free first-order logic helps to determine the feasibility...
  • Saturate

  • Referenced in 10 articles [sw21351]
  • experimental theorem prover for first-order logic, primarily based on saturation...