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