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

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

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

VeriFast
 Referenced in 66 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...

Aleph
 Referenced in 55 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...

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

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

CIRC
 Referenced in 41 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...

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

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

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

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

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

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

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

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

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

Slide
 Referenced in 20 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...

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

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