PVS‎ > ‎

### inference

This is an inference summary: most, if not all, useful PVS proof commands are included.

Current Sequent Applicable Proof Command[s] and Resulting Sequent[s]
Universal consequent

...

|-

(FORALL (a: A, b: B): alpha),

...

 Applicable Proof Commands Resulting Sequent[s] Skolemization is straightforward.(skolem * ("aa" "bb")) (skolem + ("aa" "bb")) ... |- alpha[a/aa; b/bb], ... Partial skolemization(skolem * ("_" "bb")) (skolem + ("_" "bb")) ... |- (FORALL (a: A): alpha[b/bb],  ... Well founded induction often requires human insight. (induct "a") (induct "b") several sequents corresponding to inductive cases
Existential antecedent
(EXISTS (a: A, b: B): alpha),
...
|-
...
 Applicable Proof Commands Resulting Sequent Skolemization is straightforward.(skolem * ("aa" "bb")) (skolem - ("aa" "bb")) alpha[a/aa; b/bb],...|-...

Universal consequent
...

|-

(FORALL (a: (a?)): p(a)),

...

 Applicable Proof Commands Resulting Sequent Explicit subtype information (skolem * "aa" :skolem-typepreds? t)(apply (then (skolem * "aa")(typepred "aa")) see proof management below a?(aa),... |- p(aa),...

Specific consequent

...

|-

p(eA),

...

assuming eA: A

 Applicable Proof Commands Resulting Sequent Generalization is the inverse of skolemization: requires human insight and often precedes well founded induction.(generalize "eA" "a") ...|-(FORALL (a: A): p(a)),...

Instantiation   often requires human insight: "eA" and "eB" templates may be complex expressions.

Existential consequent

...

|-

(EXISTS (a: A, b: B): alpha),

...

 Applicable Proof Commands Resulting Sequent (inst *  "eA" "eB") (inst +  "eA" "eB") (inst?) ... |- alpha[a/eA; b/eB] ... |- eA: A, ... ... |- eB: B, ...

Universal antecedent

(FORALL (a: A, b: B): alpha), ...

|-

...

 Applicable Proof Commands Resulting Sequent (inst *  "eA" "eB") (inst -  "eA" "eB") (inst?) alpha[a/eA; b/eB],...|-... ... |- eA: A, ... ... |- eB: B, ... (inst-cp *  "eA" "eB") (inst-cp -  "eA" "eB") alpha[a/eA; b/eB],(FORALL (a: A, b: B): alpha),...|-...... |- eA: A, ...... |- eB: B, ...same as above, except for preserving FORALL

Flattening      usually simplifies sequent by removing some logical connectors
 ...|-alpha IMPLIES beta,... ...|-alpha OR beta,... alpha AND beta,...|-...

Applicable Proof CommandResulting Sequent

(flatten)
 alpha,...|- beta,... ...|-alpha, beta,... alpha, beta,...|-...

Case splitting    may complexify proof but is sometimes necessary
 ... |- alpha AND beta, ... alpha OR beta, ... |- ... alpha IMPLIES beta, ... |- ... .. |- alpha IFF beta, ... ... |- IF e THEN a ELSE b ENDIF, ... ... |- CASES e OF ... ENDCASES, ...

Applicable Proof CommandResulting Sequents

(split)
 ... |- alpha, ... ... |- beta, ... alpha, ... |- ... beta, ... |- ... ... |- alpha, ... beta, ... |-  ... alpha, ... |- beta, ... beta, ... |- alpha, ... e, ... |- a, ... ... |- e, b, ... several sequents

... |- ...

 Applicable Proof Command Resulting Sequents Use a lemma on the fly.(case "alpha") alpha, ... |- ... ... |- alpha, ...

Toward  propositional calculus

Boolean equality
... |- ..., alpha = beta, ...

provided alpha, beta: bool

 Applicable Proof Command Resulting Sequent (iff) ... |- ...,  alpha IFF beta

 Embedded test... |- p(IF e THEN a ELSE b ENDIF), ... Embedded cases... |- p(CASES e OF ... ENDCASES), ...

Applicable Proof CommandResulting Sequent

(lift-if)
 ... |- IF p(e) THEN p(a) ELSE p(b) ENDIF, ... ... |- CASES e OF ... ENDCASES, ...where p applies to each clause result

Decision  procedures for propositional calculus and linear arithmetics

propositional sequent
NOT, AND, OR, IMPLIES, IFF
IF, CASES

 Applicable Proof Command Resulting Sequents (prop) some sequents or none

linear arithmetic sequent
=, <=, >, >=

 Applicable Proof Command Resulting Sequents (assert) simplified sequent (or nomore sequent)

propositional + linear arithmetic sequent

 Applicable Proof Command Resulting Sequents (ground) some sequents or none

Using  function definitions

sequent containing f (...)
typically with f non recursive

 Applicable Proof Command Resulting Sequent (expand "f")(expand "f" +)(expand "f" -) sequent with some f(...)function calls unfolded

sequent containing f(...)
typically with f recursive

 Applicable Proof Command Resulting Sequent (expand "f" :if-simplifies t) f(...) calls are unfoldedprovided some simplification occurs

... f(e1) ... f(e2) ... |- ... f(e3) ...

 Applicable Proof Command Resulting Sequent (expand "f" * 2)(expand "f" - 2) ... f(e1) ... fe2_unfolded ... |- ... f(e3) ...

sequent containing
f(...)
 Applicable Proof Command Resulting Sequent (auto-rewrite "f") sequent unchangedsubsequent (ground) will automatically trigger (expand "f" :if-simplifies t)

Using  lemmas, theorems, corollaries or the like

antecedents |- consequents

 Applicable Proof Command Resulting Sequent[s] (lemma "foo") fooLemmaFormula, antecedents |- consequents (use "foo") fooLemmaFormulaInstance, antecedents |- consequents combines (lemma "foo") and (inst?) (rewrite "foo") sequent with some term rewrittenaccording to lemma main equalitylemma hypotheses may trigger subgoals (rewrite "foo" :subst ("a" ... "b" ...)) same as above but specifiesinstantiation in part or whole (rewrite "foo" :dir RL) same as (rewrite "foo") except thatmain equality is applied from right to left (rewrite "foo" :fnums +:target-fnums +) same as (rewrite "foo") except thatrewriting only occurs within consequents (auto-rewrite "foo")Useful if "foo" lemma isa good rewrite lemma sequent unchangedsubseqent (ground) will trigger rewritingaccording to "foo" lemma if a match occursand all lemma hypotheses can be proved

Dealing with equality:  prefer (assert) whenever applicable

proving function equality
... |- f = g, ...

assuming f, g: [T -> U]

 Applicable Proof Command Resulting Sequent[s] (apply-extensionality :hide? t) ... |- f(x!1) = g(x!1), ...

Using an equality
a = b, ... |- ...

 Applicable Proof Command Resulting Sequent (replace -1 :hide? t) ...[a/b] |- ...[a/b] (replace -1 :hide? t :dir RL) ...[b/a] |- ...[b/a]

hiding
alpha1,
alpha2,
alpha3
|-
beta1
beta2
 Applicable Proof Command Resulting Sequent (hide -2 -3 1)may hinder proof robustness alpha1|-beta2 |-beta1

renaming constants
..., p(X!1, X!2), ...
|-
..., q(X!2, Y!3), ...

 Applicable Proof Command Resulting Sequent (name-replace "b" "X!2") .., p(X!1, b), ...|-..., q(b, Y!3), ... (name-replace*("a" "X!1" "b" "X!2" "c" "X!3")) ..., p(a, b), ...|-..., q(b, c), ...

... |- ...

 Applicable Proof Command Resulting Sequent (comment "Bla bla bla.") ... |- ...sequent is left unchanged

... |- ...

 Applicable Proof Command Resulting Sequent (apply (then c1 c2 c3)) sequent resulting from sequential applicationof commands c1, c2, c3 (undo) go back one proof step to parent sequent (postpone) switch to next sequent,therefore postponing current sequent proof (quit)quit quit PVS prover, saving current partial proof

Recover from  PVS crash

LISP error!!!
(PVS bug)

 Applicable Proof Command Resulting Sequent (restore) goes back to previous coherent state of the proof, just before the proof command responsible for PVS crash

Believe in  miracles!

... |- ...

 Applicable Proof Command Resulting Sequent[s] (grind) either some clumsy often unprovable sequentsor finishes proof of sequentmost powerful PVS proof command: OK to try,but undo if does not complete the proof

## More on PVS inference

The slides below have been obtained by conversion from “ppt” to “Google slides” format: the translation is not perfect! Please wait for fixes; check the “ppt” or “pdf” versions in the mean time (bottom of the page).

#### PVS inference - Slides

ą
Paul Y Gloess,
18 sept. 2013, 10:04
Ċ
Paul Y Gloess,
13 sept. 2013, 07:07
ć
Paul Y Gloess,
13 sept. 2013, 07:07