Compiled only knowing
File(s)DTR02-9.pdf (194.56 KB)
Published version
Author(s)
Bjurling, Bjorn
Broda, Krysia
Type
Report
Abstract
We report on a sound and complete proof system, COOL, for the propositional
fragment of Hector Levesque’s nonmonotonic logic ‘The Logic of
Only Knowing’ [Lev90]. The proof system is devised using the framework of
compiled labelled deductive systems [BrGaRu00], which enables a translation
of COOL-theories into theories of first order logic. With this first order
translation, we are able to perform OL-derivations in standard first order
theorem provers.
The main events in the report are the soundness and completeness theorems
for COOL.
fragment of Hector Levesque’s nonmonotonic logic ‘The Logic of
Only Knowing’ [Lev90]. The proof system is devised using the framework of
compiled labelled deductive systems [BrGaRu00], which enables a translation
of COOL-theories into theories of first order logic. With this first order
translation, we are able to perform OL-derivations in standard first order
theorem provers.
The main events in the report are the soundness and completeness theorems
for COOL.
Date Issued
2002-01-01
Citation
Departmental Technical Report: 02/09, 2002, pp.1-24
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
24
Journal / Book Title
Departmental Technical Report: 02/09
Copyright Statement
© 2002 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
02/9