Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski Rainer Grabbe and Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CASL.Induction

Description

We provide both second-order induction schemes as well as their instantiation to specific first-order formulas.

Synopsis

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