• MaLARea

  • Referenced in 50 articles [sw10278]
  • MaLARea: a Metasystem for Automated Reasoning in Large Theories. MaLARea (a Machine Learner for Automated ... simple metasystem iteratively combining deductive Automated Reasoning tools (now the E and the SPASS ... mode). Its intended use is in large theories, i.e. on a large number of problems...
  • HR

  • Referenced in 29 articles [sw10392]
  • named after mathematicians Hardy and Ramanujan -- performs theory formation in mathematical domains. It works ... effective, HR can produce large numbers of theorems for testing automated theorem provers (ATPs ... applications of HR to automated reasoning include the generation of constraints for constraint satisfaction problems...
  • PyZX

  • Referenced in 4 articles [sw40901]
  • large scale automated diagrammatic reasoning. The ZX-calculus is a graphical language for reasoning about ... calculus, we can intuitively reason about quantum theory, and optimise and validate quantum circuits ... open source library for automated reasoning with large ZX-diagrams. We give a brief introduction...
  • anthem

  • Referenced in 4 articles [sw30423]
  • anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report). In a recent paper ... program completion is extended to a large class of programs in the input language ... grounder gringo. We would like to automate the process of generating and simplifying completion formulas ... this software, in combination with automated reasoning tools, to verify that the program is correct...
  • HOARD ATINF

  • Referenced in 2 articles [sw28890]
  • prototype) is called HOARDATINF (Human Oriented Automated Reasoning on your Desk) and has been specialized ... discovering lemmata (using diagrams), handling standard theories in geometry such as commutativity and symmetry ... calculus), and proof verification in a rather large sense (by using capabilities of the calculus...
  • Imandra

  • Referenced in 1 article [sw37911]
  • Imandra Automated Reasoning System (system description). We describe Imandra, a modern computational logic theorem prover ... logic with theories, including arithmetic and datatypes. Imandra has novel features supporting large-scale industrial...
  • CoCoA

  • Referenced in 654 articles [sw00143]
  • CoCoA is a system for Computations in Commutative...
  • Coq

  • Referenced in 1890 articles [sw00161]
  • Coq is a formal proof management system. It...
  • GAP

  • Referenced in 3189 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • LEDA

  • Referenced in 263 articles [sw00509]
  • In the core computer science areas -- data structures...
  • LEO-II

  • Referenced in 51 articles [sw00512]
  • LEO-II is a standalone, resolution-based higher...
  • Maple

  • Referenced in 5373 articles [sw00545]
  • The result of over 30 years of cutting...
  • MapReduce

  • Referenced in 263 articles [sw00546]
  • MapReduce is a new parallel programming model initially...
  • Mathematica

  • Referenced in 6355 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • Matlab

  • Referenced in 13544 articles [sw00558]
  • MATLAB® is a high-level language and interactive...
  • Maxima

  • Referenced in 170 articles [sw00560]
  • Maxima is a system for the manipulation of...
  • MetiTarski

  • Referenced in 52 articles [sw00573]
  • Many inequalities involving the functions ln, exp, sin...
  • MiniSat

  • Referenced in 566 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • NAG

  • Referenced in 423 articles [sw00610]
  • Produced by experts for use in a variety...