• LEGO

  • Referenced in 107 articles [sw09685]
  • formalization closer to that of informal mathematics. The higher-order power of its underlying type ... specifying new inductive types, provide an expressive language for formalization of mathematical problems and program...
  • ISETL

  • Referenced in 20 articles [sw01370]
  • strategy in abstract algebra, calculus, and mathematical induction...
  • MPTP 0.2

  • Referenced in 50 articles [sw02589]
  • make the large formal Mizar Mathematical Library (MML) available to current first-order automated theorem ... even a simple inductive or deductive system trained on formal mathematics can be sometimes smarter...
  • Agda

  • Referenced in 207 articles [sw09689]
  • dependently typed functional programming language: It has inductive families, which are similar to Haskell ... type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin...
  • Isabelle/ZF

  • Referenced in 63 articles [sw04973]
  • main application is the formalization of mathematical proofs and in particular formal verification, which includes ... formalizing computational notions. It supports inductive definitions of infinite-branching trees for any cardinality...
  • Fasthenry

  • Referenced in 18 articles [sw08927]
  • compute the 3-D frequency dependent inductances and resistances in nearly order n time ... number of volume-filaments. The mathematical formulation and numerical solution are discussed, including two types...
  • LPL software

  • Referenced in 19 articles [sw04860]
  • proof techniques, quantifiers, basic set theory, and induction. Advanced chapters include proofs of soundness ... from first logic courses for undergraduates (philosophy, mathematics, and computer science) to a first graduate...
  • RoughSets

  • Referenced in 8 articles [sw31808]
  • functionality: discretization, feature selection, instance selection, rule induction and classification based on nearest neighbors ... Zdzisław Pawlak in 1982 as a sophisticated mathematical tool to model and process imprecise...
  • Coccinelle

  • Referenced in 3 articles [sw29246]
  • very simple inductive definition (with only 2 constructors), the adequacy with the mathematical definition...
  • Gallina

  • Referenced in 6 articles [sw27568]
  • specification language of Coq. It allows developing mathematical theories and to prove specifications of programs ... algorithm are described in Chapter Calculus of Inductive Constructions...
  • Volpano Smith

  • Referenced in 1 article [sw29543]
  • then proceeds by rule induction on the operational semantics. The mathematically most intricate part...
  • 3D-MLSI

  • Referenced in 1 article [sw08122]
  • software package 3D-MLSI was developed for inductance calculation in multilayer superconducting integrated circuits ... advantages of 3D-MLSI are: a new mathematical model that takes into account ... most applicable when both kinetic and magnetic inductances are important. A method of equivalent circuits...
  • gamet

  • Referenced in 0 articles [sw37609]
  • defined as the study of mathematical models of conflict and cooperation between intelligent and rational ... extensive form game through backward induction...
  • MAMBO

  • Referenced in 1 article [sw07685]
  • arbitrary multibody mechanism; formulate a mathematical description of a general motion of this mechanism ... modern engineering student, namely: an inductive approach to learning, whereby general patterns are discerned from ... MAMBO allows the students to check the mathematical analysis and to visualize the results...
  • ANSYS

  • Referenced in 704 articles [sw00044]
  • ANSYS offers a comprehensive software suite that spans...
  • ACL2

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

  • Referenced in 654 articles [sw00143]
  • CoCoA is a system for Computations in Commutative...
  • Coq

  • Referenced in 1890 articles [sw00161]
  • Coq is a formal proof management system. It...
  • CViz

  • Referenced in 3 articles [sw00178]
  • CViz is a visualization tool designed for analyzing...
  • Dafny

  • Referenced in 73 articles [sw00183]
  • Dafny is an imperative object-based language with...