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)])
- 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

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