
HIP
 Referenced in 29 articles
[sw09786]
 programs. The specification language allows user defined inductive predicates used to model complex data structures ... each method/loop, HIP will construct a set of separation logic proof obligations in the form...

SCC
 Referenced in 11 articles
[sw09809]
 subsorts and with domains of functions defined by conditional memberships. Our tool consists ... set of proof obligations which if discharged, ensures sufficient completeness; and (ii) Maude’s inductive...

FinFuns
 Referenced in 5 articles
[sw28536]
 Isabelle/HOL and present how to safely set up Isabelle’s code generator such that operations ... recursion combinator and an induction rule for FinFuns allow for defining and reasoning about operators ... approach to an executable formalisation of sets and use it for the semantics...

Equations
 Referenced in 6 articles
[sw28614]
 definitions made by pattern matching on inductive families in the Coq system. It allows ... structured, recursive dependentlytyped functions as a set of equations, automatically find their realization ... them. It provides a complete package to define and reason on functions in the proof...

CoqMTU
 Referenced in 3 articles
[sw19138]
 complex type theory, a Calculus of Inductive Constructions with a predicative hierarchy of universes ... specified abstractly, by a set of constructors, a set of defined symbols, axioms expressing that...

Louise
 Referenced in 1 article
[sw41513]
 setting for Inductive Logic Programming (ILP) (Muggleton, 1991). ILP is the branch of machine learning ... language bias is defined by a set of second order logic clauses called metarules. Examples...

MAMBO
 Referenced in 1 article
[sw07685]
 modern engineering student, namely: an inductive approach to learning, whereby general patterns are discerned from ... MAMBO toolbox, is based on a set of procedures written in the MAPLE programming language ... projects for which MAMBO is useful to define the specific geometry of the mechanism...

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

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

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

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

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

Magma
 Referenced in 3296 articles
[sw00540]
 Computer algebra system (CAS). Magma is a large...

Maple
 Referenced in 5363 articles
[sw00545]
 The result of over 30 years of cutting...

Mathematica
 Referenced in 6337 articles
[sw00554]
 Almost any workflow involves computing results, and that...

Matlab
 Referenced in 13460 articles
[sw00558]
 MATLAB® is a highlevel language and interactive...

MiniSat
 Referenced in 565 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...

SageMath
 Referenced in 1970 articles
[sw00825]
 Sage (SageMath) is free, opensource math software...

SINGULAR
 Referenced in 1504 articles
[sw00866]
 SINGULAR is a Computer Algebra system (CAS) for...

MACSYMA
 Referenced in 720 articles
[sw01209]
 Macsyma is a general purpose symbolicnumericalgraphical...