- Referenced in 29 articles
- 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...
- Referenced in 11 articles
- 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...
- Referenced in 5 articles
- 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...
- Referenced in 6 articles
- definitions made by pattern matching on inductive families in the Coq system. It allows ... structured, recursive dependently-typed 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...
- Referenced in 3 articles
- 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...
- Referenced in 1 article
- 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...
- Referenced in 1 article
- 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...
- Referenced in 703 articles
- ANSYS offers a comprehensive software suite that spans...
- Referenced in 654 articles
- CoCoA is a system for Computations in Commutative...
- Referenced in 1880 articles
- Coq is a formal proof management system. It...
- Referenced in 3154 articles
- GAP is a system for computational discrete algebra...
- Referenced in 698 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 3296 articles
- Computer algebra system (CAS). Magma is a large...
- Referenced in 5363 articles
- The result of over 30 years of cutting...
- Referenced in 6337 articles
- Almost any workflow involves computing results, and that...
- Referenced in 13460 articles
- MATLAB® is a high-level language and interactive...
- Referenced in 565 articles
- An extensible SAT-solver. MiniSat is a minimalistic...
- Referenced in 1970 articles
- Sage (SageMath) is free, open-source math software...
- Referenced in 1504 articles
- SINGULAR is a Computer Algebra system (CAS) for...
- Referenced in 720 articles
- Macsyma is a general purpose symbolic-numerical-graphical...