A Completeness Proof for a Logic with an Alternative Necessity Operator |
| |
Authors: | Demri Stéphane |
| |
Institution: | (1) Laboratoire Leibniz - C.N.R.S, 46, Avenue Félix Viallet, 38031 Grenoble, France |
| |
Abstract: | We show the completeness of a Hilbert-style system LK defined by M. Valiev involving the knowledge operator K dedicated to the reasoning with incomplete information. The completeness proof uses a variant of Makinson's canonical model construction. Furthermore we prove that the theoremhood problem for LK is co-NP-complete, using techniques similar to those used to prove that the satisfiability problem for propositional S5 is NP-complete. |
| |
Keywords: | knowledge logic contingency completeness complexity |
本文献已被 SpringerLink 等数据库收录! |