• XSummer

  • Referenced in 30 articles [sw06109]
  • evaluation of higher-order 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 higher-order 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 higher-order logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higher-order 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 higher-order 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 higher-order non-strict functional language Haskell, and uses ... courtesy of David Aspinall’s generic Proof General. Speed-wise, it compares favourably with similar...
  • BMIRT ToolKit

  • Referenced in 5 articles [sw13942]
  • multidimensional, multi-group item response theory model frame work; exploratory and confirmatory mode are supported ... logistic model, generalized two-parameter partial-credit model, graded response model, higher-order model, testlet...
  • SPEEDUP

  • Referenced in 2 articles [sw21743]
  • exact continuum values. Symbolic derivation of higher-order 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 Gaussian-type spinors (GTSs ... framework, two relativistic Hamiltonians, RESC and higher-order Douglas-Kroll (DK), are introduced and illustrative...
  • Nuprl-Light

  • Referenced in 1 article [sw31982]
  • Nuprl-Light: an implementation framework for higher-order logics. this paper we describe Nuprl-Light ... 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, Nuprl-Light uses generalized Horn clauses for logical specification. Indeed, specifications...
  • ADOL-C

  • Referenced in 249 articles [sw00019]
  • ADOL-C: 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...