User Tools
pvs:tools:proveit
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
pvs:tools:proveit [2016/08/25 21:09] jonathan |
pvs:tools:proveit [2016/09/01 18:58] (current) marina |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| ''proveit'' is a command line utility for running the theorem prover in batch mode. | ''proveit'' is a command line utility for running the theorem prover in batch mode. | ||
| - | $ proveit --importchain --clean interval_arith/top.pvs | + | $ proveit --importchain --clean use_bag.pvs |
| + | |||
| + | This example can be used to test ''proveit'' and the installation of NASA PVS library. | ||
| ===== Example ===== | ===== Example ===== | ||
| + | * Download the file below as ''use_bag.pvs'' (uses the NASA Library for Bag) | ||
| + | * All the conjectures can be proved with ''(grind)'' | ||
| + | * execute the above ''proveit'' command in the terminal | ||
| + | * This will generate use_bag.summary | ||
| + | |||
| + | <code> | ||
| + | *** use_bag (17:18:33 8/25/2016) | ||
| + | *** Generated by proveit - ProofLite-6.0.9 (3/14/14) | ||
| + | *** Trusted Oracles | ||
| + | *** MetiTarski: MetiTarski Theorem Prover via PVS proof rule metit | ||
| + | *** | ||
| + | Proof summary for theory use_bag | ||
| + | test1.................................proved - complete [shostak](0.04 s) | ||
| + | test2.................................proved - complete [shostak](0.03 s) | ||
| + | test3.................................proved - complete [shostak](0.01 s) | ||
| + | test4.................................proved - complete [shostak](0.01 s) | ||
| + | Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.09 s) | ||
| + | |||
| + | Grand Totals: 4 proofs, 4 attempted, 4 succeeded (0.09 s) | ||
| + | </code> | ||
| - | <code text nasalib_bag> | + | <code text use_bag> |
| use_bag : THEORY | use_bag : THEORY | ||
| BEGIN | BEGIN | ||
| Line 67: | Line 89: | ||
| | | ||
| END use_bag | END use_bag | ||
| - | <code> | + | </code> |
pvs/tools/proveit.1472159391.txt.gz · Last modified: 2016/08/25 21:09 by jonathan
Page Tools
