User Tools
pvs:commands
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
pvs:commands [2016/07/19 21:52] jonathan |
pvs:commands [2017/09/06 19:33] (current) jonathan |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ~~NOTOC~~ | ||
| - | <html><strong>This is my bold text</strong></html> | ||
| ====== PVS/Emacs Shortcuts ====== | ====== PVS/Emacs Shortcuts ====== | ||
| + | |||
| + | [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:pvs:shortcuts:start#keyboard_shortcuts|SEL wiki]] | ||
| + | |||
| + | ====== Restarting PVS ====== | ||
| + | If you have a run-away prover command (e.g. GRIND), you can type | ||
| + | ''C-c C-c'' (while in the *pvs* buffer), which will drop you into Lisp. | ||
| + | At the <rcl> prompt, type (''restore'') to get back to the previous | ||
| + | sequent. | ||
| + | |||
| + | If PVS has lost its mind, type ''M-x reset-pvs''. Note. During garbage | ||
| + | collection, this command will not engage immediately. | ||
| + | |||
| + | See Survival-Tips.pdf | ||
| ====== Emacs shortcuts with PVS ====== | ====== Emacs shortcuts with PVS ====== | ||
| Line 24: | Line 35: | ||
| M-x show-proofs-theory -- Show all proofs of theory | M-x show-proofs-theory -- Show all proofs of theory | ||
| + | M-x x-show-current-proof -- show current proof under x11 | ||
| step-proof, prs (C-c C-p s) Start proof and set up for stepping | step-proof, prs (C-c C-p s) Start proof and set up for stepping | ||
| Line 59: | Line 71: | ||
| </code> | </code> | ||
| - | ====== Restarting PVS ====== | + | ====== Keyboard Shortcuts ====== |
| - | If you have a run-away prover command (e.g. GRIND), you can type | + | |
| - | ''C-c C-c'' (while in the *pvs* buffer), which will drop you into Lisp. | + | |
| - | At the <rcl> prompt, type (''restore'') to get back to the previous | + | |
| - | sequent. | + | |
| - | If PVS has lost its mind, type ''M-x reset-pvs''. Note. During garbage | ||
| - | collection, this command will not engage immediately. | ||
| - | See Survival-Tips.pdf | ||
| - | |||
| - | ====== Proof Rules ====== | ||
| - | |||
| - | <code> | ||
| - | % When PVS proofs are expressed in a sequent calculus, the proof rule (flatten) | ||
| - | % (corresponds to the bottom-up application of either and-left or or-right, i.e., | ||
| - | |||
| - | % A,B,Gamma |- Delta | ||
| - | % ------------------------ (and-left) | ||
| - | % A /\ B, Gamma |- Delta | ||
| - | |||
| - | |||
| - | % Gamma |- Delta, A,B | ||
| - | % ----------------------- (or-right) | ||
| - | % Gamma |- Delta, A \/ B | ||
| - | |||
| - | % On the other hand, the proof rule (split) corresponds to the bottom-up | ||
| - | % application of either and-right or or-left, i.e., | ||
| - | |||
| - | |||
| - | % Gamma |- A, Delta Gamma |- B, Delta | ||
| - | % -------------------------------------- (and-right) | ||
| - | % Gamma |- A /\ B, Delta | ||
| - | |||
| - | |||
| - | % A, Gamma |- Delta B,Gamma |- Delta | ||
| - | % ----------------------------------- (or-left) | ||
| - | % A \/ B, Gamma |- Delta | ||
| - | </code> | ||
| - | |||
| - | ===== Keyboard shortcuts ===== | ||
| <html> | <html> | ||
| <head> | <head> | ||
| Line 131: | Line 105: | ||
| the formula numbered f in Hidden to the sequent.</strong><br> | the formula numbered f in Hidden to the sequent.</strong><br> | ||
| </p> | </p> | ||
| - | <table border="1" cellpadding="10" width="760"> | + | <table border="1" cellpadding="10" width="600"> |
| <tbody> | <tbody> | ||
| <tr> | <tr> | ||
| Line 286: | Line 260: | ||
| </body> | </body> | ||
| </html> | </html> | ||
| + | |||
| + | |||
| + | ====== Proof Rules ====== | ||
| + | |||
| + | <code> | ||
| + | % When PVS proofs are expressed in a sequent calculus, the proof rule (flatten) | ||
| + | % (corresponds to the bottom-up application of either and-left or or-right, i.e., | ||
| + | |||
| + | % A,B,Gamma |- Delta | ||
| + | % ------------------------ (and-left) | ||
| + | % A /\ B, Gamma |- Delta | ||
| + | |||
| + | |||
| + | % Gamma |- Delta, A,B | ||
| + | % ----------------------- (or-right) | ||
| + | % Gamma |- Delta, A \/ B | ||
| + | |||
| + | % On the other hand, the proof rule (split) corresponds to the bottom-up | ||
| + | % application of either and-right or or-left, i.e., | ||
| + | |||
| + | |||
| + | % Gamma |- A, Delta Gamma |- B, Delta | ||
| + | % -------------------------------------- (and-right) | ||
| + | % Gamma |- A /\ B, Delta | ||
| + | |||
| + | |||
| + | % A, Gamma |- Delta B,Gamma |- Delta | ||
| + | % ----------------------------------- (or-left) | ||
| + | % A \/ B, Gamma |- Delta | ||
| + | </code> | ||
| + | |||
| + | ===== Keyboard shortcuts ===== | ||
| + | |||
| <code> | <code> | ||
pvs/commands.1468965128.txt.gz · Last modified: 2016/07/19 21:52 by jonathan
Page Tools
