• # 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...