• ETPS

  • Referenced in 161 articles [sw06302]
  • automated theorem-prover for first-order logic and type theory. The latter...
  • REDLOG

  • Referenced in 166 articles [sw04250]
  • manipulation of first-order formulas over some temporarily fixed language and theory. In contrast...
  • Boolector

  • Referenced in 32 articles [sw00085]
  • vectors and arrays. Satisfiability Modulo Theories (SMT) is the problem of deciding satisfiability ... formula, expressed in a combination of first-order theories. We present the architecture and selected...
  • CVC4

  • Referenced in 125 articles [sw09485]
  • source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used ... first-order formulas in a large number of built-in logical theories and their combination...
  • TPS

  • Referenced in 75 articles [sw00973]
  • automated theorem-prover for first-order logic and type theory. The latter...
  • FOCI

  • Referenced in 62 articles [sw12868]
  • quantifier-free first-order formulas. It supports certain interpreted theories, such as equality, uninterpreted functions...
  • OTTER

  • Referenced in 320 articles [sw02904]
  • designed to prove theorems stated in first-order logic with equality. Otter’s inference rules ... includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing ... Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry. Note: Otter/Mace2...
  • f2lp

  • Referenced in 10 articles [sw09898]
  • certain conditions, system f2lp turns a first-order theory under the stable model semantics into...
  • LPTP

  • Referenced in 7 articles [sw01822]
  • pure Prolog programs. This is a first-order theory that contains induction principles corresponding...
  • CoqMTU

  • Referenced in 3 articles [sw19138]
  • universes parametrized by a decidable first-order theory. e study a complex type theory ... predicative hierarchy of universes and a first-order theory T built in its conversion relation ... theory T is specified abstractly, by a set of constructors, a set of defined symbols ... principle relying on crucial properties of first-order structures satisfying the axioms. We first show...
  • FOIL

  • Referenced in 31 articles [sw24694]
  • first-order learning system that uses information in a collection of relations to construct theories...
  • CoqMT

  • Referenced in 6 articles [sw19139]
  • Modulo Theory. Coq Modulo Theory (CoqMT) is an extension of the Coq proof assistant incorporating ... validity entailment for user-defined first-order equational theories. Such a mechanism strictly enriches ... checking algorithm and the integration of first-order decision procedures. We present here CoqMT...
  • anthem

  • Referenced in 4 articles [sw30423]
  • anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report). In a recent paper...
  • Nitpick

  • Referenced in 64 articles [sw00622]
  • builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification ... card system. Our experimental results on Isabelle theories and the TPTP library indicate that Nitpick...
  • FORT

  • Referenced in 2 articles [sw28637]
  • tool that implements the first-order theory of rewriting for the decidable class of left ... satisfy arbitrary properties expressible in the first-order theory of rewriting. In this paper...
  • TSAT++

  • Referenced in 3 articles [sw21350]
  • lazy SAT-based approach to satisfiability modulo theories (SMT). SMT is the problem of determining ... literals, where T is a first-order theory for which a satisfiability procedure...
  • PrASP

  • Referenced in 3 articles [sw18512]
  • reasoning based on logic programming and first-order theories under stable model semantics. This system ... AnsProlog) as well as first-order logic formulas (with stable model semantics), annotated with conditional...
  • AGES

  • Referenced in 3 articles [sw32284]
  • automatically generate models for order-sorted first-order theories. The tool uses linear algebra techniques...
  • AVATAR

  • Referenced in 21 articles [sw28636]
  • first-order resolution and superposition theorem provers called AVATAR (Advanced Vampire Architecture for Theories...
  • Mcmt

  • Referenced in 24 articles [sw11911]
  • state systems whose state variables are arrays. Theories specify the properties of the indexes ... system are described by quantified first-order formulae. The core of the system ... points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques, efficient heuristics...