
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 highlevel modeling capacities of answer...

CVC4
 Referenced in 109 articles
[sw09485]
 large number of builtin 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 AndInverter 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 highlevel 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 firstorder 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 nondeterminism and probabilities...

SMTRAT
 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 SMTRAT. Further modules for closed quantifierfree 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 firstorder theories...

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