PVS Theorem Proving Enhancements.

Abstract

The goal of the project was to augment PVS with features that simplified the construction and management of proofs, and to document the PVS functions needed for writing proof strategies. The extensions to PVS developed in this project include: (1) Multiple-proof maintenance, (2) Comments in proofs, (3) Labeling and accessing sequent formulas, (4) Rerunning proofs with checkpoints, (5) Deconstructing EXPAND, and (6) Saved SKIP command.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1997
Accession Number
ADA326917

Entities

People

  • Natarajan Shankar

Organizations

  • SRI International

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Arithmetic
  • Buildings And Structures
  • Computer Science
  • Computers
  • Construction
  • Contracts
  • Engineering
  • Equations
  • Inequalities
  • Lisp Programming Language
  • Maintenance
  • Mathematics
  • Military Research
  • Observatories
  • Printing
  • Research Facilities
  • Scientists

Readers

  • Computer Science.
  • Mathematical Modeling and Probability Theory.