• AXIOM

  • Referenced in 169 articles [sw00063]
  • Axiom is a general purpose Computer Algebra system (CAS). It is useful for research...
  • E Theorem Prover

  • Referenced in 186 articles [sw10187]
  • formal proof for the conjecture, assuming the axioms. If a proof is found, the system...
  • GOLOG

  • Referenced in 169 articles [sw02159]
  • modeled, on the basis of user supplied axioms about the preconditions and effects of actions...
  • Pesca

  • Referenced in 126 articles [sw13664]
  • extend them by systems of nonlogical axioms. The implementation of Pesca is written...
  • MaLARea

  • Referenced in 43 articles [sw10278]
  • which in a consistent fashion use many axioms, lemmas, theorems, definitions and symbols. The system ... information to prune the set of available axioms for the next theorem proving cycle. Although...
  • Smallfoot

  • Referenced in 52 articles [sw09787]
  • separation logic, namely: avoidance of frame axioms (which say what a procedure does not change...
  • Ynot

  • Referenced in 35 articles [sw12334]
  • accessing a mutable store, and throwing/catching exceptions.The axioms of Ynot form a small trusted computing ... Type Theory (HTT). We show how these axioms can be combined with the powerful type...
  • ConGolog

  • Referenced in 48 articles [sw01801]
  • primitive actions can be user-defined by axioms in the situation calculus. Some mathematical properties...
  • IBM Scratchpad

  • Referenced in 34 articles [sw00429]
  • Axiom is a general purpose Computer Algebra system. It is useful for research and development ... programming language and a built-in compiler. Axiom has been in development since...
  • KL-ONE

  • Referenced in 40 articles [sw28891]
  • rôle in description logics (number restrictions, terminological axioms, and role constructors), and show how they...
  • UCPOP

  • Referenced in 38 articles [sw20687]
  • goals. In addition, UCPOP 4.1 allows domain axioms and predicates that call Common Lisp code...
  • HR

  • Referenced in 29 articles [sw10392]
  • generator to generate objects of interest from axiom sets (ii) performing the concept formation...
  • Separoids

  • Referenced in 20 articles [sw08819]
  • general mathematical properties of separoids and related axiom systems, as well as connections with other ... number of models of the separoid axioms, how the concept of separoid unifies a variety...
  • CC-Pi

  • Referenced in 26 articles [sw15033]
  • names in terms of restriction and structural axioms closer to nominal calculi than to variables...
  • ALDOR

  • Referenced in 24 articles [sw01220]
  • conceived as an extension language for the Axiom system, but is now used more...
  • MPTP

  • Referenced in 23 articles [sw02489]
  • Proof Advisor (MPA) used for selecting suitable axioms from the large library for an arbitrary...
  • SRASS

  • Referenced in 12 articles [sw21370]
  • SRASS -- a semantic relevance axiom selection system. This paper describes the design, implementation, and testing ... system for selecting necessary axioms from a large set also containing superfluous axioms, to obtain ... selection is determined by semantics of the axioms and conjecture, ordered heuristically by a syntactic...
  • MTT

  • Referenced in 21 articles [sw09783]
  • strategies for controlling the execution, matching modulo axioms, and so on, that are used...
  • MaLeCoP

  • Referenced in 20 articles [sw07197]
  • system. While in MaLA Rea learning-based axiom selection is done outside unmodified theorem provers...
  • UniMath

  • Referenced in 13 articles [sw15140]
  • classical mathematics by adding the excluded middle axiom for types of h-level ... axiom of choice for types of h-level 2. UniMath is a growing library...