Example 3 Suppose Alice defines "vehicle" as in Example 1. Then stubA = (has2wheels ∨ has3wheels ∨ has4wheels ∨ *has6wheels*) ∧
(hasHandlebar ∨ *hasSteeringWheel*) ∧ (hasMotor ∨ has2bicyclePedals ∨ has4bicyclePedals ∨ *hasTowBar* )
is the stubbornness part of Alice's knowledge whose interpretation is I(*stub*A) =
{bicycle,tandem, motorbike,scooter,truck, car,trailer, chariot}. Let flex kA = has4wheels ∧ hasSteeringWheel ∧ (hasMotor ∨ *has2bicyclePedals*)
be the CAF of Alice that it is not equivalent to her stubbornness knowledge and its interpretation is I(*flex* kA) = {car,truck} ⊂ I(*stub*A). Suppose Alice changes her CAF
by means of a weakening action (W); then:
flex k+1 A = (has4wheels ∨ has2wheels) ∧ (hasSteeringWheel ∨ *hasHandlebar* ) ∧
(hasMotor ∨ *has2bicyclePedals*)
The interpretation of *flex* k+1 Ais I(*flex* k+1 A) = {motorbike,scooter, car,truck} ⊂ I(*flex* kA).

Otherwise, suppose Alice changes her CAF by means of a changing theory action (C); then:
flex k+1 A = has6wheels ∧ hasSteeringWheel ∧ (hasMotor ∨ *hasTowBar* )
The interpretation of *flex* k+1 Ais I(*flex* k+1 A) = {truck,trailer} and I(*flex* k+1 A) *
I(*flex* kA). 

## 3 The Mn Process

In this section, we formalize the MN process by defining the negotiation language
(Section 3.1), i.e. how the agents send their proposals to the opponents, and the negotiation rules (Section 3.2) governing the development of the MN process, both for bilateral (Section 3.2.1) and 1-n negotiation (Section 3.2.2). We then (Section 3.3)
show how the bilateral MN develops depending upon the relation between the stubborn knowledge of the agents. We do not show the development of the 1-n MN because it can be viewed as n − 1 instances of bilateral MN between the auctioneer and the other agents, where n is the number of the involved agents.

During the MN, agents make proposals and say if they are in agreement or not with respect to the proposals made by the opponents. Proposals are negotiation formulas like j : ϕ, where we assume that the opponent i is able to recognize the name label j in j : ϕ and remove it in order to evaluate ϕ.

In general, negotiating agents may not share the same language but have different signatures. Hence, when i evaluates an assertion by j, she first has to *translate* the symbols occurring in it to symbols belonging to her signature. Such a translation depends, of course, on the particular terms that are being considered for the negotiation, so we assume abstractly that for each pair of agents (*i, j*) there is the *translation function* τi,j such that:
τi,j : Σj → Σi.