# quantification_of_resource_production_incompleteness__b81a6c34.pdf

Quantification of Resource Production Incompleteness

Yakoub Salhi CRIL, U. Artois & CNRS, Lens, France salhi@cril.fr

In a situation where an agent has to produce specific resources using the available ones, it may not be possible to achieve the complete goal, but only obtaining some of its parts. This incompleteness problem calls for reasoning models to make rational decisions. In this paper, we introduce a logic-based framework for measuring resource production incompleteness: the greater the value returned by a measure, the greater is the intensity of incompleteness. After motivating our work by describing situations where the incompleteness measures can be applied, we introduce our framework by using a postulate-based approach. To some extent, the incompleteness measures can be seen as a counterpart of inconsistency measures in resource logics. Here, intuitionistic affine logic is used for representing and reasoning about resource consummation and production. Besides, we propose different notions that are useful for defining different types of incompleteness measures. We also present several measures to illustrate the introduced concepts and notions.

Introduction Resource management is an essential task in several areas, including economics, social policy, and computer science. In this work, we focus on the general situation where an agent has to use available resources to attain a given goal. One of the main problems that an agent may face in this context is when the available resources do not allow reaching the entire goal but only some of its parts. Indeed, under this incompleteness problem, an agent may need to represent and reason about the difficulty to produce the desired resources. This explains the interest in defining reasoning tools for making particularly rational decisions. The purpose of this paper is to introduce a logic-based framework for defining measures that can be used for reasoning and analyzing the intensity of resource production incompleteness. Up to a point, these measures can be seen as a counterpart of inconsistency measures in resource logics. Inconsistency measures are functions that associate non-negative values with knowledge bases to quantify the amount of conflicts (e.g. see (Hunter and Konieczny 2010; Thimm 2016; Bona et al. 2018; Thimm 2018a)). By contrast, rather than focusing on truth as in the case of inconsistency

Copyright c 2021, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

in classical logic, we concentrate in this work on the use of formulas as resources by dealing with resource availability, consummation, and production. To give an illustration of this point, consider the implication φ = have-one-dollar have-a-metro-ticket. Clearly, we obtain in classical logic have-one-dollar, φ have-one-dollar have-a-metro-ticket. This means that we can have a metro ticket without consuming the available dollar, which is not appropriate if the formulas are used to represent resources. Linear logic is a substructural logic that can be used for reasoning about resource-sensitive problems (Girard 1987). The main idea behind the resource-oriented interpretation is to consider formulas in a proof as resources that can be consumed or produced. In particular, this logic takes into account the number of occurrences of formulas (two occurrences of a given formula have a different meaning from a single occurrence of the same formula). The intuitionistic variant of linear logic was defined through the sequent calculus of linear logic by restricting sequents to have exactly one formula on the right-hand side (Girard and Lafont 1987; Troelstra 1992). This variant allows reasoning about resources in a more natural way than linear logic and avoiding some logical connectives that are difficult to explain in terms of resources (there is particularly no negation operator). This point can be illustrated by encodings of problems such as Petri net reachability (Engberg and Winskel 1990, 1993) and classical AI planning (Kanovich and Vauzeilles 2001). We consider in this work intuitionistic affine logic, which is obtained from intuitionistic linear logic by adding the structural rule of weakening. This structural rule is needed because we are interested in having the monotonicity property, that is, if resources Γ allow producing a resource φ, then it is also possible to produce φ by adding new elements to Γ. It appears in the literature that intuitionistic affine logic is appropriate for reasoning about resources in several contexts (e.g. see (Kamide 2006; Porello and Endriss 2010; Kanovich and Vauzeilles 2011; Bugliesi et al. 2013; Ferm uller and Lang 2017)). In this paper, we first discuss resource managementrelated situations to motivate our proposal and show how incompleteness measures can be applied for reasoning about resource consummation and production. Then, we present our framework for quantifying resource production incompleteness. An incompleteness measure is defined as a func-

The Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI-21)

tion that associates non-negative values with pairs that represent available resources and goals, where each value intends to describe the degree of difficulty to obtain the considered goal using the available resources. Intuitionistic affine logic is used in this context for representing and reasoning about resources. The definition of incompleteness measures is under guidance of postulates that are used to capture important rational aspects related to resource consummation and creation. For instance, our definition uses a postulate that states that the amount of incompleteness can only grow by adding new resources to the goal (a more demanding goal). Additionally, we introduce properties that can be used for emphasizing differences between measures. Then, we propose notions that are useful for defining different types of incompleteness measures and present measures that are based on them. Intuitively, these notions can be exploited in a similar way as maximal consistent subsets and minimal inconsistent subsets for defining inconsistency measures in the case of classical logic (e.g. see (Thimm 2018b)). Particularly, we introduce the notion of maximal produced sub-multisets that can be seen as possible optimal solutions of the resource production problem, since they are obtained by maximizing the satisfied part in the goal (the maximality is considered with respect to multiset inclusion). We also introduce the notion of minimal adjustment multiset that is defined as a minimal multiset of positive literals that has to be added to the available resources to achieve the goal. This notion represents specific minimal changes that can be applied to the available resources to attain the objective.

Resource Logic Multiset

In this paper, the multiset structure allows taking into account the number of formula occurrences. A multiset can be seen as a set in which every element may have multiple occurrences. It is thus a generalization of the notion of set. For instance, {a, b, b, c} is a multiset where b occurs twice. A multiset S can also be written as a set of elements of the form n : e where n is a strictly positive integer representing the number of the occurrences of e in S. For instance, the previous example corresponds to {1 : a, 2 : b,1 : c}. If an element e occurs once, 1 : e can be replaced with e. We use m(e, S) to denote the number of the occurrences of the element e in the multiset S. Moreover, given a set X, we use mult(X) to denote the set of finite multisets of elements occurring in X. We also use set(S) to denote the set containing the elements occurring in the multiset S. In the same way as in the case of sets, we write e S to denote the property that e belongs to the multiset S (e occurs at least once in S). The size of S, denoted |S|, is defined as the number of element occurrences in S, that is |S| = P e S m(e, S). Further, S is said to be a sub-multiset of S , written S S , iff m(e, S) m(e, S ) for every e S. We say that S is a proper sub-multiset of S , written S S , iff S S and S = S . The multiset union operator, denoted , is defined as follows: S S = {m(e, S)+m(e, S ) : e | e S or e S }. For instance, {a, b, b, c} {a, b, d} = {a, a, b, b, b, c, d} =

{2 : a, 3 : b, c, d}. In addition, the relative complement of S in S, denoted S \ S , is the multiset {m(e, S) m(e, S ) : e | e S and m(e, S) > m(e, S )}. For example, {a, b, b, c, c, c} {a, a, b, c, d} = {b, c, c}. The multiset intersection operator, denoted , is defined as follows: S S = {min(m(e, S), m(e, S )) : e S and e S }, where min stands for the minimum.

Intuitionistic Affine logic We use multiplicative-additive intuitionistic affine logic (IMAAL) for representing resources. Intuitively, this logic is obtained by removing the contraction rule if we formulate it using the sequent calculus of classical logic. IMAAL is also defined by adding the weakening rule to intuitionistic linear logic. Let us recall that the contraction and weakening rules are defined as follows: Γ, φ, φ ψ

Γ, φ ψ [contraction] Γ ψ

Γ, φ ψ [weakening]

In fact, removing the contraction rules allows attaching importance to the number of occurrences: n occurrences of a given formula can have a different meaning from n 1 occurrences of the same formula. The set of formulas, denoted FIMAAL, is defined inductively starting from a set of positive literals, denoted PL, with additional constants , 1 and , and using the binary connectives , , and 1. We call and additive connectives, and and multiplicative connectives. Similarly to conjunction and disjunction in classical logic, , and are associative and commutative. We sometimes use the

notation n : φ inside formulas for

n times z }| { φ φ. We also use N{φ1, . . . , φn} to denote φ1 φn. The set of positive literals occurring in a formula φ is denoted PLit(φ). Intuitively, the additive connective and can be interpreted in the same way as conjunction and disjunction in classical logic, respectively. The multiplicative connectives allows dealing with the formulas as resources. For example, the formula $ $ $ can be used to represent the fact that an agent has three dollars. The connective can be seen as a resource variant of implication in the sense that φ ψ indicates that the resource ψ can be produced by consuming the resource φ. The choice of IMAAL is motivated by several reasons. First, this logic allows dealing with formulas as resources since it is sensitive to the number of occurrences (e.g. having one dollar is different from having two dollars). Second, the inference process of IMAAL integrates the concepts of resource consumption and production: formulas are consumed in order to produce other formulas. For example, we have {$, $ coffee} coffee without having {$, $ coffee} coffee $, since the dollar on the lefthand side is consumed to produce a coffee. Third, IMAAL satisfy the property of monotonicity: if Γ φ then Γ φ

1In (Girard 1987), the connectives and are denoted by & and respectively. However, we use the notational convention of classical logic to emphasize the fact that these connectives are similar to conjunction and disjunction in classical logic (this convention is also used in (Restall 2000; Paoli 2002)).

φ φ [Id] 1 [1R] Γ [ R] Γ, ψ [ L] Γ ψ

Γ, φ1, φ2 ψ

Γ, φ1 φ2 ψ [ L] Γ1 ψ1 Γ2 ψ2 Γ1, Γ2 ψ1 ψ2 [ R] Γ, φ1 ψ Γ, φ2 ψ

Γ, φ1 φ2 ψ [ L] Γ ψi Γ ψ1 ψ2 [ i {1,2} R ]

Γ1 φ1 Γ2, φ2 ψ

Γ1, Γ2, φ1 φ2 ψ [ L] Γ, φ ψ

Γ φ ψ [ R] Γ, φi ψ

Γ, φ1 φ2 ψ [ i {1,2} L ] Γ ψ1 Γ ψ2 Γ ψ1 ψ2 [ R]

Figure 1: Sequent Calculus CIMAAL

for every Γ Γ (it is a consequence of the rule of weakening). To put it another way, this property means that if the available resources allow producing a resource, then it is also possible to produce this resource by enriching the available resources. It is worth noting that (intuitionistic) linear logic does not satisfy this property of monotonicity. Finally, in the literature, IMAAL has been shown appropriate for reasoning about resources in several contexts (e.g. see (Kamide 2006; Porello and Endriss 2010; Kanovich and Vauzeilles 2011; Bugliesi et al. 2013; Ferm uller and Lang 2017)). In this work, we only use IMAAL without the constant , denoted IMAAL\ . This allows us to avoid the principle of explosion, that is, any resource can be produced form . Avoiding this principle leads to a more natural resource interpretation. To clarify this point, consider the fact that having the resource $ $ means that from the resource $ $, anything can be produced. Furthermore, it is difficult to interpret $ $ in terms of resources: the resource 2 : $ can be transformed into falsehood. Additionally, the use of IMAAL with as the underlying logic invalidates desirable properties that we consider for quantifying the amount of production incompleteness. Regarding computational complexity, the provability problem in IMAAL\ is PSPACEcomplete, even the extended Horn fragment -Horn (which is without the constant ) is PSPACE-complete (Kanovich 1992).

Sequent Calculus

Let us now describe briefly the sequent calculus of IMAAL used for defining validity. We define an inference rule as a

structure of the following form: P1 Pn

C [R] , where

R is its name, C its conclusion, and P1, . . . , Pn its premises. An axiom is a rule without any premise. In the case of IMAAL, a sequent is a structure of the form Γ ψ where Γ is a multiset of formulas and ψ a formula. The validity of a sequent in IMAAL can be defined through the sequent calculus CIMAAL depicted in Figure 1 (Girard 1987; Troelstra 1992). Note that we use the standard notational convention in our description of CIMAAL that uses the comma to represent the multiset union in every sequent. For instance, the rule [ L]

can be rewritten as follows: Γ {φ1} {φ2} ψ

Γ {φ1 φ2} ψ [ L] .

Proof-search in a sequent calculus corresponds to a

bottom-up construction of derivations using its inference rules, that is, a construction from the conclusion to instances of axioms (e.g. see (Troelstra and Schwichtenberg 1996)). For example, the proof of the sequent p, q, p r, (r q) (r s) q q in CIMAAL is as follows:

[ R] q, q q q

[ L] q, r, r q q q

[ L] p, q, p r , r q q q

[ 1 L] p, q, p r, (r q) (r s) q q

Applications This work aims at proposing a framework for measuring the severity of incompleteness of resource production. In this regard, we define an incompleteness measure as a function that associates a non-negative value with every ordered pair of multisets of formulas; the first multiset represents the available resources, while the second represents the goal. Although we use intuitionistic affine logic for resource representation, the approach behind our framework can be adapted to other resource representation formalisms. In order to motivate our proposal, we describe in this section situations where quantifying incompleteness can be applied. The main idea consists in using the preference ordering induced by an incompleteness measure for making a decision about how the available resources have to be exploited. We first deal with the case of a user that has to select a service, among the suggested ones, for producing desired resources. We then consider the situation where the available resources have to be shared between a set of agents having different goals. Finally, we show how the incompleteness measures can be involved in approaches for agent grouping.

Service Selection under Incompleteness Let us consider the situation described in Figure 2. It corresponds to an agent that has to choose a service among four available ones to produce certain desired resources, that is, the three files f1, f2 and f3. Moreover, the agent as well as the services possess resources. In particular, the user has the following resources that can be used in combination with the selected service: two dollars (2 : $), three time intervals (3 : TI) and two memory units (2 : MU). For instance, the

R1 =(2 : $) (1 : TI) f2, (3 : $) (2 : TI) f3 R2 = (2 : $) (2 : TI) (3 : MU) (f1 f2),1 : MU

(2 : $) (2 : TI) (2 : MU) (f2 f3), R3 = (2 : $) (3 : TI) (2 : MU) (f1 f2) (2 : $) (3 : TI) (f1 f3) R4 =

R0 = 2 : $, 3 : Time Interval (TI), 2 : Memory Unit (MU)

Goal = Files : f1, f2, f3

R0, R2 f1 f2 User

Figure 2: An example of service selection.

user s resources and the service S2 allow obtaining the files f1 and f2, since we have 2 : $, 3 : TI, 2 : MU, (2 : $) (2 : TI) (3 : MU) (f1 f2), 1 : MU f1 f2. Clearly, it is reasonable to consider that the service S2 is better than S1 because the latter allows only producing the file f1: the incompleteness is more severe using S1. However, it is more difficult to compare S4 and S2 since the former allows obtaining the file f3 (R0 R4 f1 f3), which cannot be produced using S2, and conversely S2 allows producing f2, which cannot be obtained using S4. By inducing an ordering over the available services, a measure that quantifies the severity of incompleteness can be helpful for choosing the appropriate service. In our framework, the definition of incompleteness measures is driven by rationality postulates, which provides a flexible approaches that can be adapted to the considered context (the suitable measure is obtained by choosing the suitable properties).

Resource Sharing We deal here with the problem of sharing resources between agents having different goals. The principal difficulty occurs when it is not possible to satisfy all goals. In order to illustrate this point, consider that the available resources R are as follows:

2 : Energy Unit (EU), 2 : $, and two raw materials m1 and m2;

φ1 = EU $ p1 p2 (the combination of the resources EU and $ allows producing two products p1 and p2);

φ2 = m1 $ p3 (m1 and $ allow producing the product p3);

φ3 = m2 EU p4 (m2 and EU allow producing the product p4).

Additionally, consider the following three agent requests: (a1) the products p1 and p4, (a2) p2 and p3, and (a3) $ and EU. One can see that it is not possible to satisfy these three requests, since R p1 p2 p3 p4 $ EU. To partially satisfy the considered requests, one can share

the resources as follows: R1 = {EU, $, φ1} for the agent a1, R2 = {m1, $, φ2} for a2, and R3 = {EU} for the agent a3. Thus, the agents a1, a2 and a3 can obtain p1, p3 and EU respectively (R1 p1, R2 p3 and R3 EU). Another way to share the available resources is as follows: R 1 = {2 : EU, $, m2, φ1} for a1, R 2 = {m1, $, φ2} for a2, and R 3 = {} for a3, which allows satisfying the goal of a1 (R 1 p1 p4), but at the expense of a3. Incompleteness measurement can be used in this context to prevent imbalance in resource sharing. For example, one can require the property that the maximum incompleteness value has to be reduced as far as possible, which can be seen as a simple way to share the severity of incompleteness between the agents. More precisely, the previous property can be expressed as follows: S is an acceptable partition of the available resources if and only if for every other resource partition S , max{M(Ra, Ga) : a A} max{M(R a, Ga) : R a S }, where M is an incompleteness measure, A is the set of the considered agents, Ra (resp. R a) is the set of the resources that are given to the agent a in S (resp. S ), and Ga is the goal of the agent a. In fact, using incompleteness measurement, it is possible to define other more sophisticated properties for reasoning about resource sharing under incompleteness.

Agent Grouping We show that quantifying incompleteness of resource production can guide the task of assigning agents to groups. The main idea consists in using incompleteness measures to improve the quality of the built groups by reducing the incompleteness values. In this context, we consider that every agent has resources and a goal. The cooperation between agents aims at achieving their goals. For instance, consider the following six agents:

a1: R1 = {2 : $, $ Coffee} (the available resources), G1 = Bus-Ticket (the required goal);

a2: R2 = {5 : $}, G2 = Bus-Ticket Book;

a3: R3 = {$, 3 : $ Sandwich, 3 : $ Salad}, G3 = Sandwich;

a4: R4 = {$ Bus-Ticket}, G4 = Coffee;

a5: R5 = {10 : $}, G5 = Salad Coffee Book;

a6: R6 = {4 : $ Book, $ Coffee}, G6 = Coffee.

Our purpose is to compose three groups of cooperating agents with two agents per group. One can see that the group C1 = {a1, a4} allows their agents to achieve their goals since we have R1 R4 G1 G4. However, the group C2 = {a3, a5} allows only satisfying the goal of the agent a3. Using an incompleteness measure M, the value associated to the group C2 (M(R3 R5, {G3, G5})) can be used to determine the quality of this group, since, even if C2 does not allow a5 to achieve the associated goal, it allows satisfying one of its parts (R3 R5 G3 Salad). In fact, there is no agent that can allow a5 to achieve all the parts of the associated goal. Thus, the use of an incompleteness measure can be helpful in improving the quality of the group containing a5 by reducing the incompleteness value.

Incompleteness Measures

This section is devoted to the introduction of the notion of incompleteness measure. We first introduce the notion of resource production scenario, which corresponds to an ordered pair that represents the available resources and the goal. Then, an incompleteness measure is defined as a function that associate non-negative values with the resource production scenarios and satisfies some rationality postulates.

Definition 1 (RP-Scenario). A resource production scenario (RP-scenario) is an ordered pair (R, G) of finite multisets of FIMAAL\ ; R is the multiset of available resources and G the goal.

Given a function M defined over RP-scenarios and an RP-scenario S = (R, G), we sometimes write for the sake of simplicity M(R, G) to refer to M(S) (it does not mean that M is a function with two parameters). From now on, we use RPSIMAAL\ to denote the set of RP-scenarios.

Example 1. The RP-scenario ({2 : $, $ Coffee, $ $ Bus-Ticket}, {Coffee, Bus-Ticket}) represents the situation where the aim is to produce a coffee and a bus ticket using two dollars and the transformation processes $ Coffee and $ $ Bus-Ticket. Clearly, two dollars do not allow us to have both a coffee and a bus ticket, which corresponds to a situation of incompleteness.

We use R+ to denote the set of positive real number augmented with a greatest element denoted .

Definition 2 (Incompleteness Measure). An incompleteness measure M is a function RPSIMAAL\ R+ that satisfies the following properties:

COMPLETENESS: (R, G) RPSIMAAL\ , M(R, G) = 0 iff R N G; GOAL ADDITION: (R, G) RPSIMAAL\ and φ FIMAAL\ , M(R, G {φ}) M(R, G);

EXTENSION: (R, G) RPSIMAAL\ and φ FIMAAL\ , M(R {φ}, G {φ}) M(R, G).

COMPLETENESS says that the incompleteness value is null if and only if it is possible to produce the entire goal, which means that an incompleteness measure must allow differentiating completeness from incompleteness. GOAL ADDITION means that the amount of incompleteness can only grow by adding new resources to the goal. Regarding EXTENSION, it states that the amount of incompleteness cannot increase by adding the same resource to both the available resources and the desired goal. This comes from the fact that a resource can be used to obtain itself, that is, φ φ holds for every φ FIMAAL\ . For instance, the simple function defined as follows is an incompleteness measure:

Mb(R, G) = 0 if R N G 1 otherwise

This measure allows only distinguishing completeness from incompleteness.

The following proposition says that adding formulas to the available resources cannot increase the amount of incompleteness. The validity of this property explains why it is not used as a rationality postulate in Definition 2.

Proposition 1. Let M be an incompleteness measure. Then, for every (R, G) RPSIMAAL\ and every φ FIMAAL\ , M(R {φ}, G) M(R, G) holds.

Proof. Using GOAL ADDITION, we obtain M(R {φ}, G) M(R {φ}, G {φ}). Furthermore, using EXTENSION, M(R {φ}, G {φ}) M(R, G) holds. Thus, M(R {φ}, G) M(R, G) ensues.

Let us now examine the following additional properties on incompleteness measures:

SUBADDITIVITY: (R R , G G ) RPSIMAAL\ , M(R R , G G ) M(R, G) + M(R , G );

SEPARABILITY: (R R , G G ) RPSIMAAL\ , if PLit(R G) PLit(R G ) = then M(R R , G G ) = M(R, G) + M(R , G ).

These properties can be used for emphasizing differences between incompleteness measures. They are not required in Definition 2 because it may be unsuitable in certain cases. For example, the basic measure Mb does not satisfy them. SUBADDITIVITY decrees that the incompleteness value for the result of joining available resources and goals is less than or equal to the sum of the incompleteness values for the available resources and goals considered separately. It is motivated by the fact that joining the available resources may provide additional possibilities compared to the case where they are taken independently. SEPARABILITY requires that if it is possible to partition the available resources and goals in two parts that do not share any literal, then the incompleteness value is the sum of the incompleteness values of the two parts. Alternatively stated, joining two multisets of available resources and goals that have nothing in common cannot provide any further possibility. We now show that SUBADDITIVITY is stronger than EXTENSION.

Proposition 2. If an incompleteness measure satisfies SUBADDITIVITY then it satisfies also EXTENSION.

Proof. Let M be an incompleteness measure, S = (R, G) RPSIMAAL\ and φ FIMAAL\ . Using SUB-

ADDITIVITY, we have M(R {φ}, G {φ}) M(S) + M({φ}, {φ}). Thus, M(R {φ}, G {φ}) M(R, G) holds.

The decomposition of RP-scenarios in the same way as in SEPARABILITY deserves much attention. Indeed, certain decomposition-based properties may seem intuitively appropriate while they are not satisfied by any incompleteness measure. To clarify this point, consider the following property:

MULTIPLICITY: (R, G) RPSIMAAL\ , M(R R, G G) = 2 M(R, G).

Even if MULTIPLICITY might seem intuitively suitable in some cases, we formally show in the following proposition that it cannot be satisfied by any measure.

Proposition 3. There is no incompleteness measure that satisfies MULTIPLICITY.

Proof. Let M be an incompleteness measure and S = ({p, p p q q, p, p p q q}, {2 : q}) an RPscenario. Clearly, we have {p, p p q q, p, p p q q} q q. Consequently, using COMPLETENESS, we obtain M(S) = 0. Assume that M satisfies MULTIPLICITY. Then, we have M(S) = 2 M({p, p p q q}, {q}). Using COMPLETENESS, M({p, p p q q}, {q}) > 0 holds, since {p, p p q q} q. Therefore, we have also M(S) > 0 and we obtain a contradiction.

Syntactic Incompleteness Measures

In this section, we propose notions that are useful for defining syntactic incompleteness measures and describe several measures that are based on them. Intuitively, these notions can be exploited in a similar way to maximal consistent subsets and minimal inconsistent subsets for defining inconsistency measures in the case of classical logic (e.g. see (Thimm 2018b)).

Definition 3 (Maximal Produced Sub-multiset). Let S = (R, G) be an RP-scenario. A multiset G of formulas in FIMAAL\ is a maximal produced sub-multiset (MPS) of S iff (i) G G, (ii) R N G , and (iii) G G with G G , R N G .

We use MPS(S) to denote the set of all the MPSes of S. An MPS can be seen as a possible optimal solution of the resource production problem, since it is obtained by maximizing the satisfied part in the desired goal (the maximality is considered with respect to multiset inclusion). In a sense, the notion of MPS can be seen as the counterpart of that of maximal consistent subset in classical logic. In order to show that MPSes can be used for quantifying and reasoning about incompleteness, consider the following incompleteness measures: for every S = (R, G) RPSIMAAL\ ,

MMP S max (S) = |G| max{|G | : G MPS(S)},

MMP S cov (S) = min{|Γ| 1 : Γ mult(MPS(S)) and G U Γ} with MMP S cov (S) = if Γ mult(MPS(S)), G U Γ holds.

Following MMP S max , the amount of incompleteness corresponds to the minimum number of resources that cannot be produced. This measure corresponds, probably, to the most intuitive and direct manner for quantifying incompleteness. Indeed, in many cases involving resource production, the aim consists in maximizing the quantity of acquired resources. The measure MMP S cov counts the minimum number of MPSes that cover the desired goal. Intuitively, it corresponds to the repeated effort needed to achieve the goal. We use for the case where it is not possible to cover the entire resources.

Proposition 4. The functions MMP S max and MMP S cov are incompleteness measures that satisfy SUBADDITIVITY and SEPARABILITY.

Proof. We only consider the case of MMP S max , the case of MMP S cov being similar. - COMPLETENESS. S = (R, G) RPSIMAAL\ , we have MMP S max (S) = 0 iff MPS(S) = {G}. Thus, MMP S max (S) = 0 iff R N G. - GOAL ADDITION. Let S = (R, G) RPSIMAAL\ , φ Res and G MPS(R, G {φ}) s.t. MMP S max (R, G {φ}) = |G {φ}| |G |. Clearly, there exists an MPS G MPS(S) s.t. G \ {φ} G . Hence, |G {φ}| |G | |G| |G | holds. As a consequence, we have M(R, G {φ}) M(R, G). - SUBADDITIVITY. Let (R R , G G ) RPSIMAAL\ . For every MPS G1 MPS(R, G) and every G2 MPS(R , G ), there exists an MPS G3 MPS(R R , G G ) s.t. G1 G2 G3. Indeed, we have R R N(G1 G2) since R N G1 and R N G2. Therefore, M(R R , G G ) M(R, G) + M(R , G ) holds. - EXTENSION. A consequence of Proposition 2. - SEPARABILITY. Let (R R , G G ) RPSIMAAL\ s.t. PLit(R G) PLit(R G ) = . Thus, for every G1 G, R R N G1 iff R N G1. Similarly, for every G2 G , R R N G2 iff R N G2. Hence, for every G3 MPS(R R , G G ), G3 \ G MPS(R, G) and G3 \ G MPS(R , G ). Consequently, we obtain M(R R , G G ) = M(R, G) + M(R , G ).

We now use the notion of MPS to define an additional notion that can be used for defining properties on incompleteness measures.

Definition 4 (Assured Subgoal). Given an RP-scenario S = (R, G), the assured subgoal of S is the intersection of all the MPSes of S, i.e., T MPS(S).

We use AS(S) to denote the assured subgoal of S. In other words, the assured subgoal is the part of the desired resources that is in every solution obtained by maximizing the produced resources (w.r.t. multiset inclusion). To some extent, the assured subgoal can be considered as the part of the goal that is not involved in the causes of incompleteness. This property can be expressed as follows:

ASSURED SUBGOAL: (R, G) RPSIMAAL\ , M(R, G) = M(R, G \ AS(R, G)).

Proposition 5. The incompleteness measures MMP S max and MMP S cov satisfy ASSURED SUBGOAL.

Proof. Let S = (R, G) RPSIMAAL\ . - Case of MMP S max . Let G MPS(R, G \ AS(S)) s.t. MMP S max (R, G \ AS(S)) = |G \ AS(S)| |G |. Assume that R N(G AS(R, G)). Then, there exists an MPS of S s.t. AS(S) MPS(S) (that including G ), and we obtain a contradiction with the definition of assured subgoal. Thus, R N(G AS(S)) holds, and we obtain MMP S max (R, G \ AS(S)) MMP S max (S). In addition, using Proposition 1, MMP S max (R, G\AS(S)) MMP S max (S) holds.

- Case of MMP S cov . If MMP S cov (R, G \ AS(S)) = then MMP S cov (R, G) = holds since MMP S cov (R, G \ AS(S)) MMP S cov (S) (see Proposition 1). Otherwise, let Γ mult(MPS(R, G \ AS(S))) s.t. G U Γ and MMP S cov (R, G \ AS(S)) = |Γ|. Using the definition of assured subgoal, it holds R N(G AS(S)) for every G MPS(R, G \ AS(S)) (see the proof in the case of MMP S max ). As a consequence, we obtain MMP S cov (R, G) |Γ|. Furthermore, MMP S cov (R, G) |Γ| is obtained using Proposition 1.

In the following definition, we introduce a notion defined through adding positive literals, which are the building blocks of any formula, to the available resources to reach the goal.

Definition 5 (MAM). Let S = (R, G) be an RP-scenario. A minimal adjustment multiset (MAM) of S is a multiset X of positive literals where (i) R X N G and (ii) for every multiset of positive literals Y with Y X, R Y N G.

We use MAM(S) to denote the set of all the MAMs of S. Alternatively stated, a MAM corresponds to what is needed in terms of building blocks of resources (positive literals) to attain the considered goal. The following proposition shows that there exists a multiset of positive literals that allows having completeness for every RP-scenario.

Proposition 6. For every S = (R, G) RPSIMAAL\ , there exists a finite multiset X of positive literals s.t. R X N G.

Proof. We consider w.l.o.g. that G contains a single formula φ. Our proof is by induction of the size of φ (the number of symbols occurring in φ). If φ is a positive literal then the property is obtained with X = {φ}: R {φ} φ. We now consider only the case where φ corresponds to a formula of the form φ1 φ2, the other cases begin similar. Using induction hypothesis, we know that there exist finite multisets X1 and X2 of positive literals s.t. R X1 φ1 and R X2 φ2. Then, using the weakening rule, we obtain both R X1 X2 φ1 and R X X2 φ2. By applying the rule [ R], R X1 X2 φ1 φ2 holds.

Let us consider the following incompleteness measures: for every S RPSIMAAL\ ,

MMAM min (S) = min{|X| : X MAM(S)}

MMAM min,set(S) = min{|set(X)| : X MAM(S)}.

The amount of incompleteness using MMAM min is equal to the minimum number of positive literal occurrences that are needed with the available resources to obtain the entire goal. The measure MMAM min,set(S) is defined in the same way as the previous one, except that it takes into account the number of distinct positive literals instead of the number of occurrences.

Proposition 7. The functions MMAM min and MMAM min,set are incompleteness measures that satisfy SUBADDITIVITY and SEPARABILITY.

Contrary to the MPS-based measures, MMAM min and MMAM min,set do not satisfy ASSURED SUBGOAL. For instance, consider the RP-scenario S = ({p (p 3 : q)}, {p, 3 : q}), which has a single MPS: {p}; hence, we have AS(S) = {p}. Additionally, {p} is also the smallest MAM of S = (R, G \ {p}), and consequently MMAM min (S ) = 1 holds. However, the multiset {2 : p} is the unique smallest MAM of S, and we obtain MMAM min (S) = 2. Note that interesting measures can also be obtained without involving the previous notions. For example, consider the following measure: for every S = (R, G) RPSIMAAL\ ,

Mnc(S) = |G| max{k : G G, if |G | = k then R N G }.

This measure is inspired by the inconsistency measure introduced in (Doder et al. 2010) (see also (Thimm 2016)). The value v = max{k : G G, if |G | = k then R N G } corresponds to the maximum value v so that any part from the goal of size v can be obtained from the available resources. The function Mnc is an incompleteness measure that satisfies SUBADDITIVITY and SEPARABILITY. This measure shows also that some concepts used in defining inconsistency measures can be adapted to define incompleteness measures.

Example 2. Consider R = {p, (2 : p) p q, r, r (2 : s), s (2 : s), t (2 : t)} and G = {p, q, r, 2 : s, 2 : t}. There are only two MPSes: G1 = {p, r} and G2 = {p, 2 : s}. Thus, we have MMP S max (R, G) = 4. Furthermore, there is no combination of G1 and G2 that can cover the entire goal; hence, MMP S max (R, G) = holds. In addition, using the fact that the MAMs are {p, r, t}, {q, r, t}, {p, s, t}, and {q, s, t}, we obtain MMAM min (R, G) = MMAM min,set(R, G) = 3. Moreover, we have max{k : G G, if |G | = k then R N G } = 0, which means that Mnc(R, G) = 7.

Conclusion and Perspectives The ability to reason about resource production incompleteness is a key point to make rational decisions in many contexts. In this paper, using intuitionistic affine logic for resource representation and reasoning, we have introduced a logic-based framework for quantifying the intensity of resource production incompleteness through a postulate-based approach. Additionally, we have proposed syntactic notions that can be used to build different types of measures and presented several measures based on them. Besides, we have described situations where incompleteness measures can be applied. There are several perspectives for future work related to the measurement of resource production incompleteness. Indeed, it is interesting to adapt the proposed framework to other resource-sensitive logics such as the logic of bunched implications (O Hearn and Pym 1999). Additionally, it is worthwhile to study further properties on the incompleteness measures that correspond to aspects related to resource management (e.g. the presence of infinite resources). The definition of other types of incompleteness measures is as well an interesting perspective.

Bona, G. D.; Grant, J.; Hunter, A.; and Konieczny, S. 2018. Towards a Unified Framework for Syntactic Inconsistency Measures. In Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, New Orleans, Louisiana, USA.

Bugliesi, M.; Calzavara, S.; Eigner, F.; and Maffei, M. 2013. Logical Foundations of Secure Resource Management in Protocol Implementations. In Principles of Security and Trust - Second International Conference, POST 2013, Rome, Italy, volume 7796 of Lecture Notes in Computer Science, 105 125. Springer.

Doder, D.; Raskovic, M.; Markovic, Z.; and Ognjanovic, Z. 2010. Measures of inconsistency and defaults. Int. J. Approx. Reason. 51(7): 832 845.

Engberg, U.; and Winskel, G. 1990. Petri Nets as Models of Linear Logic. In Arnold, A., ed., CAAP 90, 15th Colloquium on Trees in Algebra and Programming, Copenhagen, Denmark, Proceedings, volume 431 of Lecture Notes in Computer Science, 147 161. Springer.

Engberg, U.; and Winskel, G. 1993. Linear Logic on Petri Nets. In de Bakker, J. W.; de Roever, W. P.; and Rozenberg, G., eds., A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium, Noordwijkerhout, The Netherlands, Proceedings, volume 803 of Lecture Notes in Computer Science, 176 229. Springer.

Ferm uller, C. G.; and Lang, T. 2017. Interpreting Sequent Calculi as Client-Server Games. In Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Bras ılia, Brazil, volume 10501 of Lecture Notes in Computer Science, 98 113. Springer.

Girard, J.-Y. 1987. Linear Logic. Theoretical Computer Science 50: 1 102.

Girard, J.-Y.; and Lafont, Y. 1987. Linear Logic and Lazy Computation. In TAPSOFT 87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, Volume 2., volume 250 of Lecture Notes in Computer Science, 52 66. Springer.

Hunter, A.; and Konieczny, S. 2010. On the measure of conflicts: Shapley Inconsistency Values. Artificial Intelligence 174(14): 1007 1026.

Kamide, N. 2006. Linear and affine logics with temporal, spatial and epistemic operators. Theoretical Computer Science 353(1-3): 165 207.

Kanovich, M. I. 1992. Horn Programming in Linear Logic Is NP-Complete. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS 92), Santa Cruz, California, USA, 200 210. IEEE Computer Society.

Kanovich, M. I.; and Vauzeilles, J. 2001. The classical AI planning problems in the mirror of Horn linear logic: semantics, expressibility, complexity. Mathematical Structures in Computer Science 11(6): 689 716.

Kanovich, M. I.; and Vauzeilles, J. 2011. Linear logic as a tool for planning under temporal uncertainty. Theoretical Computer Science 412(20): 2072 2092. O Hearn, P. W.; and Pym, D. J. 1999. The logic of bunched implications. Bulletin of Symbolic Logic 5(2): 215 244. Paoli, F. 2002. Substructural Logics: A Primer. Trends in Logic. Springer Netherlands. Porello, D.; and Endriss, U. 2010. Modelling Combinatorial Auctions in Linear Logic. In Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference, KR 2010, Toronto, Ontario, Canada. AAAI Press. Restall, G. 2000. An Introduction to Substructural Logics. Routledge. Thimm, M. 2016. On the expressivity of inconsistency measures. Artificial Intelligence 234: 120 151. Thimm, M. 2018a. On the Evaluation of Inconsistency Measures. In Grant, J.; and Martinez, M. V., eds., Measuring Inconsistency in Information, volume 73 of Studies in Logic. College Publications. Thimm, M. 2018b. On the Evaluation of Inconsistency Measures. In Measuring Inconsistency in Information, volume 73 of Studies in Logic. College Publications. Troelstra, A. 1992. Lectures on Linear Logic. Center for the Study of Language and Information Publication Lecture Notes. Cambridge University Press. Troelstra, A. S.; and Schwichtenberg, H. 1996. Basic Proof Theory. USA: Cambridge University Press.