
Agda
 Referenced in 190 articles
[sw09689]
 dependently typed functional programming language: It has inductive families, which are similar to Haskell...

LERS
 Referenced in 121 articles
[sw08637]
 paper presents the system LERS for rule induction. The system handles inconsistencies in the input...

LEGO
 Referenced in 107 articles
[sw09685]
 theories, and the support of specifying new inductive types, provide an expressive language for formalization...

VeriFast
 Referenced in 57 articles
[sw07705]
 manipulating imperative programs. The programmer may declare inductive datatypes and primitive recursive functions for specification ... through explicit ghost statements. Lemma functions enable inductive proofs of memory representation equivalences and facts...

Nominal Isabelle
 Referenced in 70 articles
[sw12055]
 equated terms. We also prove strong induction principles that have the usual variable convention already...

Aleph
 Referenced in 48 articles
[sw12108]
 Proposing Hypotheses (Aleph). Aleph is an Inductive Logic Programming (ILP) system. This manual ... Muggleton and L. De Raedt (1994), Inductive Logic Programming: Theory and Methods, Jnl. Logic Programming...

Dafny
 Referenced in 66 articles
[sw00183]
 sequential, supports generic classes, dynamic allocation, and inductive datatypes, and builds in specification constructs...

CIRC
 Referenced in 40 articles
[sw06202]
 principle generalizes both circular coinduction and structural induction and can be expressed in plain English ... variable, then it becomes a structural induction (on that variable) derivation rule. This way, Circ ... supports both coinduction and induction as projections of a more general principle...

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

Nitpick
 Referenced in 61 articles
[sw00622]
 model finder. Nitpick supports unbounded quantification, (co)inductive predicates and datatypes, and (co)recursive functions...

FOCI
 Referenced in 58 articles
[sw12868]
 discovering predicates in predicate abstraction, and computing inductive invariants...

GOLEM
 Referenced in 52 articles
[sw24695]
 rlggs in a covering approach. For the induction of a single clause, it randomly selects...

KIV
 Referenced in 51 articles
[sw10060]
 this pursose, KIV was integrated with an induction theorem prover and a case tool...

CVC
 Referenced in 47 articles
[sw09462]
 Subsidiary decision procedures for theories of arrays, inductive datatypes, and linear real arithmetic are currently...

MPTP 0.2
 Referenced in 45 articles
[sw02589]
 This situation suggests that even a simple inductive or deductive system trained on formal mathematics...

CoCasl
 Referenced in 26 articles
[sw13076]
 allows for modelling systems in terms of inductive datatypes as well as of coinductive...

Polyp
 Referenced in 31 articles
[sw09131]
 function that is defined by induction on the structure of userdefined datatypes. This paper...

FOIL
 Referenced in 31 articles
[sw24694]
 Induction of logic programs: FOIL and related systems. FOIL is a firstorder learning system...

Slide
 Referenced in 18 articles
[sw28542]
 SLIDE  Separation Logic with Inductive Definitions. Automatabased entailment checking for Separation Logic with Inductive ... entailment in Separation Logic with userprovided inductive definitions of recursive data structures (lists, trees...

IsaPlanner
 Referenced in 29 articles
[sw02047]
 proof technique written in IsaPlanner is an inductive theorem prover based on Rippling. This...