• OTTER

  • Referenced in 316 articles [sw02904]
  • current automated deduction system Otter is designed to prove theorems stated in first-order logic...
  • ETPS

  • Referenced in 157 articles [sw06302]
  • Linux systems, and to some extent under Windows. Potential applications of automated theorem proving include ... hardware and software verification, partial automation of various mathematical activities, promoting development of formal theories ... wide variety of disciplines, deductive information systems for these disciplines, expert systems which can reason...
  • TPS

  • Referenced in 71 articles [sw00973]
  • Linux systems, and to some extent under Windows. Potential applications of automated theorem proving include ... hardware and software verification, partial automation of various mathematical activities, promoting development of formal theories ... wide variety of disciplines, deductive information systems for these disciplines, expert systems which can reason...
  • SAD

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

  • Referenced in 41 articles [sw03709]
  • systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated ... natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which...
  • MaLARea

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

  • Referenced in 21 articles [sw21343]
  • Deduction Proofs at the Assertion Level. The Tramp system transforms the output of several automated ... first order logic with equality into natural deduction proofs at the assertion level. Through this ... interface, other systems such as proof presentation systems or interactive deduction systems can access proofs...
  • daTac

  • Referenced in 3 articles [sw26325]
  • system daTac is to do automated deduction in first-order logic with equality. Its speciality...
  • Grail

  • Referenced in 7 articles [sw24229]
  • assistant for categorial grammar logics. The Grail system is a tool for the development ... fragments for categorial logics. Grail is an automated theorem prover based on proof nets ... graph-based representation of proofs, and labeled deduction...
  • KIDS

  • Referenced in 11 articles [sw15441]
  • Kestrel Interactive Development System (KIDS), which provides automated support for the development of correct ... described. The system has components for performing algorithm design, deductive inference, program simplification, partial evaluation...
  • MPTP 0.2

  • Referenced in 45 articles [sw02589]
  • Library (MML) available to current first-order automated theorem provers (ATPs) (and vice versa ... Mizar schemes are now handled by the system, too, by remembering (and, if necessary, abstracting ... longer detected by the ATP systems, suggesting that the `Mizar deconstruction’ done by MPTP ... premises are selected by a machine-learning system trained on previous proofs...
  • F*

  • Referenced in 20 articles [sw27563]
  • puts together the automation of an SMT-backed deductive verification tool with the expressive power ... underlying cryptographic primitives. F*’s type system includes dependent types, monadic effects, refinement types...
  • Symlog

  • Referenced in 3 articles [sw32623]
  • Symlog. Automated advice in Fitch-style proof construction. Symlog is a system for learning symbolic ... formal proofs in Fitch-style natural deduction systems of propositional and predicate logic...
  • LogAnswer

  • Referenced in 3 articles [sw21369]
  • deduction-based question answering system. (System description). LogAnswer is an open domain question answering system ... which employs an automated theorem prover to infer correct replies to natural language questions...
  • ANDP

  • Referenced in 1 article [sw29686]
  • implement automated natural deduction prover (ANDP), the natural deduction was adapted from Gentzen system. There...
  • MizarMode

  • Referenced in 18 articles [sw01973]
  • design principles behind the Mizar system, and show how these design principles -- mainly the concentration ... methods and tools now include, e.g., the automated generation of proof skeletons, semantic browsing ... learning tools like the Mizar Proof Advisor, deductive tools like MoMM, etc. We give...
  • KEIM

  • Referenced in 1 article [sw19608]
  • KEIM: A toolkit for automated deduction. KEIM is a collection of software modules, written ... used in the implementation of automated reasoning systems. KEIM is intended to be used ... those who want to build or use deduction systems (such as resolution theorem provers) without...
  • Guardol

  • Referenced in 2 articles [sw28543]
  • Guardol system generates Ada code from Guardol programs and also provides specification and automated verification ... translated to higher order logic, then deductively transformed to a form suitable...
  • mkbTT

  • Referenced in 6 articles [sw10018]
  • completion is a classical calculus in automated deduction for transforming a set of equations into ... this paper we describe the inference system, give the full proof of its correctness...
  • SNARK

  • Referenced in 4 articles [sw19611]
  • Automated Reasoning Kit. SNARK is an automated theorem-proving program being developed in Common Lisp ... High Performance Knowledge Base (HPKB) system, which deduces answers to questions based on large repositories ... information, and as the deductive core of NASA’s Amphion system, which composes software from...