From SMART to agent systems development

n order for agent-oriented software engineering to prove effective it must use principled notions of agents and enabling specification and reasoning, while still considering routes to practical implementation. This paper deals with the issue of individual agent specification and construction, departing from the conceptual basis provided by the smart agent framework. smart offers a descriptive specification of an agent architecture but omits consideration of issues relating to construction and control. In response, we introduce two new views to complement smart: a behavioural specification and a structural specification which, together, determine the components that make up an agent, and how they operate. In this way, we move from abstract agent system specification to practical implementation. These three aspects are combined to create an agent construction model, actsmart, which is then used to define the AgentSpeak(L) architecture in order to illustrate the application of actsmart.

Herbrand's Theorem and Equational Reasoning: Problems and Solutions

The famous Herbrand's theorem of mathematical logic plays an important role in automated theorem proving. In the first part of this article, we recall the theorem and formulate a number of natural decision problems related to it. Somewhat surprisingly, these problems happen to be equivalent. One of these problems is the so-called simultaneous rigid E-unification problem. In the second part, we survey recent result on the simultaneous rigid E-unification problem.

Kanger's Choices in Automated Reasoning

This article explains these choices and their place in modern automated deduction.