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) Psi and verifying the existence of a program (sequence of inference steps) that, starting from a given knowledge base K, leads Psi to a state satisfying a given formula phi. 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 rules. We then go on to show how the transition system can be used to automatically verify the existence of a derivation, and present experimental results using the Model Based Planner (mbp) which illustrates how the length of the deduction varies for different memory sizes

Verifying space and time requirements for resource-bounded agents

Bertoli, Piergiorgio;Ghidini, Chiara;Serafini, Luciano
2006-01-01

Abstract

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) Psi and verifying the existence of a program (sequence of inference steps) that, starting from a given knowledge base K, leads Psi to a state satisfying a given formula phi. 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 rules. We then go on to show how the transition system can be used to automatically verify the existence of a derivation, and present experimental results using the Model Based Planner (mbp) which illustrates how the length of the deduction varies for different memory sizes
2006
9781595933034
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/2671
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact