
SQEMA
 Referenced in 40 articles
[sw03056]
 Algorithmic correspondence and completeness in modal logic. IV. Semantic extensions of SQEMA ... introduced the algorithm SQEMA for computing firstorder equivalents and proving canonicity of modal formulae ... thus established a very general correspondence and canonical completeness result. SQEMA is based on transformation...

SLEP
 Referenced in 42 articles
[sw13487]
 smooth convex optimization via the firstorder blackbox methods. 3) Efficient Projection. The projection ... functions that efficiently compute the pathwise solutions corresponding to a series of regularization parameters...

Pyhybridanalysis
 Referenced in 3 articles
[sw14549]
 step, the algorithm builds the firstorder formula corresponding to the evolution of the automaton ... states that are reached for the first time in the last step is empty ... Tarski’s theory (i.e., is a firstorder formula involving polynomials), the sphere semantics ... Tarski’s theory and the corresponding formulae can be obtained from itself by applying...

LPTP
 Referenced in 7 articles
[sw01822]
 This is a firstorder theory that contains induction principles corresponding to the definition...

MATLANG
 Referenced in 5 articles
[sw39112]
 corresponds to equivalence by means of sentences in the threevariable fragment of firstorder ... smaller MATLANG fragment is shown to correspond to equivalence by means of sentences...

GEOTHER 1.1
 Referenced in 32 articles
[sw02842]
 lists or sets of predicates that correspond to the geometric hypotheses and the conclusion ... that is needed in order to manipulate and prove the theorem. From the specification, GEOTHER ... English or Chinese statement, into a firstorder logical formula, or into algebraic expressions; draw...

IsaFoR
 Referenced in 6 articles
[sw10106]
 proofs for recursive functions in (a firstorder subset of) Isabelle/HOL by encoding them ... Isabelle/HOL to the termination of the corresponding term rewrite system. We automate this reduction...

na8
 Referenced in 5 articles
[sw11513]
 formulation of the firstorder necessary conditions of optimality in terms of interpolation constraints ... this algorithm are illustrated and the corresponding program is implemented using MATLAB functions.par The claim...

Algorithm 982
 Referenced in 2 articles
[sw22551]
 solutions of homogeneous triangular systems of firstorder linear initialvalue ordinary differential equations with ... multiple zero eigenvalues provided the entire column corresponding to a zero eigenvalue is zero...

TSAT++
 Referenced in 3 articles
[sw21350]
 literals, where T is a firstorder theory for which a satisfiability procedure ... theoryspecific satisfiability checker cooperate in order to solve SMT. Modularity allows both different enumerators ... modules used (and of the corresponding theory). Some experimental results are presented, showing that TSAT...

LINUS
 Referenced in 1 article
[sw03010]
 successful propositional learners in a firstorder framework. As various propositional learners can be integrated ... modes. Running in CLASS mode, it corresponds to an enhanced attributevalue learner. In RELATION...

Boolector
 Referenced in 32 articles
[sw00085]
 Boolector: an efficient SMT solver for bitvectors...

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

gmp
 Referenced in 289 articles
[sw00363]
 GMP is a free library for arbitrary precision...

JMP
 Referenced in 58 articles
[sw00476]
 For more than 20 years, JMP statistical discovery...

Macaulay2
 Referenced in 1958 articles
[sw00537]
 Macaulay2 is a software system devoted to supporting...

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

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

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

Octave
 Referenced in 312 articles
[sw00646]
 GNU Octave is a highlevel language, primarily...