
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 sideeffect...

CVC
 Referenced in 48 articles
[sw09462]
 Subsidiary decision procedures for theories of arrays, inductive datatypes, and linear real arithmetic are currently ... highperformance 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...

MyhillNerode
 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 ifthen rules in a meningitis ... dataset. GDTRS 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 nonwellfounded 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 domainspecific reasoning tools. Plastic is implemented in the higherorder...

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

DLlearner
 Referenced in 7 articles
[sw14439]
 Inductive Logic Programming. DLLearner 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 nonmonotonic (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...