TestProp2CNF.hs revision 926b3c5491f1c608f5b79e2d8014d7a1385558c3
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
ce5989998d7dc680ac7d1494ac26a6aadd0735d5Felix Gabriel ManceDescription : Instance of class Logic for propositional logic
29454fc45be6d7e3caec75e08a933cdf77db3453Felix Gabriel ManceCopyright : (c) Dominik Luecke, Uni Bremen 2007
29454fc45be6d7e3caec75e08a933cdf77db3453Felix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
29454fc45be6d7e3caec75e08a933cdf77db3453Felix Gabriel ManceMaintainer : luecke@tzi.de
29454fc45be6d7e3caec75e08a933cdf77db3453Felix Gabriel ManceStability : experimental
29454fc45be6d7e3caec75e08a933cdf77db3453Felix Gabriel MancePortability : non-portable (imports Logic.Logic)
29454fc45be6d7e3caec75e08a933cdf77db3453Felix Gabriel ManceTest cases for Prop2CNF
29454fc45be6d7e3caec75e08a933cdf77db3453Felix Gabriel Mance http://en.wikipedia.org/wiki/Propositional_logic
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance What is a Logic?.
fc05327b875b5723b6c17849b83477f29ec12c90Felix Gabriel Mance In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
29454fc45be6d7e3caec75e08a933cdf77db3453Felix Gabriel Manceimport qualified SoftFOL.ProverState as PState
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport qualified Propositional.Conversions as PC
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian Maederimport qualified SoftFOL.Sign as SPS
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai CodescuaId = simpleIdToId $ mkSimpleId "a"
7852de3551fc797566ee71165bafe05b6d81728cnotanartistbId = simpleIdToId $ mkSimpleId "b"
80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskicId = simpleIdToId $ mkSimpleId "c"
30a43dc06f8b3127d84f76843e27772facb2e2aaFelix Gabriel MancemySig = addToSig (addToSig (addToSig emptySig aId) bId) cId
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian MaedermyForm :: FORMULA
f8ebf49601fc282a2c044f9f37ed80340b187314Felix Gabriel MancemyForm = (Disjunction [(Predication (mkSimpleId "a")),
34782d04d5818cd2e91ae11ee16d1f40c1403111Felix Gabriel Mance Negation (Predication (mkSimpleId "a")) nullRange]
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel MancemyOtherForm :: FORMULA
2cbb342fb7737cb25ee4494fc4d4e8f899b3f3a9Christian MaedermyOtherForm = Conjunction [(Equivalence (Predication (mkSimpleId "a"))
34782d04d5818cd2e91ae11ee16d1f40c1403111Felix Gabriel Mance (Predication (mkSimpleId "c"))
7852de3551fc797566ee71165bafe05b6d81728cnotanartistmyForm :: FORMULA
7852de3551fc797566ee71165bafe05b6d81728cnotanartistmyForm = (Predication (mkSimpleId "a"))
7852de3551fc797566ee71165bafe05b6d81728cnotanartistmyEmptyForm = [SenAttr
5ddbc7bb1d91485baec25291cfa4a90a1c5f0830Felix Gabriel Mance senAttr = "myForm"
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance , isAxiom = True
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance , isDef = False
7852de3551fc797566ee71165bafe05b6d81728cnotanartist , wasTheorem = False
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance , sentence = myForm
3e05436e2df004f421c72c2003883972aaa1ebc3mcodescumyForms = [SenAttr
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel Mance senAttr = "myForm"
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel Mance , isAxiom = True
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance , isDef = False
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance , wasTheorem = False
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel Mance , sentence = myForm
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance senAttr = "myOtherForm"
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance , isAxiom = True
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance , isDef = False
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance , wasTheorem = False
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance , sentence = myOtherForm
6e8e773cee72274a065907b397bedf71eb4936c4mcodescurunAll = show $ translateToCNF (mySig, myEmptyForm)
6e8e773cee72274a065907b397bedf71eb4936c4mcodescushowStuff = PC.ioDIMACSProblem "Problem " mySig myForms []
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel ManceshowProof = PC.goalDIMACSProblem "DIMACSProblem" (propProverState mySig myForms)
a08878ef4de7c156dabaa25714372e07b2f3e151mcodescu senAttr = "myOtherForm"
30a43dc06f8b3127d84f76843e27772facb2e2aaFelix Gabriel Mance , isAxiom = True
30a43dc06f8b3127d84f76843e27772facb2e2aaFelix Gabriel Mance , isDef = False
f008d37d7fd3b2394a717ac3561f5f1982bb0b28Felix Gabriel Mance , wasTheorem = False
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , sentence = myOtherForm