Typing #done does not clean everything it's supposed to. Look at these two
session examples:
--- Loading LAX and checking the scope of a bang rule
:> #load ../examples/proofsystems/lax
Loading file ../examples/proofsystems/lax
?> #scopebang
Please type the subexponential:
cr
!cr :
The following will have their formulas erased:
The following should be empty:
r,
?> #done
:> #load ../examples/proofsystems/s4
Loading file ../examples/proofsystems/s4
?> rght(imp (nec a) (poss a)).
Typing #done does not clean everything it's supposed to. Look at these two session examples:
--- Loading LAX and checking the scope of a bang rule
:> #load ../examples/proofsystems/lax Loading file ../examples/proofsystems/lax ?> #scopebang Please type the subexponential: cr !cr : The following will have their formulas erased:
The following should be empty: r, ?> #done :> #load ../examples/proofsystems/s4 Loading file ../examples/proofsystems/s4 ?> rght(imp (nec a) (poss a)).
No. ?>
--- Loading S4 directly
:> #load ../examples/proofsystems/s4 Loading file ../examples/proofsystems/s4 ?> rght(imp (nec a) (poss a)).
Yes. ?>
On the first case the system was not able to find a proof for rght(imp (nec a) (poss a)).