• 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 infinite-branching 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 co-inductive...
  • Polyp

  • Referenced in 31 articles [sw09131]
  • function that is defined by induction on the structure of user-defined datatypes. This paper...
  • FOIL

  • Referenced in 31 articles [sw24694]
  • Induction of logic programs: FOIL and related systems. FOIL is a first-order learning system...
  • Slide

  • Referenced in 18 articles [sw28542]
  • SLIDE - Separation Logic with Inductive Definitions. Automata-based entailment checking for Separation Logic with Inductive ... entailment in Separation Logic with user-provided 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...