• OTTER

  • Referenced in 204 articles [sw02904]
  • designed to prove theorems stated in first-order logic with equality. Otter’s inference rules...
  • VAMPIRE

  • Referenced in 151 articles [sw02918]
  • automatic theorem prover for first-order classical logic. It consists of a shell ... kernel. The kernel implements the calculi of ordered binary resolution and superposition for handling equality ... ordered unit equalities, and a lightweight basicness. The CASC version uses the Knuth-Bendix ordering ... accepts a problem in the full first-order logic syntax, clausifies it and performs...
  • E Theorem Prover

  • Referenced in 114 articles [sw10187]
  • theorem prover for full first-order logic with equality. It accepts a problem specification, typically ... consisting of a number of first-order clauses or formulas, and a conjecture, again either ... powerful and friendly reasoning systems for first-order logic. The prover has successfully participated...
  • ETPS

  • Referenced in 132 articles [sw06302]
  • automated theorem-prover for first-order logic and type theory. The latter...
  • SPASS

  • Referenced in 87 articles [sw04108]
  • automated theorem prover for first-order logic with equality. So the input for the prover ... valid and because validity in first-order logic is undecidable, SPASS may run forever without...
  • TPS

  • Referenced in 64 articles [sw00973]
  • automated theorem-prover for first-order logic and type theory. The latter...
  • Prover9

  • Referenced in 90 articles [sw04969]
  • automated theorem prover for first-order and equational logic, and Mace4 searches for finite models...
  • KeY

  • Referenced in 51 articles [sw09969]
  • novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly...
  • Ivy

  • Referenced in 21 articles [sw10279]
  • Preprocessor and Proof Checker for First-Order Logic. This case study shows how non-ACL2 ... resolution/paramodulation automated theorem proving for first-order logic. The top ACL2 function takes a conjecture...
  • SCR

  • Referenced in 20 articles [sw06939]
  • semantics by enabling events in first-order logic via two symbols pred and succ. This ... slight extension of first-order logic allows us to increase the readability...
  • iProver

  • Referenced in 20 articles [sw09707]
  • instantiation-based theorem prover for first-order logic. iProver is an instantiation-based theorem prover ... Inst-Gen calculus, complete for first-order logic. One of the distinctive features of iProver...
  • GEOTHER 1.1

  • Referenced in 27 articles [sw02842]
  • English or Chinese statement, into a first-order logical formula, or into algebraic expressions; draw...
  • REDLOG

  • Referenced in 122 articles [sw04250]
  • logic system, i.e., a system that provides algorithms for the symbolic manipulation of first-order...
  • ModLeanTAP

  • Referenced in 17 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...
  • Princess

  • Referenced in 17 articles [sw06872]
  • Theorem Proving in First-Order Logic modulo Linear Integer Arithmetic. Princess is a theorem prover...
  • Athena

  • Referenced in 9 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...
  • PARTHEO

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

  • Referenced in 12 articles [sw04175]
  • automated theorem prover for first order clausal logic. It accepts problems formulated in tptp ... problems than propositional approaches. Darwin is the first implementation of the Model Evolution Calculus ... lifts the propositional DPLL procedure to first-order logic. One of the main motivations ... possibility of migrating to the first-order level some of those very effective search techniques...
  • FORS

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

  • Referenced in 9 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...