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 |

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