{- |
Module : ./Propositional/TestProp2CNF.hs
Description : Instance of class Logic for propositional logic
Copyright : (c) Dominik Luecke, Uni Bremen 2007
License : GPLv2 or higher, see LICENSE.txt
Maintainer : luecke@informatik.uni-bremen.de
Stability : experimental
Portability : non-portable (imports Logic.Logic)
Test cases for Prop2CNF
-}
{-
Ref.
Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
What is a Logic?.
In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
2005.
-}
module Propositional.TestProp2CNF
where
import Propositional.Prop2CNF -- FIXME: What happened to Prop2CNF?
import Propositional.Sign
import Common.Id
import Common.AS_Annotation
import qualified SoftFOL.ProverState as PState
import qualified Propositional.Conversions as PC
import Propositional.Prove
import Propositional.ProverState
import qualified SoftFOL.Sign as SPS
aId :: Id
aId = stringToId "a"
bId :: Id
bId = stringToId "b"
cId :: Id
cId = stringToId "c"
mySig :: Sign
mySig = addToSig (addToSig (addToSig emptySig aId) bId) cId
myForm :: FORMULA
myForm = Disjunction [Predication (mkSimpleId "a"),
Negation (Predication (mkSimpleId "a")) nullRange]
nullRange
myOtherForm :: FORMULA
myOtherForm = Conjunction [Equivalence (Predication (mkSimpleId "a"))
(Predication (mkSimpleId "c"))
nullRange] nullRange
{-
myForm :: FORMULA
myForm = (Predication (mkSimpleId "a"))
-}
myEmptyForm = makeNamed "myForm" myForm
otherForm = makeNamed "myOtherForm" myOtherForm
myForms = [myEmptyForm, otherForm]
runAll = translateToCNF (mySig, [myEmptyForm])
showStuff :: IO String
showStuff = PC.showDIMACSProblem "Problem " mySig myForms []
showProof = PC.goalDIMACSProblem "DIMACSProblem"
(propProverState mySig myForms [])
otherForm []