• OTTER

  • Referenced in 316 articles [sw02904]
  • current automated deduction system Otter is designed to prove theorems stated in first-order logic ... fourth-generation Argonne National Laboratory deduction system whose ancestors (dating from the early 1960s) include...
  • Twelf

  • Referenced in 173 articles [sw06888]
  • specify, implement, and prove properties of deductive systems such as programming languages and logics. Large...
  • ELAN

  • Referenced in 108 articles [sw02179]
  • environment for specifying and prototyping deduction systems in a language based on rules controlled ... both the logical framework in which deduction systems can be expressed and combined...
  • ETPS

  • Referenced in 160 articles [sw06302]
  • been used extensively under Unix and Linux systems, and to some extent under Windows. Potential ... wide variety of disciplines, deductive information systems for these disciplines, expert systems which can reason ... expansion proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction ... interactive facilities of TPS for constructing natural deduction proofs have been used under the name...
  • XSB

  • Referenced in 144 articles [sw13877]
  • Logic Programming and Deductive Database system for Unix and Windows. XSB Prolog. It is being...
  • MPTP 0.2

  • Referenced in 50 articles [sw02589]
  • premises are selected by a machine-learning system trained on previous proofs ... that even a simple inductive or deductive system trained on formal mathematics can be sometimes...
  • TPS

  • Referenced in 73 articles [sw00973]
  • been used extensively under Unix and Linux systems, and to some extent under Windows. Potential ... wide variety of disciplines, deductive information systems for these disciplines, expert systems which can reason ... expansion proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction...
  • TRAMP

  • Referenced in 21 articles [sw21343]
  • Proofs into Natural Deduction Proofs at the Assertion Level. The Tramp system transforms the output ... into natural deduction proofs at the assertion level. Through this interface, other systems such ... proof presentation systems or interactive deduction systems can access proofs originally produced by any system...
  • KeYmaera

  • Referenced in 44 articles [sw03709]
  • hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover ... natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which...
  • DLV

  • Referenced in 33 articles [sw04640]
  • deductive database system, based on disjunctive logic programming, which offers front-ends to several advanced...
  • LEGO

  • Referenced in 107 articles [sw09685]
  • Jersey ML. It implements various related type systems - the Edinburgh Logical Framework (LF), the Calculus ... natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes...
  • MUltlog

  • Referenced in 19 articles [sw06604]
  • MUltlog is a system which takes as input the specification of a finitely-valued first ... produces a sequent calculus, a natural deduction system, and clause formation rules for this logic...
  • Delphin

  • Referenced in 18 articles [sw21365]
  • Delphin: Functional programming with deductive systems. We present the design and implementation of the strict...
  • MBase

  • Referenced in 17 articles [sw08724]
  • knowledge bases with a hierarchy of logical systems that are linked by logic morphisms. These ... various formats currently in use in deduction systems. On the other hand they define higher...
  • Leo-III

  • Referenced in 16 articles [sw18516]
  • project, a new agent-based deduction system for classical higher-order logic is developed...
  • MEDLAR

  • Referenced in 14 articles [sw02888]
  • general framework (LDS, labelled deductive systems) to produce the specific reasoning capabilities; exploration...
  • STeP

  • Referenced in 36 articles [sw17948]
  • restricted to finite-state systems, but combines model checking with deductive methods to allow...
  • Protege

  • Referenced in 60 articles [sw17512]
  • system. Protégé provides a graphic user interface to define ontologies. It also includes deductive classifiers...
  • MaLARea

  • Referenced in 50 articles [sw10278]
  • combining deductive Automated Reasoning tools (now the E and the SPASS ATP systems) with...
  • SAD

  • Referenced in 15 articles [sw09796]
  • System for automated deduction (SAD): A tool for proof verification. In this paper a proof...