| Copyright | (c) Till Mossakowski, Rainer Grabbe and Uni Bremen 2002-2006 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | till@informatik.uni-bremen.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
CASL.Induction
Description
We provide both second-order induction schemes as well as their instantiation to specific first-order formulas.
- inductionScheme :: FormExtension f => [Constraint] -> FORMULA f
- generateInductionLemmas :: FormExtension f => Bool -> (Sign f e, [Named (FORMULA f)]) -> (Sign f e, [Named (FORMULA f)])
Documentation
inductionScheme :: FormExtension f => [Constraint] -> FORMULA f
derive a second-order induction scheme from a sort generation constraint the second-order predicate variables are represented as predicate symbols P[s], where s is a sort
generateInductionLemmas :: FormExtension f => Bool -> (Sign f e, [Named (FORMULA f)]) -> (Sign f e, [Named (FORMULA f)])
for goals try to generate additional implications based on induction