Formalizing belief revision in type theory

V.A.J. Borghuis, F. Kamareddine, R.P. Nederpelt

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

This paper formalizes belief revision for belief states in type theory. Type theory has been influential in logic and computer science but as far as we know, this is the first account at using type theory in belief revision. The use of type theory allows an agent's beliefs as well as his justifications for these beliefs to be explicitly represented and hence to act as first-class citizens. Treating justifications as first-class citizens allows for a deductive perspective on belief revision. We propose a procedure for identifying and removing "suspect" beliefs, and beliefs depending on them. The procedure may be applied iteratively, and terminates in a consistent belief state. The procedure is based on introducing explicit justification of beliefs. We study the belief change operations emerging from this perspective in the setting of typed lambda-calculus, and situate these operations with respect to standard approaches.
Original languageEnglish
Pages (from-to)461-500
JournalLogic Journal of the IGPL
Volume10
Issue number5
DOIs
Publication statusPublished - 2002

Fingerprint

Dive into the research topics of 'Formalizing belief revision in type theory'. Together they form a unique fingerprint.

Cite this