• Isabelle/ZF

  • Referenced in 62 articles [sw04973]
  • formalizing computational notions. It supports inductive definitions of infinite-branching trees for any cardinality...
  • Slide

  • Referenced in 19 articles [sw28542]
  • SLIDE - Separation Logic with Inductive Definitions. Automata-based entailment checking for Separation Logic with Inductive ... Definitions. SLIDE is a prototype tool for checking entailment ... Separation Logic with user-provided inductive definitions of recursive data structures (lists, trees, and beyond...
  • Nominal Isabelle

  • Referenced in 72 articles [sw12055]
  • lambda-abstractions. Our extension includes new definitions of α-equivalence and establishes automatically the reasoning ... equated terms. We also prove strong induction principles that have the usual variable convention already...
  • Tac

  • Referenced in 7 articles [sw09455]
  • order logic with inductive and co-inductive definitions in which the introduction rules are partitioned ... capable of automatically proving many theorems using induction and coinduction. Since the automatic proof procedure...
  • IDP3

  • Referenced in 7 articles [sw22941]
  • first-order logic enriched with types, inductive definitions, aggregates and partial functions. It offers...
  • IDP

  • Referenced in 5 articles [sw23254]
  • order logic (FO) with types, aggregates, inductive definitions, bounded arithmetic, partial functions, etc. More information...
  • Coccinelle

  • Referenced in 3 articles [sw29246]
  • approach are a very simple inductive definition (with only 2 constructors), the adequacy with...
  • LPTP

  • Referenced in 7 articles [sw01822]
  • order theory that contains induction principles corresponding to the definition of the predicates ... appropriate axioms for built-in predicates. The inductive extension allows to express modes and types...
  • KIV

  • Referenced in 51 articles [sw10060]
  • logic. The main applications rely on a definition of dynamic logic, for reasoning about ... this pursose, KIV was integrated with an induction theorem prover and a case tool...
  • Template-Coq

  • Referenced in 3 articles [sw27569]
  • kernel’s declaration structures for definitions and inductives, and implement a monad for general manipulation...
  • Polyp

  • Referenced in 33 articles [sw09131]
  • function that is defined by induction on the structure of user-defined datatypes. This paper ... polytypic functions. The extended language type checks definitions of polytypic functions, and infers the types...
  • ACE

  • Referenced in 9 articles [sw22675]
  • MacCarthy’s recursion induction principle, using a predefined library of recursive definitions. As the complexity...
  • GidL

  • Referenced in 1 article [sw23255]
  • logic with several constructs such as inductive definitions, aggregates and arithmetic. We describe the input...
  • POSIX Lexing

  • Referenced in 1 article [sw28598]
  • this entry we give our inductive definition of what a POSIX value is and show...
  • Equations

  • Referenced in 6 articles [sw28614]
  • present a compiler for definitions made by pattern matching on inductive families...
  • MODL

  • Referenced in 10 articles [sw18797]
  • speed, accuracy and understandability of the induction models. In this paper, we propose ... this model space. This results in the definition of a Bayes optimal evaluation criterion ... real and synthetic data demonstrate the high inductive performances obtained by the new discretization method...
  • SKIL

  • Referenced in 2 articles [sw25433]
  • denoted AF2 which includes induction through the data type definitions [{it J.-L. Krivine...
  • LISA

  • Referenced in 1 article [sw33631]
  • definition, analysis and resolution of Markovian processes: Symbolic and inductive techniques. This paper presents...
  • Gallina

  • Referenced in 6 articles [sw27568]
  • from axioms, hypotheses, parameters, lemmas, theorems and definitions of constants, functions, predicates and sets ... algorithm are described in Chapter Calculus of Inductive Constructions...
  • Hereditarily Finite Sets

  • Referenced in 6 articles [sw29249]
  • other HF sets; they enjoy an induction principle and satisfy all the axioms ... using infinite sets are possible here. The definition of addition for the HF sets follows...