TestProp2CNF.hs revision 926b3c5491f1c608f5b79e2d8014d7a1385558c3
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
{- |
Module : $Header$
Description : Instance of class Logic for propositional logic
Copyright : (c) Dominik Luecke, Uni Bremen 2007
License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
Maintainer : luecke@tzi.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
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 = simpleIdToId $ mkSimpleId "a"
bId :: Id
bId = simpleIdToId $ mkSimpleId "b"
cId :: Id
cId = simpleIdToId $ mkSimpleId "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 = [SenAttr
{
senAttr = "myForm"
, isAxiom = True
, isDef = False
, wasTheorem = False
, sentence = myForm
}
]
myForms = [SenAttr
{
senAttr = "myForm"
, isAxiom = True
, isDef = False
, wasTheorem = False
, sentence = myForm
}
,SenAttr
{
senAttr = "myOtherForm"
, isAxiom = True
, isDef = False
, wasTheorem = False
, sentence = myOtherForm
}
]
runAll = show $ translateToCNF (mySig, myEmptyForm)
showStuff = PC.ioDIMACSProblem "Problem " mySig myForms []
showProof = PC.goalDIMACSProblem "DIMACSProblem" (propProverState mySig myForms)
SenAttr
{
senAttr = "myOtherForm"
, isAxiom = True
, isDef = False
, wasTheorem = False
, sentence = myOtherForm
}
[]