script.kps 767 Bytes
Newer Older
Sarah Grebing's avatar
Sarah Grebing committed
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
script agascript() {
impRight;
andLeft;
notLeft;

andLeft;
andLeft;
andLeft;
andLeft;
andLeft;
andLeft;
andLeft;
andLeft;
andLeft;
andLeft;
andLeft;

exLeft;
andLeft;
eqSymm formula = `agatha = butler`;
nnf_imp2or on= `hates(agatha, w6) -> hates(butler, w6)`; 
 
//nnf_imp2or; -> wirft hier ScriptCommandNotApplicableException 
//wirft ansonsten immer java.lang.RuntimeException: de.uka.ilkd.key.macros.scripts.meta.ConversionException: Could not convert value hates(agatha, w6) -> hates(butler, w6) to type interface de.uka.ilkd.key.logic.Term
	at 
//nnf_imp2or formula= `hates(agatha, w6) -> hates(butler, w6)`;
//nnf_imp2or on = `hates(agatha, w6) -> hates(butler, w6)` formula=` \forall S w6; (hates(agatha, w6) -> hates(butler, w6))`;
}