
Isabelle/ZF
 Referenced in 62 articles
[sw04973]
 formalizing computational notions. It supports inductive definitions of infinitebranching trees for any cardinality...

Slide
 Referenced in 19 articles
[sw28542]
 SLIDE  Separation Logic with Inductive Definitions. Automatabased entailment checking for Separation Logic with Inductive ... Definitions. SLIDE is a prototype tool for checking entailment ... Separation Logic with userprovided inductive definitions of recursive data structures (lists, trees, and beyond...

Nominal Isabelle
 Referenced in 72 articles
[sw12055]
 lambdaabstractions. 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 coinductive 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]
 firstorder 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 builtin 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...

TemplateCoq
 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 userdefined 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...