Modal Theorem Proving,

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1986
Accession Number
ADA325959

Entities

People

  • Martin Abadi
  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Autonomy

DTIC Thesaurus Topics

  • Algorithms
  • Artificial Intelligence
  • Automatic
  • Computer Science
  • Computers
  • Consistency
  • Extraction
  • Formal Languages
  • Guarantees
  • Language
  • Polarity
  • Semantics
  • Sequences
  • Universities

Readers

  • Mathematical Modeling and Probability Theory.