Hets - the Heterogeneous Tool Set

Copyright(c) Dominik Luecke, Uni Bremen 2007
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityexperimental
Portabilityportable
Safe HaskellNone

Propositional.Conservativity

Description

THe QBF solver sKizzo is used for conservativity checking. This is the code connecting it to Hets

Synopsis

Documentation

conserCheck

Arguments

:: (Sign, [Named FORMULA])

Initial sign and formulas

-> Morphism

morhpism between specs

-> [Named FORMULA]

Formulas of extended spec

-> IO (Result (Conservativity, [FORMULA])) 

Conservativity Check for Propositional Logic