• HOL

  • Referenced in 532 articles [sw05492]
  • Higher Order Logic (HOL) is a programming environment in which theorems can be proved ... particularly suitable as a platform for implementing combinations of deduction, execution, and property checking...
  • ELAN

  • Referenced in 108 articles [sw02179]
  • support the design of theorem provers, logic programming languages, constraints solvers and decision procedures ... their combination. Its purpose is to support the design of theorem provers, logic programming languages ... offer a modular framework for studying their combination. ELAN takes from functional programming the concept ... both the logical framework in which deduction systems can be expressed and combined...
  • clasp

  • Referenced in 93 articles [sw07095]
  • solver for (extended) normal logic programs. It combines the high-level modeling capacities of answer...
  • CVC4

  • Referenced in 109 articles [sw09485]
  • large number of built-in logical theories and their combination. CVC4 is the fourth...
  • Curry

  • Referenced in 43 articles [sw08981]
  • combining them has grown over the last decade. However, integrated functional logic languages are currently ... ideas of existing functional logic languages and recent developments, and combines the most important features ... functional and logic languages. Thus, Curry can be the basis to combine the currently separated...
  • Prolog

  • Referenced in 69 articles [sw06518]
  • This opens contraint logic programming to the user combining the power of constraint programming...
  • ABC

  • Referenced in 37 articles [sw12910]
  • appearing in synchronous hardware designs. ABC combines scalable logic transformations based on And-Inverter Graphs...
  • PRISM

  • Referenced in 424 articles [sw01186]
  • against specifications written in the probabilistic temporal logics PCTL and CSL. The tool features three ... based on sparse matrices; and one which combines both symbolic and sparse matrix methods. PRISM...
  • Clingcon

  • Referenced in 34 articles [sw09892]
  • Clingcon is a hybrid solver combining the monolithic answer set solver Clingo ... solver for (extended) constraint normal logic programs. It combines the high-level modeling capacities ... finite integers can be used in the logic programs. The primary clingcon algorithm adopts state...
  • Hyperproof

  • Referenced in 24 articles [sw22172]
  • Unlike traditional treatments of first-order logic, Hyperproof combines graphical and sentential information, presenting...
  • CVC

  • Referenced in 48 articles [sw09462]
  • checker. Decision procedures for decidable logics and logical theories have proven to be useful tools ... implements a framework for combining subsidiary decision procedures for certain logical theories into a decision...
  • MathSAT

  • Referenced in 58 articles [sw09449]
  • several useful theories: (combinations of) equality and uninterpreted functions, difference logic, linear arithmetic...
  • ETPS

  • Referenced in 157 articles [sw06302]
  • allows students to concentrate on the essential logical problems underlying the proofs, and it gives ... work forwards, backwards, or in a combination of these modes, and provides facilities for rearranging ... Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof...
  • CoLoSS

  • Referenced in 14 articles [sw07016]
  • graded modal logic, and probabilistic modal logic. Logics are easily integrated into CoLoSS by providing ... synthesises decision procedures for modular combinations of logics that include the fusion of two modal ... reasoning support e.g. for logics interpreted over probabilistic automata that combine non-determinism and probabilities...
  • SMT-RAT

  • Referenced in 18 articles [sw13091]
  • modules. These modules can be combined to (1) an SMT solver or (2) a theory ... solver in order to extend the supported logics of an existing SMT solver ... supported logics of SMT-RAT. Further modules for closed quantifier-free formulas over the theory ... well as combinations of these logics with already supported logics (QF_UFLRA, QF_UFLIA...
  • SMART_

  • Referenced in 33 articles [sw04097]
  • logic and probabilistic analysis of complex systems. Smart can combine different formalisms in the same...
  • MEDLAR

  • Referenced in 14 articles [sw02888]
  • goals of the MEDLAR(MEchanising Deduction in Logics of Practical Reasoning)-II project ... model building, in a given combination of logics; the development of the general framework...
  • GraphBase

  • Referenced in 123 articles [sw01555]
  • economy, college football scores, computational logic circuits, the Mona Lisa, etc. Others are based ... quaternions. Graphs can be modified and combined by union, intersection, complementation, product, and forming line...
  • Boolector

  • Referenced in 28 articles [sw00085]
  • deciding satisfiability of a logical formula, expressed in a combination of first-order theories...
  • iProver

  • Referenced in 49 articles [sw09707]
  • order logic. One of the distinctive features of iProver is a modular combination of instantiation...