• GHC

  • Referenced in 43 articles [sw23765]
  • additional syntactic construct, guard. Although Guarded Horn Clauses can be classified into the family ... viewed as a generalization of these frameworks. The simplicity and generality of GHC will make ... implemented with the same time-complexity as the time-complexity of many- to-one communication ... implementation of exhaustive solution search for Horn- clause programs. We showed how to automatically compile...
  • NiVER

  • Referenced in 18 articles [sw06958]
  • problem, Variable Elimination Resolution, has exponential space complexity. To tackle that, the backtracking-based DPLL ... variables), 58% decrease in $K$ (Number of clauses) and 46% decrease in $L$ (Literal count ... hence, can be incorporated into all general purpose SAT solvers...
  • ProGolem

  • Referenced in 4 articles [sw13855]
  • least general generalisation (RLGG) which are based on subsumption relative to a bottom clause. With ... Plotkin’s RLGG, clause length grows exponentially in the number of examples. By contrast ... bottom clause, clause length is bounded by the length of the initial bottom clause. ARMGs ... cases where clauses in the target theory are long and complex...
  • SMTS

  • Referenced in 1 article [sw29289]
  • SMTS: distributed, visualized constraint solving. The inherent complexity of parallel computing makes development, resource monitoring ... design (i) is based on a general parallelization technique that supports recursively combining algorithm portfolios ... executions, and visualizing solving, structure, and learned clauses of SMT instances...
  • Coq

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

  • Referenced in 622 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • KANT/KASH

  • Referenced in 156 articles [sw00481]
  • KASH/KANT is a computer algebra system (CAS) for...
  • ManySAT

  • Referenced in 36 articles [sw00544]
  • ManySAT: a parallel SAT solver. ManySAT, a new...
  • MiniSat

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

  • Referenced in 259 articles [sw00740]
  • PSPLIB -- a project scheduling problem library. We present...
  • R

  • Referenced in 8776 articles [sw00771]
  • R is a language and environment for statistical...
  • SCIP

  • Referenced in 484 articles [sw01091]
  • SCIP is currently one of the fastest non...
  • ML

  • Referenced in 517 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • ALGOL 68

  • Referenced in 291 articles [sw01226]
  • ALGOL 68 (short for ALGOrithmic Language 1968) is...
  • Ada95

  • Referenced in 289 articles [sw01753]
  • Ada is a structured, statically typed, imperative, wide...
  • OTTER

  • Referenced in 316 articles [sw02904]
  • Our current automated deduction system Otter is designed...
  • CHIP

  • Referenced in 80 articles [sw03450]
  • Solving a cutting-stock problem with the constraint...
  • PVS

  • Referenced in 624 articles [sw03484]
  • PVS is a verification system: that is, a...
  • Eiffel

  • Referenced in 289 articles [sw03522]
  • Eiffel is an ISO-standardized, object-oriented programming...