• 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 first-order 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 syntax-independent 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 higher-order 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 high-level 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 full-scale 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 general-purpose functional...