• # QUBOS

• Referenced in 25 articles [sw09580]
• QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers. We describe QUBOS (QUantified BOolean Solver ... decision procedure for quantified Boolean logic. The procedure is based on nonclausal simplification techniques that...
• # semprop

• Referenced in 18 articles [sw28383]
• Boolean formulas. The increasing role of quantified Boolean logic in many applications calls for practically ... propositional case are generalised to the quantified Boolean case and the occuring differences are discussed...
• # LPL software

• Referenced in 19 articles [sw04860]
• Logic covers topics such as the boolean connectives, formal proof techniques, quantifiers, basic set theory ... soundness and completeness for propositional and predicate logic, as well as an accessible sketch...
• # ToyElim

• Referenced in 3 articles [sw09900]
• function which takes a formula of propositional logic extended with operators for projection and circumscription ... these operators. Tasks like elimination of Boolean quantifiers, computation of uniform interpolants, certain forms ... formulas according to various semantics of logic programming can be expressed and integrated in this...
• # STABLE

• Referenced in 2 articles [sw11913]
• solver for hard verification problems combining Boolean reasoning with computer algebra. This paper presents ... solver, STABLE, for formulas of the quantifier-free logic over fixed-sized bit vectors...
• # DDDLIB

• Referenced in 1 article [sw00192]
• manipulating formulae in a first-order logic over Boolean variables and inequalities of the form ... with the standard Boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding functional properties...
• # SONOLAR

• Referenced in 2 articles [sw26291]
• Solver that solves quantifier-free fixed-size bit-vector logic formulas. The solver supports ... format including the following logics: Bit vectors (QF_BV). Bit vectors with arrays ... logic names are yet to be defined for this theory, the logics ... blasting to translate bitvector constraints to a Boolean formula and lets a SAT solver decide...