script.kps 769 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
script agascript() {
impRight;
andLeft;
notLeft;

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

exLeft;
andLeft;
eqSymm formula = `agatha = butler`;
Sarah Grebing's avatar
Sarah Grebing committed
21
//nnf_imp2or on= `hates(agatha, w6) -> hates(butler, w6)`;
Sarah Grebing's avatar
Sarah Grebing committed
22 23 24
 
//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
Sarah Grebing's avatar
Sarah Grebing committed
25
//	at
Sarah Grebing's avatar
Sarah Grebing committed
26 27 28
//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))`;
}