• Smodels

  • Referenced in 239 articles [sw04631]
  • encode the constraints of a problem as a logic program such that the answer sets ... program correspond to the solutions of the problem ... Then we can solve the problem by letting a logic program engine to find...
  • ETPS

  • Referenced in 160 articles [sw06302]
  • prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... expansion proofs, and solving unification problems in higher-order logic. It has a formula editor ... students to concentrate on the essential logical problems underlying the proofs, and it gives them ... them. The rules of inference and predefined problems in ETPS are mostly taken from...
  • SATO

  • Referenced in 196 articles [sw04451]
  • methods for the satisfiability (SAT) problem of propositional logic. In the last decade, we developed ... solve over one hundred open quasigroup problems in design theory. We also experimented SATO...
  • VAMPIRE

  • Referenced in 258 articles [sw02918]
  • automatic theorem prover for first-order classical logic. It consists of a shell ... shell accepts a problem in the full first-order logic syntax, clausifies it and performs...
  • E Theorem Prover

  • Referenced in 206 articles [sw10187]
  • full first-order logic with equality. It accepts a problem specification, typically consisting ... friendly reasoning systems for first-order logic. The prover has successfully participated in many competitions...
  • NQTHM

  • Referenced in 151 articles [sw07543]
  • partial recursive functions. These changes in the logic were described completely in their “Metafunctions: proving ... proof procedures” [in “The correctness problem in computer science” (1981; Zbl 0476.68009)] and “The addition ... quantification and partial functions to a computational logic and its theorem prover” [J. Autom. Reasoning ... have been comparatively minor changes to the logic and the theorem prover since the publication...
  • CHIP

  • Referenced in 82 articles [sw03450]
  • Solving a cutting-stock problem with the constraint logic programming language CHIP...
  • TPS

  • Referenced in 73 articles [sw00973]
  • prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... expansion proofs, and solving unification problems in higher-order logic. It has a formula editor...
  • ILTP

  • Referenced in 28 articles [sw00437]
  • first-order and propositional intuitionistic logic. It includes two problem collections for first-order ... systems and tools for converting the problems into the input syntax of some existing intuitionistic ... systems for intuitionistic logic and their performance results on the problems in the ILTP library...
  • AMRCLAW

  • Referenced in 72 articles [sw15478]
  • conservation form, problems with source terms of capacity functions, and logically rectangular curvilinear grids...
  • Mathpert

  • Referenced in 18 articles [sw24047]
  • found when computational “operators” have logical side conditions that must be satisfied before they ... internal solution of the problem...
  • Darwin

  • Referenced in 26 articles [sw04175]
  • prover for first order clausal logic. It accepts problems formulated in tptp or tme format ... general faster and scales better on such problems than propositional approaches. Darwin is the first ... propositional DPLL procedure to first-order logic. One of the main motivations for this approach...
  • Ltur

  • Referenced in 40 articles [sw11689]
  • calculus is a fundamental problem in the area of logic programming for many reasons. Among...
  • Mercury

  • Referenced in 69 articles [sw08333]
  • existing logic programming systems, and close to conventional programming systems. Mercury addresses the problems...
  • CoqHammer

  • Referenced in 17 articles [sw29396]
  • proofs with the translation of problems to the logics of automated systems and the reconstruction ... relatively simple goals using available lemmas. The problem is to find appropriate lemmas ... achieved for statements ”close to” first-order logic and lemmas from the standard library...
  • CVC4

  • Referenced in 124 articles [sw09485]
  • theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove ... large number of built-in logical theories and their combination. CVC4 is the fourth...
  • Boolector

  • Referenced in 31 articles [sw00085]
  • Theories (SMT) is the problem of deciding satisfiability of a logical formula, expressed...
  • KL-ONE

  • Referenced in 41 articles [sw28891]
  • tableau algorithms for description logics. Description logics are a family of knowledge representation formalisms that ... reasoning problems (like subsumption and satisfiability) in a great variety of description logics...
  • QMLTP

  • Referenced in 11 articles [sw09915]
  • QMLTP problem library for first-order modal logics. The Quantified Modal Logic Theorem Proving (QMLTP ... proving (ATP) systems for first-order modal logics. The main purpose of the library ... QMLTP library includes 600 problems represented in a standardized extended TPTP syntax. Status and difficulty ... Furthermore, a small number of problems for multi-modal logic are included as well...
  • Coq/SSReflect

  • Referenced in 71 articles [sw09360]
  • higher-order nature of Coq’s underlying logic to provide effective automation for many small ... This is often accomplished by restating (”reflecting”) problems in a more concrete form, hence...