script.kps 1.03 KB
Newer Older
Alexander Weigl's avatar
Alexander Weigl committed
1
script SolveAgathaRiddle_1() {
Alexander Weigl's avatar
Alexander Weigl committed
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
    impRight;
    andLeft;
    notLeft;

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

    exLeft;
    andLeft;
    eqSymm formula = `agatha = butler`;
Alexander Weigl's avatar
Alexander Weigl committed
21
    auto;
Alexander Weigl's avatar
Alexander Weigl committed
22
23
24
25
26
27
28
29
30

    //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))`;
}

Alexander Weigl's avatar
Alexander Weigl committed
31
script SolveAgathaRiddle_2() {
Alexander Weigl's avatar
Alexander Weigl committed
32
33
34
35
36
37
38
    impRight;
    andLeft;
    notLeft;
    repeat { andLeft; }
    exLeft;
    andLeft;
    eqSymm formula = `agatha = butler`;
Alexander Weigl's avatar
Alexander Weigl committed
39
    auto;
Sarah Grebing's avatar
Sarah Grebing committed
40
}