In this paper we discuss the pure logic of necessitation N, a modal logic containing classical propositional calculus, with modus ponens and necessitation as inference rules, but without any axioms for manipulating modalities. We develop a theory of the logic N. We propose a sound and complete Kripke-like semantics for N and build a tableaux system for testing whether a formula is provable from a theory in the logic N. An alternative method to compute modal-free consequences of a finite theory is also given. Our main motivation to consider the logic N comes from the area of nonmonotonic reasoning. The nonmonotonic variant of N seems to be particularly useful in investigations of knowledge sets built when only partial information is available. In particular, this logic N is deeply connected with the default logic. In this paper, we apply our results to problems in nonmonotonic reasoning and we design algorithms for building the nonmonotonic consequence operator associated with N.
|Number of pages||25|
|Journal||Journal of Logic and Computation|
|State||Published - Jun 1992|
Bibliographical noteFunding Information:
M. C. Fitting was partially supported by the National Science Foundation under grant CCR-8901489. V. W. Marek and M. Truszczyiiski were partially supported by the Army Research Office under grant DAAL03-89-K-0124 and by the National Science Foundation and the Commonwealth of Kentucky EPSCoR program under grant RII 8610671.
ASJC Scopus subject areas
- Theoretical Computer Science
- Arts and Humanities (miscellaneous)
- Hardware and Architecture