
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 userdefined 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 builtin compiler. Axiom has been in development since...

KLONE
 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...

CCPi
 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 learningbased 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 hlevel ... axiom of choice for types of hlevel 2. UniMath is a growing library...