Accession Number : ADA325959

Title :   Modal Theorem Proving,

Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Abadi, Martin ; Manna, Zohar

PDF Url : ADA325959

Report Date : MAY 1986

Pagination or Media Count : 21

Abstract : We describe resolution proof systems for several modal logics. First we present the propositional versions of the systems and prove their completeness. The first-order resolution rule for classical logic is then modified to handle quantifiers directly. This new resolution rule enables us to extend our propositional systems to complete first-order systems. The systems for the different modal logics are closely related.

Descriptors :   *COMPUTER LOGIC, *COMPUTER PROGRAM VERIFICATION, COMPUTER PROGRAMMING, SEMANTICS, RULE BASED SYSTEMS, SYSTEMS ANALYSIS, SYNTAX.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE