Deductive Algorithmic Knowledge

The framework of algorithmic knowledge assumes that agents use algorithms to compute the facts they explicitly know. In many cases of interest, a logical theory, rather than a particular algorithm, can be used to capture the formal reasoning used by the agents to compute what they explicitly know. We introduce a logic for reasoning about both implicit and explicit knowledge, where the latter is given with respect to a deductive system formalizing a logical theory for agents. The highly structured nature of such logical theories leads to a very natural axiomatization of the resulting logic over a deductive system. In the case when the deductive system is in fact tractable, we show that the decision problem for the logic is NP-complete, no harder than propositional logic.

• Type: Conference
• Year: 2004
• Where: AMAI
• Authors: Riccardo Pucella
• Keywords: AMAI 2004, Artificial Intelligence, Deductive System, Formal Reasoning, Logical Theory