• SATO

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

  • Referenced in 97 articles [sw04630]
  • programs provided by users into equivalent propositional logic programs. The answer sets of such programs...
  • KL-ONE

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

  • Referenced in 38 articles [sw05200]
  • systems, automata, if-then-else and propositional logic rules. Once a hybrid system is modeled...
  • ILTP

  • Referenced in 26 articles [sw00437]
  • Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem ... systems for first-order 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 18 articles [sw12368]
  • ModLeanTAP: Lean Tableau-based 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 24 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...
  • STRIP

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

  • Referenced in 10 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 fine-grained control ... method against seven other systems on the propositional fragment of the ILTP library. We found...
  • Cogent

  • Referenced in 14 articles [sw01300]
  • machine-level interpretation of expressions into propositional logic, and supports finite machine-level variables...
  • 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 logic-based languages such as Hornlog...
  • TRP++

  • Referenced in 15 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...
  • fCube

  • Referenced in 7 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...
  • MaTest

  • Referenced in 10 articles [sw11873]
  • speaking, defined a list of connectives as logical matrices, with a set of designated values ... truth-tables in the classical propositional logic. This is, in fact, a special case...
  • LPL software

  • Referenced in 18 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 38 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 25 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 first-order logic. One of the main ... first-order version of the (binary) propositional splitting inference rule...
  • bv2epr

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

  • Referenced in 49 articles [sw09707]
  • Inst-Gen calculus, complete for first-order logic. One of the distinctive features of iProver ... modular combination of instantiation and propositional reasoning. In particular, any state...