Verifying space and time requirements for resource-bounded agents

The effective reasoning capability of an agent can be defined as its capability to infer, within a given space and time bound, facts that are logical consequences of its knowledge base. In this paper we show how to determine the effective reasoning capability of an agent with limited memory by encoding the agent's reasoning system as a finite state machine (FSM) and verifying the existence of a program (sequence of inference steps) that, starting from a given knowledge base K, leads to a state satisfying a given formula . Our approach is general enough to admit verification of any reasoning agent whose inference rules can be encoded as transitions between FSM states. As an illustration, we show how to encode two example reasoners: a classical propositional reasoner which can derive all classical consequences of its knowledge base given unlimited memory, and a forward-chaining rule-based reasoner of the kind found in many applications employing ontological reasoning and business...

• Type: Conference
• Year: 2006
• Where: ATAL
• Authors: Natasha Alechina, Mark Jago, Piergiorgio Bertoli, Brian Logan, Chiara Ghidini, Luciano Serafini
• Keywords: ATAL 2006, Effective Reasoning Capability, Intelligent Agents, Knowledge Base, Reasoning