• Nominal Isabelle

  • Referenced in 74 articles [sw12055]
  • automatically the reasoning infrastructure for α-equated terms. We also prove strong induction principles that...
  • evt

  • Referenced in 8 articles [sw09805]
  • successful proofs such as inductive and compositional reasoning, and an efficient treatment of side-effect...
  • CVC

  • Referenced in 48 articles [sw09462]
  • Subsidiary decision procedures for theories of arrays, inductive datatypes, and linear real arithmetic are currently ... high-performance Chaff solver for propositional reasoning, and the ability to produce independently checkable proofs...
  • KIV

  • Referenced in 53 articles [sw10060]
  • definition of dynamic logic, for reasoning about the correctness of software systems. Several other object ... this pursose, KIV was integrated with an induction theorem prover and a case tool...
  • Myhill-Nerode

  • Referenced in 11 articles [sw28547]
  • straightforward to formalise in theorem provers. The reason is that natural representations for automata ... inductive datatypes. Regular expressions can be defined straightforwardly as a datatype and a corresponding reasoning...
  • Aligators

  • Referenced in 1 article [sw09779]
  • algebraic techniques to carry out inductive reasoning over array content. The Aligators’ loop extraction module...
  • RSBR_

  • Referenced in 19 articles [sw02934]
  • Rough Sets with Boolean Reasoning (RSBR) respectively, for mining if-then rules in a meningitis ... dataset. GDT-RS is a soft hybrid induction system, and RSBR is used for discretization...
  • EXPANDER

  • Referenced in 6 articles [sw22715]
  • EXPANDER: Inductive Expansion in SML. EXPANDER is a proof support system for reasoning about data...
  • IsaPlanner

  • Referenced in 30 articles [sw02047]
  • prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture ... proof technique written in IsaPlanner is an inductive theorem prover based on Rippling. This...
  • CoCLAM

  • Referenced in 2 articles [sw28719]
  • dual of induction. It allows reasoning about non-well-founded structures such as lazy lists...
  • FinFuns

  • Referenced in 5 articles [sw28536]
  • combinator and an induction rule for FinFuns allow for defining and reasoning about operators...
  • Plastic

  • Referenced in 18 articles [sw07403]
  • defined (Luo, 1994). Extensions include Inductive Types, Universes, and Coercive Subtyping. It may be regarded ... platform for implementing domain-specific reasoning tools. Plastic is implemented in the higher-order...
  • SCC

  • Referenced in 11 articles [sw09809]
  • completeness tool, which explicitly supports sufficient completeness reasoning for partial conditional specifications having sorts ... ensures sufficient completeness; and (ii) Maude’s inductive theorem prover (ITP) that is used...
  • DL-learner

  • Referenced in 7 articles [sw14439]
  • Inductive Logic Programming. DL-Learner includes several learning algorithms, support for different OWL formats, reasoner...
  • KReator

  • Referenced in 3 articles [sw06946]
  • relational reasoning This article presents KReator, a versatile integrated development environment for probabilistic inductive logic ... currently under development. The area of probabilistic inductive logic programming (or statistical relational learning) aims ... common and simple interface for representing, reasoning and learning with different relational probabilistic approaches ... various frameworks within the area of probabilistic inductive logic programming and statistical relational learning. Currently...
  • PrASP

  • Referenced in 3 articles [sw18512]
  • programming”). PrASP is both an uncertainty reasoning and machine learning software and a probabilistic logic ... research software platform for non-monotonic (inductive) probabilistic logic programming, our framework mainly targets applications ... area of uncertainty stream reasoning. PrASP programs can consist of ASP (AnsProlog) as well...
  • ACE

  • Referenced in 9 articles [sw22675]
  • Complexity Evaluator) system is able to analyze reasonably large programs, like sorting programs ... nonrecursive equivalent according to MacCarthy’s recursion induction principle, using a predefined library of recursive...
  • Equations

  • Referenced in 6 articles [sw28614]
  • definitions made by pattern matching on inductive families in the Coq system. It allows ... type theory and generate proofs to ease reasoning on them. It provides a complete package...
  • Kami

  • Referenced in 4 articles [sw28644]
  • verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper ... library that enables similar expressive and modular reasoning for hardware designs expressed in the style...
  • UALib

  • Referenced in 1 article [sw36875]
  • power of inductive and dependent types for representing and reasoning about algebraic and relational structures...