Resolution for Epistemic Logics

Abstract

Quantified modal logics have emerged as useful tools in computer science for reasoning about knowledge and belief of agents and systems. An important class of these logics have a possible-world semantics from Kripke. In this paper we report on a resolution proof method for logics of belief that is suitable for automatic reasoning in commonsense domains. This method is distinguished by its use of an unrestricted first-order modal language, a "bullet operator" for dealing with quantified-in variables and skolemization, semantic attachment methods for analyzing the belief operators, and an efficient implementation using a slight modification of ordinary first-order resolution.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 25, 1991
Accession Number
ADA461010

Entities

People

  • Kurt Konolige

Organizations

  • SRI International

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Attachment
  • Automatic
  • Availability
  • Classification
  • Computer Science
  • Computers
  • Contracts
  • Formal Languages
  • Information Operations
  • Instructions
  • Language
  • Monitoring
  • Reasoning
  • Security
  • Words (Language)

Readers

  • Artificial Intelligence
  • Mathematical Modeling and Probability Theory.