
XSummer
 Referenced in 30 articles
[sw06109]
 evaluation of higherorder perturbative corrections in quantum field theory. Of particular interest have been ... sums, where the harmonic sums and their generalizations appear as building blocks, originating for example...

LEGO
 Referenced in 107 articles
[sw09685]
 Constructions (CC), the Generalized Calculus of Constructions (GCC) and the Unified Theory of Dependent Types ... that of informal mathematics. The higherorder power of its underlying type theories...

ETPS
 Referenced in 160 articles
[sw06302]
 various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive ... prove theorems of first and higherorder logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higherorder logic. It has a formula editor which ... Mellon for a number of years. Students generally learn to use ETPS fairly quickly just...

Bedwyr
 Referenced in 22 articles
[sw09460]
 Checking over Syntactic Expressions. Bedwyr is a generalization of logic programming that allows model checking ... implementation of two recent advances in the theory of proof search. The first is centered ... operational semantics. The second is that higherorder abstract syntax is directly supported using term...

Plastic
 Referenced in 18 articles
[sw07403]
 framework type theory, in which other type theories may be defined (Luo, 1994). Extensions include ... tools. Plastic is implemented in the higherorder nonstrict functional language Haskell, and uses ... courtesy of David Aspinall’s generic Proof General. Speedwise, it compares favourably with similar...

BMIRT ToolKit
 Referenced in 5 articles
[sw13942]
 multidimensional, multigroup item response theory model frame work; exploratory and confirmatory mode are supported ... logistic model, generalized twoparameter partialcredit model, graded response model, higherorder model, testlet...

SPEEDUP
 Referenced in 2 articles
[sw21743]
 exact continuum values. Symbolic derivation of higherorder effective actions is implemented in SPEEDUP Mathematica ... approach. In addition to the general 1D quantum theory, developed Mathematica codes are capable...

REL4D
 Referenced in 1 article
[sw24378]
 computational aspects of relativistic electronic structure theories that are efficient enough to make calculations ... efficient computational schemes that take advantage of generally contracted spherical harmonic Gaussiantype spinors (GTSs ... framework, two relativistic Hamiltonians, RESC and higherorder DouglasKroll (DK), are introduced and illustrative...

NuprlLight
 Referenced in 1 article
[sw31982]
 NuprlLight: an implementation framework for higherorder logics. this paper we describe NuprlLight ... type theories and mathematical domains. The framework itself assumes (and provides) no type theory ... such as LF, Nuprl, set theory, and other theories can be defined and developed. Since ... generic theorem prover, NuprlLight uses generalized Horn clauses for logical specification. Indeed, specifications...

ADOLC
 Referenced in 249 articles
[sw00019]
 ADOLC: Automatic Differentiation of C/C++. We present...

ANSYS
 Referenced in 703 articles
[sw00044]
 ANSYS offers a comprehensive software suite that spans...

ACL2
 Referenced in 283 articles
[sw00060]
 ACL2 is both a programming language in which...

Coq
 Referenced in 1880 articles
[sw00161]
 Coq is a formal proof management system. It...

Expokit
 Referenced in 198 articles
[sw00258]
 Expokit provides a set of routines aimed at...

GAP
 Referenced in 3154 articles
[sw00320]
 GAP is a system for computational discrete algebra...

Gmsh
 Referenced in 720 articles
[sw00366]
 Gmsh is a 3D finite element grid generator...

Isabelle
 Referenced in 698 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

ISOGAT
 Referenced in 310 articles
[sw00457]
 A tutorial 2D MATLAB code for solving elliptic...

Isolde
 Referenced in 29 articles
[sw00458]
 ISOLDE, a Maple package for systems of linear...

LAPACK
 Referenced in 1695 articles
[sw00503]
 LAPACK is written in Fortran 90 and provides...