| 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.
Synopsis
- inductionScheme :: FormExtension f => [Constraint] -> FORMULA f
- inductionSentence :: FormExtension f => [Constraint] -> FORMULA f
- generateInductionLemmas :: FormExtension f => Bool -> (Sign f e, [Named (FORMULA f)]) -> (Sign f e, [Named (FORMULA f)])
- substitute :: FormExtension f => VAR -> SORT -> TERM f -> FORMULA f -> FORMULA f
Documentation
inductionScheme :: FormExtension f => [Constraint] -> FORMULA f Source #
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
inductionSentence :: FormExtension f => [Constraint] -> FORMULA f Source #
generateInductionLemmas :: FormExtension f => Bool -> (Sign f e, [Named (FORMULA f)]) -> (Sign f e, [Named (FORMULA f)]) Source #
for goals try to generate additional implications based on induction
substitute :: FormExtension f => VAR -> SORT -> TERM f -> FORMULA f -> FORMULA f Source #
substitute a term for a variable in a formula