
miniKanren
 Referenced in 6 articles
[sw20082]
 Constraint Logic Programming, probabilistic logic programming, nominal logic programming, and tabling...

aleanTAP
 Referenced in 2 articles
[sw09987]
 prove ground theorems in firstorder classical logic. Since it is declarative, αleanTAP generates theorems ... leanTAP into αKanren, an embedding of nominal logic programming in Scheme. We then show ... combination of tagging and nominal unification to eliminate the impure operators inherited from leanTAP, resulting...

FAME
 Referenced in 3 articles
[sw26270]
 extension of the basic description logic ALC with nominals, inverse roles and role inclusions. Fame...

Konclude
 Referenced in 13 articles
[sw12474]
 language is formally characterised by the Description Logic (DL) SROIQV(D). In other words, Konclude ... almost all datatypes. In addition, Konclude supports nominal schemas which allow for expressing arbitrary...

Herod
 Referenced in 3 articles
[sw09445]
 work presents two provers for basic hybrid logic HL(@), which have been implemented with ... point of view, the different treatment of nominal equalities of the two calculi...

Pilate
 Referenced in 3 articles
[sw09446]
 work presents two provers for basic hybrid logic HL(@), which have been implemented with ... point of view, the different treatment of nominal equalities of the two calculi...

Robinson arithmetic
 Referenced in 2 articles
[sw42008]
 Robinson Arithmetic: We instantiate our syntaxindependent logic infrastructure developed in a separate AFP entry ... latter was formalised using Nominal Isabelle by adapting Larry Paulson’s formalization of the Hereditarily...

Shuhai
 Referenced in 1 article
[sw42914]
 this article, we bridge the gap between nominal specifications and actual performance by characterizing ... noisier systems due to their complex control logic and cache hierarchy. Since the memory itself...

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

HYBRID
 Referenced in 19 articles
[sw00421]
 Hybrid: a package for higherorder syntax in...

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

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

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

Nitpick
 Referenced in 64 articles
[sw00622]
 Nitpick is a counterexample generator for Isabelle/HOL that...

Ott
 Referenced in 32 articles
[sw00663]
 Semantic definitions of fullscale programming languages are...

R
 Referenced in 10253 articles
[sw00771]
 R is a language and environment for statistical...

TPS
 Referenced in 75 articles
[sw00973]
 TPS and ETPS are, respectively, the Theorem Proving...

SCIP
 Referenced in 558 articles
[sw01091]
 SCIP is currently one of the fastest non...

ML
 Referenced in 524 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...