
SATO
 Referenced in 197 articles
[sw04451]
 satisfiability (SAT) problem of propositional logic. In the last decade, we developed a very efficient...

Gringo
 Referenced in 109 articles
[sw04630]
 programs provided by users into equivalent propositional logic programs. The answer sets of such programs...

KLONE
 Referenced in 41 articles
[sw28891]
 closely related to propositional modal logics and logics of programs (such as propositional dynamic logic...

HYSDEL
 Referenced in 39 articles
[sw05200]
 systems, automata, ifthenelse and propositional logic rules. Once a hybrid system is modeled...

ILTP
 Referenced in 29 articles
[sw00437]
 Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem ... systems for firstorder and propositional intuitionistic logic. It includes two problem collections for first ... order and propositional intuitionistic ATP systems and tools for converting the problems into the input ... about currently available ATP systems for intuitionistic logic and their performance results on the problems...

ModLeanTAP
 Referenced in 19 articles
[sw12368]
 ModLeanTAP: Lean Tableaubased Deduction for Propositional Modal Logics. ModLeanTAP is a lean Prolog implementation ... modular labelled tableau calculus for propositional modal logics (where the labels contain free and universal...

QUBOS
 Referenced in 25 articles
[sw09580]
 QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers. We describe QUBOS (QUantified BOolean Solver ... logic. The procedure is based on nonclausal simplification techniques that reduce formulae to a propositional...

Imogen
 Referenced in 11 articles
[sw11384]
 Polarized Inverse Method for Intuitionistic Propositional Logic. In this paper we describe Imogen, a theorem ... prover for intuitionistic propositional logic using the focused inverse method. We represent finegrained control ... method against seven other systems on the propositional fragment of the ILTP library. We found...

TRP++
 Referenced in 18 articles
[sw14679]
 theorem prover for Propositional Linear Time Temporal Logic based on the temporal resolution calculus ... clausal resolution approach to propositional temporal logic; Creating an experimental environment to try different modifications...

STRIP
 Referenced in 15 articles
[sw04650]
 theorem prover for intuitionistic propositional logic with two main characteristics: it deals with the duplication...

Cogent
 Referenced in 14 articles
[sw01300]
 machinelevel interpretation of expressions into propositional logic, and supports finite machinelevel variables...

fCube
 Referenced in 9 articles
[sw11383]
 fCube: an efficient prover for intuitionistic propositional logic. We present fCube, a theorem prover ... intuitionistic propositional logic based on a tableau calculus. The main novelty of fCube is that...

TABLEAUX
 Referenced in 18 articles
[sw11674]
 general theorem proving system for propositional modal logics, called TABLEAUX. The main feature...

Ltur
 Referenced in 40 articles
[sw11689]
 expression in propositional calculus is a fundamental problem in the area of logic programming ... fact that the basic solution techniques for propositional Horn formulae have been shown ... design of efficient interpreters for some predicate logicbased languages such as Hornlog...

MaTest
 Referenced in 11 articles
[sw11873]
 speaking, defined a list of connectives as logical matrices, with a set of designated values ... truthtables in the classical propositional logic. This is, in fact, a special case...

LPL software
 Referenced in 19 articles
[sw04860]
 Language, Proof and Logic covers topics such as the boolean connectives, formal proof techniques, quantifiers ... soundness and completeness for propositional and predicate logic, as well as an accessible sketch...

leanTAP
 Referenced in 41 articles
[sw09985]
 modal logics T, K4 and S4. The paper is restricted to the propositional case ... extended to the case of quantified modal logics as long as the Barcan formula...

Darwin
 Referenced in 26 articles
[sw04175]
 automated theorem prover for first order clausal logic. It accepts problems formulated in tptp ... scales better on such problems than propositional approaches. Darwin is the first implementation ... Evolution Calculus lifts the propositional DPLL procedure to firstorder logic. One of the main ... firstorder version of the (binary) propositional splitting inference rule...

SMTCoq
 Referenced in 7 articles
[sw32310]
 solver ZChaff, for propositional logic, and the SMT solvers veriT and CVC4, for the quantifier...

bv2epr
 Referenced in 7 articles
[sw07142]
 translation from QF_BV into effectively propositional logic (EPR). This allows us to solve...