d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Description : Implementation of logic instance Mon
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Copyright : (c) Daniel Hausmann & Georgel Calin & Lutz Schroeder, DFKI Lab Bremen,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder - Rob Myers & Dirk Pattinson, Department of Computing, ICL
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu - License : GPLv2 or higher, see LICENSE.txt
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Maintainer : hausmann@dfki.de
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Stability : provisional
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Portability : portable
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Provides the implementation of the matching functions monotonic modal logic.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ------------------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance of feature for Monotonic logic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder------------------------------------------------------------------------------ -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata Mon a = Mon [Formula a] deriving (Eq, Show)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- For any combination of a positive and a negative literal, there is a premise
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedercontaining only one sequent. This sequent contains only one formula over the
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederstripped positive literal and the negated stripped negative literal.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedere.g. seq = [ (M Mon p), !(M Mon q), (M Mon !p), !(M Mon !r)]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedermatch seq = [ [[ p, !q]], [[p, r]], [[ !p, !q]], [[ !p, r]] ] -}
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmanninstance (SigFeature b c d, Eq (b (c d)), Eq (c d)) => NonEmptyFeature Mon b c d where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nefMatch flags seq =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let stripnlits = [ Neg (head phi) | Neg (Mod (Mon phi)) <- seq]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder striplits = [ head phi | Mod (Mon phi) <- seq]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in [ [[Sequent [Neg (And (Neg neg) (Neg pos))]]] |
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder neg <- stripnlits, pos <- striplits]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefPretty d = genfPretty d "[Mon]"
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefFeatureFromSignature sig = Mon
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefFeatureFromFormula phi = Mon
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefStripFeature (Mon phis) = phis
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ------------------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance of sigFeature for Monotonic logic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder------------------------------------------------------------------------------ -}
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmanninstance (SigFeature b c d, Eq (c d), Eq (b (c d))) => NonEmptySigFeature Mon b c d where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder neGoOn = genericPGoOn