Concept Bottleneck Models (CBMs) predict through human-interpretable concepts, but they typically output point concept probabilities that conflate epistemic uncertainty (reducible model underspecification) with aleatoric uncertainty (irreducible input ambiguity).This makes concept-level uncertainty hard to interpret and, more importantly, hard to act upon.We introduce CREDENCE (Credal Ensemble Concept Estimation), a CBM framework that decomposes concept uncertainty by construction.CREDENCE represents each concept as a credal prediction (a probability interval), derives epistemic uncertainty from disagreement across diverse concept heads, and estimates aleatoric uncertainty via a dedicated ambiguity output trained to match annotator disagreement when available.The resulting signals support prescriptive decisions: automate low-uncertainty cases, prioritize data collection for high-epistemic cases, route high-aleatoric cases to human review, and abstain when both are high.Across several tasks, we show that epistemic uncertainty is positively associated with prediction errors, whereas aleatoric uncertainty closely tracks annotator disagreement, providing guidance beyond error correlation.Our implementation is available at the following link: https://github.com/Tankiit/ Credal_Sets/tree/ensemble-credal-cbm

International audience

In this work, we show how the class of improvement operators --- a general class of iterated belief change operators --- can be used to define a learning model. Focusing on binary classification, we present learning and inference algorithms suited to this learning model and we evaluate them empirically. Our findings highlight two key insights: first, that iterated belief change can be viewed as an effective form of online learning, and second, that the well-established axiomatic foundations of belief change operators offer a promising avenue for the axiomatic study of classification tasks.

This paper presents BeliefFlow, a novel framework for representing how logical beliefs spread among interacting agents within a network. In a Belief Flow Network (BFN), agents communicate asynchronously. The agents' beliefs are represented using epistemic states, which encompass their current beliefs and conditional beliefs guiding future changes. When communication occurs between two connected agents, the receiving agent changes its epistemic state using an improvement operator, a well-known type of rational iterated belief change operator that generalizes belief revision operators. We show that BFNs satisfy appealing properties, leading to two significant outcomes. First, in any BFN with strong network connectivity, the beliefs of all agents converge towards a global consensus. Second, within any BFN, we show that it is possible to compute an optimal strategy for influencing the global beliefs. This strategy, which involves controlling the beliefs of a least number of agents through bribery, can be identified from the topology of the network and can be computed in polynomial time.

We present and evaluate empirically an XAI protocol for ruling interactions between a tree-based ML model (the AI system) and its user U, in the context of a prediction task. The pieces of knowledge held by U concerning the prediction task are supposed to be representable by a set of classification rules that is reliable and consistent, but (typically) incomplete. The proposed protocol aims to help U decide what to do with each prediction made by AI (accept it, reject it). It also aims to improve the quality of further predictions made by AI thanks to the expertise of U, and, reciprocally, to complete the pieces of knowledge held by U by leveraging the predictions made by AI. Experiments show that the approach can prove valuable in practice.

A contrastive explanation is a local explanation that is looked for when the prediction achieved by an ML model on an input instance x differs from what was foreseen. A contrastive explanation indicates how to change x to another instance xc from which a prediction that complies with the user’s expectations can be obtained. In this paper, we present a constraint-based approach to the generation of contrastive explanations that are suited to regression functions represented by boosted trees. We show how to compute the smallest interval containing all the regression values that are attainable given a set of characteristics of x that are protected (i.e., not amenable to change). We also show how to generate minimal contrastive explanations for x given a target interval, i.e., instances with regression values within the specified interval and that are as close as possible to x. Closeness is captured using user-dependent mappings reflecting preferences about value change for the attributes (or combinations of attributes) considered in the representation of x.

In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ‖∃ X . Σ‖ of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.

This paper is about editing Boolean classifiers, i.e., determining how a Boolean classifier should be modified when new pieces of evidence must be incorporated. Our main goal is to delineate what are the rational ways of making such edits. This goes through a number of rationality postulates inspired from those considered so far for belief revision. We give a representation theorem and present some families of edit operators satisfying the postulates.

Boosted trees is a dominant ML model, exhibiting high accuracy. However, boosted trees are hardly intelligible, and this is a problem whenever they are used in safety-critical applications. Indeed, in such a context, provably sound explanations for the predictions made are expected. Recent work have shown how subset-minimal abductive explanations can be derived for boosted trees, using automated reasoning techniques. However, the generation of such well-founded explanations is intractable in the general case. To improve the scalability of their generation, we introduce the notion of tree-specific explanation for a boosted tree. We show that tree-specific explanations are provably sound abductive explanations that can be computed in polynomial time. We also explain how to derive a subset-minimal abductive explanation from a tree-specific explanation. Experiments on various datasets show the computational benefits of leveraging tree-specific explanations for deriving subset-minimal abductive explanations.

We define contrastive explanations that are suited to tree-based classifiers. In our framework, contrastive explanations are based on the set of (possibly non-independent) Boolean characteristics used by the classifier and are at least as general as contrastive explanations based on the set of characteristics of the instances considered at start. We investigate the computational complexity of computing contrastive explanations for Boolean classifiers (including tree-based ones), when the Boolean conditions used are not independent. Finally, we present and evaluate empirically an algorithm for computing minimum-size contrastive explanations for random forests.

We elaborate on the notion of rectification of a classifier Σ based on Boolean features, introduced in [10]. The purpose is to determine how to modify Σ when the way it classifies a given instance is considered incorrect since it conflicts with some expert knowledge T. Given Σ and T, postulates characterizing the way Σ must be changed into a new classifier Σ ⋆ T that complies with T were presented. We focus here on the specific case of binary classifiers, i.e., there is a single target concept, and any instance is classified either as positive (an element of the concept), or as negative (an element of the complementary concept). In this specific case, our main contribution is twofold: (1) we show that there is a unique rectification operator ⋆ satisfying the postulates, and (2) when Σ and T are Boolean circuits, we show how a classification circuit equivalent to Σ ⋆ T can be computed in time linear in the size of Σ and T; when Σ is a decision tree (resp. a random forest, a boosted tree) and T is a decision tree, a decision tree (resp. a random forest, a boosted tree) equivalent to Σ ⋆ T can be computed in time polynomial in the size of Σ and T.

We present two algorithms for generating (resp. evaluating) abductive explanations for boosted regression trees. Given an instance x and an interval I containing its value F (x) for the boosted regression tree F at hand, the generation algorithm returns a (most general) term t over the Boolean conditions in F such that every instance x′ satisfying t is such that F (x′ ) ∈ I. The evaluation algorithm tackles the corresponding inverse problem: given F , x and a term t over the Boolean conditions in F such that t covers x, find the least interval I_t such that for every instance x′ covered by t we have F (x′ ) ∈ I_t . Experiments on various datasets show that the two algorithms are practical enough to be used for generating (resp. evaluating) abductive explanations for boosted regression trees based on a large number of Boolean conditions.

In this paper, the succinctness of various ML models is studied. To be more precise, the existence of polynomial-time and polynomial-space translations between representation languages for classifiers is investigated. The languages that are considered include decision trees, random forests, several types of boosted trees, binary neural networks, Boolean multilayer perceptrons, and various logical representations of binary classifiers. We provide a complete map indicating for every pair of languages C, C' whether or not a polynomial-time / polynomial-space translation exists from C to C'. We also explain how to take advantage of the resulting map for XAI purposes.

Random forests have long been considered as powerful model ensembles in machine learning. By training multiple decision trees, whose diversity is fostered through data and feature subsampling, the resulting random forest can lead to more stable and reliable predictions than a single decision tree. This however comes at the cost of decreased interpretability: while decision trees are often easily interpretable, the predictions made by random forests are much more difficult to understand, as they involve a majority vote over multiple decision trees. In this paper, we examine different types of reasons that explain "why" an input instance is classified as positive or negative by a Boolean random forest. Notably, as an alternative to prime-implicant explanations taking the form of subset-minimal implicants of the random forest, we introduce majoritary reasons which are subset-minimal implicants of a strict majority of decision trees. For these abductive explanations, the tractability of the generation problem (finding one reason) and the optimization problem (finding one minimum-sized reason) are investigated. Unlike prime-implicant explanations, majoritary reasons may contain redundant features. However, in practice, prime-implicant explanations - for which the identification problem is DP-complete - are slightly larger than majoritary reasons that can be generated using a simple linear-time greedy algorithm. They are also significantly larger than minimum-sized majoritary reasons which can be approached using an anytime Partial MaxSAT algorithm.

Abductive explanations take a central place in eXplainable Artificial Intelligence (XAI) by clarifying with few features the way data instances are classified. However, instances may have exponentially many minimum-size abductive explanations, and this source of complexity holds even for ``intelligible'' classifiers, such as decision trees. When the number of such abductive explanations is huge, computing one of them, only, is often not informative enough. Especially, better explanations than the one that is derived may exist. As a way to circumvent this issue, we propose to leverage a model of the explainee, making precise her / his preferences about explanations, and to compute only preferred explanations. In this paper, several models are pointed out and discussed. For each model, we present and evaluate an algorithm for computing preferred majoritary reasons, where majoritary reasons are specific abductive explanations suited to random forests. We show that in practice the preferred majoritary reasons for an instance can be far less numerous than its majoritary reasons.

We consider the problem Enum·IP of enumerating prime implicants of Boolean functions represented by decision decomposable negation normal form (dec-DNNF) circuits. We study Enum·IP from dec-DNNF within the framework of enumeration complexity and prove that it is in OutputP, the class of output polynomial enumeration problems, and more precisely in IncP, the class of polynomial incremental time enumeration problems. We then focus on two closely related, but seemingly harder, enumeration problems where further restrictions are put on the prime implicants to be generated. In the first problem, one is only interested in prime implicants representing subset-minimal abductive explanations, a notion much investigated in AI for more than thirty years. In the second problem, the target is prime implicants representing sufficient reasons, a recent yet important notion in the emerging field of eXplainable AI, since they aim to explain predictions achieved by machine learning classifiers. We provide evidence showing that enumerating specific prime implicants corresponding to subset-minimal abductive explanations or to sufficient reasons is not in OutputP.

Quantified Boolean logic results from adding operators to Boolean logic for existentially and universally quantifying variables. This extends the reach of Boolean logic by enabling a variety of applications that have been explored over the decades. The existential quantification of literals (variable states) and its applications have also been studied in the literature. We complement this by studying universal literal quantification and its applications, particularly to explainable AI. We also provide a novel semantics for quantification and discuss the interplay between variable/literal and existential/universal quantification. We further identify classes of Boolean formulas and circuits that allow efficient quantification. Literal quantification is more fine-grained than variable quantification, which leads to a refinement of quantified Boolean logic with literal quantification as its primitive.

Certifying the output of tools solving complex problems so as to ensure the correctness of the results they provide is of tremendous importance. Despite being widespread for SAT-solvers, this level of exigence has not yet percolated for tools solving more complex tasks, such as model counting or knowledge compilation. In this paper, the focus is laid on a general family of top-down Decision-DNNF compilers. We explain how those compilers can be tweaked so as to output certifiable Decision-DNNF circuits, which are mainly standard Decision-DNNF circuits decorated by annotations serving as certificates. We describe a polynomial-time checker for testing whether a given CNF formula is equivalent or not to a given certifiable Decision-DNNF circuit. Finally, leveraging a modified version of the compiler d4 for generating certifiable Decision-DNNF circuits and an implementation of the checker, we present the results of an empirical evaluation that has been conducted for assessing how large are in practice certifiable Decision-DNNF circuits, and how much time is needed to compute and to check such circuits.

An important issue in ML consists in developing approaches exploiting background knowledge T for improving the accuracy and the robustness of learned classifiers C. Delegating the classification task to a Boolean circuit Σ exhibiting the same input-output behaviour as C, the problem of exploiting T within C can be viewed as a belief change scenario. However, usual change operations are not suited to the task of modifying the classifier encoding Σ in a minimal way, to make it complying with T. To fill the gap, we present a new belief change operation, called rectification. We characterize the family of rectification operators from an axiomatic perspective and exhibit operators from this family. We identify the standard belief change postulates that every rectification operator satisfies and those it does not. We also focus on some computational aspects of rectification and compliance.

In this paper, we investigate the computational intelligibility of Boolean classifiers, characterized by their ability to answer XAI queries in polynomial time. The classifiers under consideration are decision trees, DNF formulae, decision lists, decision rules, tree ensembles, and Boolean neural nets. Using 9 XAI queries, including both explanation queries and verification queries, we show the existence of large intelligibility gap between the families of classifiers. On the one hand, all the 9 XAI queries are tractable for decision trees. On the other hand, none of them is tractable for DNF formulae, decision lists, random forests, boosted decision trees, Boolean multilayer perceptrons, and binarized neural networks.

Quantified Boolean logic results from adding operators to Boolean logic for existentially and universally quantifying variables. This extends the reach of Boolean logic by enabling a variety of applications that have been explored over the decades. The existential quantification of literals (variable states) and its applications have also been studied in the literature. In this paper, we complement this by introducing and studying universal literal quantification and its applications, particularly to explainable AI. We also provide a novel semantics for quantification, discuss the interplay between variable/literal and existential/universal quantification, and identify some classes of Boolean formulas and circuits on which quantification can be done efficiently. Literal quantification is more fine-grained than variable quantification as the latter can be defined in terms of the former, leading to a refinement of quantified Boolean logic with literal quantification as its primitive.

Learning pseudo-Boolean (PB) constraints in PB solvers exploiting cutting planes based inference is not as well understood as clause learning in conflict-driven clause learning solvers. In this paper, we show that PB constraints derived using cutting planes may contain irrelevant literals, i.e., literals whose assigned values (whatever they are) never change the truth value of the constraint. Such literals may lead to infer constraints that are weaker than they should be, impacting the size of the proof built by the solver, and thus also affecting its performance. This suggests that current implementations of PB solvers based on cutting planes should be reconsidered to prevent the generation of irrelevant literals. Indeed, detecting and removing irrelevant literals is too expensive in practice to be considered as an option (the associated problem is NP-hard).

We study how belief merging operators can be considered as maximum likelihood estimators, i.e., we assume that there exists a (unknown) true state of the world and that each agent participating in the merging process receives a noisy signal of it, characterized by a noise model. The objective is then to aggregate the agents' belief bases to make the best possible guess about the true state of the world. In this paper, some logical connections between the rationality postulates for belief merging (IC postulates) and simple conditions over the noise model under consideration are exhibited. These results provide a new justification for IC merging postulates. We also provide results for two specific natural noise models: the world swap noise and the atom swap noise, by identifying distance-based merging operators that are maximum likelihood estimators for these two noise models.

Iterated belief change aims to determine how the belief state of a rational agent evolves given a sequence of change formulae. Several families of iterated belief change operators (revision operators, improvement operators) have been pointed out so far, and characterized from an axiomatic point of view. This paper focuses on the inference problem for iterated belief change, when belief states are represented as a special kind of stratified belief bases. The computational complexity of the inference problem is identified and shown to be identical for all revision operators satisfying Darwiche and Pearl's (R*1-R*6) postulates. In addition, some complexity bounds for the inference problem are provided for the family of soft improvement operators. We also show that a revised belief state can be computed in a reasonable time for large-sized instances using SAT-based algorithms, and we report empirical results showing the feasibility of iterated belief change for bases of significant sizes.

One of the key purposes of eXplainable AI (XAI) is to develop techniques for understanding predictions made by Machine Learning (ML) models and for assessing how much reliable they are. Several encoding schemas have recently been pointed out, showing how ML classifiers of various types can be mapped to Boolean circuits exhibiting the same input-output behaviours. Thanks to such mappings, XAI queries about classifiers can be delegated to the corresponding circuits. In this paper, we define new explanation and/or verification queries about classifiers. We show how they can be addressed by combining queries and transformations about the associated Boolean circuits. Taking advantage of previous results from the knowledge compilation map, this allows us to identify a number of XAI queries that are tractable provided that the circuit has been first turned into a compiled representation.

We present a recursive algorithm for projected model counting, i.e., the problem consisting in determining the number of models k∃X.Σk of a propositional formula Σ after eliminating from it a given set X of variables. Based on a ”standard” model counter, our algorithm projMC takes advantage of a disjunctive decomposition scheme of ∃X.Σ for computing k∃X.Σk. It also looks for disjoint components in its input for improving the computation. Our experiments show that in many cases projMC is significantly more efficient than the previous algorithms for projected model counting from the literature.

When one wants to draw non-trivial inferences from an inconsistent belief base, a very natural approach is to take advantage of the maximal consistent subsets of the base. But few inference relations from maximal consistent subsets exist. In this paper we point out new such relations based on selection of some of the maximal consistent subsets, leading thus to inference relations with a stronger inferential power. The selection process must obey some principles to ensure that it leads to an inference relation which is rational. We define a general class of monotonic selection relations for comparing maximal consistent sets. And we show that it corresponds to the class of rational inference relations.

We consider the problem of identifying the change formula in a belief revision scenario: given that an unknown announcement (a formula mu) led a set of agents to revise their beliefs and given the prior beliefs and the revised beliefs of the agents, what can be said about mu? We show that under weak conditions about the rationality of the revision operators used by the agents, the set of candidate formulae has the form of a logical interval. We explain how the bounds of this interval can be tightened when the revision operators used by the agents are known and/or when mu is known to be independent from a given set of variables. We also investigate the completeness issue, i.e., whether mu can be exactly identified. We present some sufficient conditions for it, identify its computational complexity, and report the results of some experiments about it.

We define a consensus postulate in the propositional belief merging setting. In a nutshell, this postulate imposes the merged base to be consistent with the pieces of information provided by each agent involved in the merging process. The interplay of this new postulate with the IC postulates for belief merging is studied, and an incompatibility result is proved. The maximal sets of IC postulates which are consistent with the consensus postulate are exhibited. When satisfying some of the remaining IC postulates, consensus operators are shown to suffer from a weak inferential power. We then introduce two families of consensus operators having a better inferential power by setting aside some of these postulates.

We study pseudo-Boolean constraints (PBC) and their special case cardinality constraints (CARD) from the perspective of knowledge representation. To this end, the succinctness of PBC and CARD is compared to that of many standard propositional languages. Moreover, we determine which queries and transformations are feasible in polynomial time when knowledge is represented by PBC or CARD, and which are not (unconditionally or unless P = NP). In particular, the advantages and disadvantages compared to CNF are discussed.

We present and evaluate DMC, a distributed model counter for propositional CNF formulae based on the state-of-the-art sequential model counter D4. DMC can take advantage of a (possibly large) number of sequential model counters running on (possibly heterogeneous) computing units spread over a network of computers. For ensuring an efficient workload distribution, the model counting task is shared between the model counters following a policy close to work stealing. The number and the sizes of the messages which are exchanged by the jobs are kept small. The results obtained show DMC as a much more efficient counter than D4, the distribution of the computation yielding large improvements for some benchmarks. DMC appears also as a serious challenger to the parallel model counter CountAntom and to the distributed model counter dCountAntom.

Existing belief merging operators take advantage of all the models from the bases, including those contradicting the integrity constraint. In this paper, we argue that this is not suited to every merging scenario, especially when the integrity constraint encodes physical laws. In that case the bases have to be ‘rationalized’ with respect to the integrity constraint during the merging process. We define several conditions characterizing the operators that are independent to such a rationalization process, and we show how these conditions interact with the standard IC postulates for belief merging. Especially, we give an independence-based axiomatic characterization of a distance-based operator.

We present SAT encoding schemes for distance-based belief merging operators relying on the (possibly weighted) drastic distance or the Hamming distance between interpretations, and using sum, GMax (leximax) or GMin (leximin) as aggregation function. In order to evaluate these encoding schemes, we generated benchmarks of a time-tabling problem and translated them into belief merging instances. Then, taking advantage of these schemes, we compiled the merged bases of the resulting instances into query-equivalent CNF formulae. Experiments have shown the benefits which can be gained by considering the SAT encoding schemes we pointed out. Especially, thanks to them, we succeeded in computing query-equivalent formulae for merging instances based on hundreds of variables, which are out of reach of previous implementations.

We present and evaluate a new compiler, called d4, targeting the Decision-DNNF language. As the state-of-the-art compilers C2D and Dsharp targeting the same language, d4 is a top-down tree-search algorithm exploring the space of propositional interpretations. d4 is based on the same ingredients as those considered in C2D and Dsharp (mainly, disjoint component analysis, conflict analysis and non-chronological backtracking, component caching). d4 takes advantage of a dynamic decomposition approach based on hypergraph partitioning, used sparingly. Some simplification rules are also used to minimize the time spent in the partitioning steps and to promote the quality of the decompositions. Experiments show that the compilation times and the sizes of the Decision-DNNF representations computed by d4 are in many cases significantly lower than the ones obtained by C2D and Dsharp.

We present and evaluate a new CNF encoding scheme for reducing probabilistic inference from a graphical model to weighted model counting. This new encoding scheme elaborates on the CNF encoding scheme ENC4 introduced by Chavira and Darwiche, and improves it by taking advantage of log encodings of the elementary variable/value assignments and of the implicit encoding of the most frequent probability value per conditional probability table. From the theory side, we show that our encoding scheme is faithful, and that for each input network, the CNF formula it leads to contains less variables and less clauses than the CNF formula obtained using ENC4. From the practical side, we show that the C2D compiler empowered by our encoding scheme performs in many cases significantly better than when ENC4 is used, or when the state-of-the-art ACE compiler is considered instead.

In this paper, some distances between KD45n Kripke models are introduced and investigated. We define several distances between Kripke models, based on different criteria, inspired by various concepts such as bisimulation and propositional distances between valuations for different modal degrees. We study the properties of these distances. Such distances are useful for defining belief change operators in multi-agent scenarios. We show that they can be used to define belief revision operators based on the standard AGM framework and suited to KD45n Kripke models.

This paper is concerned with knowledge compilation (KC), a family of approaches developed in AI for more than twenty years. Knowledge compilation consists in pre-processing some pieces of the available information in order to improve the computational efficiency (especially, the time complexity) of some tasks. In this paper, the focus is laid on three KC topics which gave rise to many works: the development of knowledge compilation techniques for the clausal entailment problem in propositional logic, the concept of compilability and the notion of knowledge compilation map. The three topics, as well as an overview of the main results from the literature, are presented. Some recent research lines are also discussed.

Belief revision games (BRGs) are concerned with the dynamics of the beliefs of a group of communicating agents. BRGs are "zero-player" games where at each step every agent revises her own beliefs by taking account for the beliefs of her acquaintances. Each agent is associated with a belief state defined on some finite propositional language. We provide a general definition for such games where each agent has her own revision policy, and show that the belief sequences of agents can always be finitely characterized. We then define a set of revision policies based on belief merging operators. We point out a set of appealing properties for BRGs and investigate the extent to which these properties are satisfied by the merging-based policies under consideration.

Valued decision diagrams (VDDs) are data structures that represent functions mapping variable-value assignments to non-negative real numbers. They prove useful to compile cost functions, utility functions, or probability distributions. While the complexity of some queries (notably optimization) and transformations (notably conditioning) on VDD languages has been known for some time, there remain many significant queries and transformations, such as the various kinds of cuts, marginalizations, and combinations, the complexity of which has not been identified so far. This paper contributes to filling this gap and completing previous results about the time and space efficiency of VDD languages, thus leading to a knowledge compilation map for real-valued functions. Our results show that many tasks that are hard on valued CSPs are actually tractable on VDDs.

This paper is concerned with preprocessing techniques for propositional model counting. We have implemented a preprocessor which includes many elementary preprocessing techniques, including occurrence reduction, vivification, backbone identification, as well as equivalence, AND and XOR gate identification and replacement. We performed intensive experiments, using a huge number of benchmarks coming from a large number of families. Two approaches to model counting have been considered downstream: ”direct” model counting using Cachet and compilation-based model counting, based on the C2D compiler. The experimental results we have obtained show that our preprocessor is both efficient and robust.

In this paper, symmetries are exploited for achieving significant space savings in a knowledge compilation perspective. More precisely, the languages FBDD and DDG of decision diagrams are extended to the languages Sym-FBDDX,Yand Sym-DDGX,Yof symmetry-driven decision diagrams, where X is a set of “symmetry-free” variables and Y is a set of “top” variables. Both the time efficiency and the space efficiency of Sym-FBDDX,Yand Sym-DDGX,Yare analyzed, in order to put those languages in the knowledge compilation map for propositional representations. It turns out that each of Sym-FBDDX,Yand Sym-DDGX,Ysatisfies CT (the model counting query). We prove that no propositional language over a set X∪Y of variables, satisfying both CO (the consistency query) and CD (the conditioning transformation), is at least as succinct as any of Sym-FBDDX,Yand Sym-DDGX,Yunless the polynomial hierarchy collapses. The price to be paid is that only a restricted form of conditioning and a restricted form of forgetting are offered by Sym-FBDDX,Yand Sym-DDGX,Y. Nevertheless, this proves sufficient for a number of applications, including configuration and planning. We describe a compiler targeting Sym-FBDDX,Yand Sym-DDGX,Yand give some experimental results on planning domains, highlighting the practical significance of these languages.

There are two theories of aggregation of logical formulae: merging and judgment aggregation. In this work we investigate the relationships between these theories; one of our objectives is to point out some correspondences/discrepancies between the associated rationality properties.

Artificial intelligence (AI) was not born ex nihilo in the mid-fifties of the XXthcentury. Beyond its immediate roots in cybernetics and in computer science that started about two decades before, its emergence is the result of a long and slow process in the history of humanity. This can be articulated around two main questions: the formalization of reasoning and the design of machines having autonomous capabilities in terms of computation and action. The aim of this paper is to gather some insufficiently known elements about the prehistory of AI in the last 350 years that precede the official birth of AI, a time period where only a few very well-known names, such as Thomas Bayes and Georges Boole, are usually mentioned in relation with AI.

We present and study a general family of belief update operators in a propositional setting. Its operators are based on formula/ literal dependence, which is more fine-grained than the notion of formula/ variable dependence that was proposed in the literature: formula/variable dependence is a particular case of formula/literal dependence. Our update operators are defined according to the “forget-then-conjoin” scheme: updating a belief base by an input formula consists in first forgetting in the base every literal on which the input formula has a negative influence, and then conjoining the resulting base with the input formula. The operators of our family differ by the underlying notion of formula/literal dependence, which may be defined syntactically or semantically, and which may or may not exploit further information like known persistent literals and pre-set dependencies. We argue that this allows to handle the frame problem and the ramification problem in a more appropriate way. We evaluate the update operators of our family w.r.t. two important dimensions: the logical dimension, by checking the status of the Katsuno-Mendelzon postulates for update, and the computational dimension, by identifying the complexity of a number of decision problems (including model checking, consistency and inference), both in the general case and in some restricted cases, as well as by studying compactability issues. It follows that several operators of our family are interesting alternatives to previous belief update operators.

Recently, Dunne et al. [9,10] introduced the concept of WAF (Weighted Argumentation Framework). Such frameworks extend standard Dung's ones for abstract argumentation by associating weights with attacks. In the WAF setting, weights are used for relaxing extensions, which proves useful when there are too few extensions. In this paper, we exploit weights in a different perspective. We show how to take advantage of attacks weights within an argumentation process for selecting some extensions among Dung's ones, which proves useful when there are too many extensions, in order to improve the inferential power of the argumentation framework.

Argument aggregation is the problem of combining argumentation frameworks. An argument aggregation procedure takes as input an argument framework for each agent in a system, intuitively representing the beliefs of that agent with respect to a disputed domain of discourse; the output is an argumentation framework that represents the social position on the domain of discourse. There are clear analogies between argument aggregation and the well-known preference aggregation problem, which has been extensively studied in the social choice community. The first contribution of this paper is to apply some of the methodology developed in social choice theory to argument aggregation. After recalling the basic framework of Dung's abstract argument systems, and introducing the argument aggregation problem, we motivate and formally define a collection of axioms that specific argument aggregation procedures might or might not satisfy. The second contribution of the paper is to consider the analysis of argument aggregation procedures with respect to these various axioms. We consider a natural representation for argument aggregation procedures, based on Boolean circuits. We then investigate the problem of verifying whether an argument aggregation procedure, presented in this way, does or does not satisfy a number of the axioms we introduced.

In this paper, we study the knowledge compilation task for propositional epistemic logic S5. We first extend many of the queries and transformations considered in the classical knowledge compilation map to S5. We then show that the notion of disjunctive normal form (DNF) can be profitably extended to the epistemic case; we prove that the DNF fragment of S5, when appropriately defined, satisfies essentially the same queries and transformations as its classical counterpart.

This paper is centered on the problem of merging (possibly conflicting) information coming from different sources. Though this problem has attracted much attention in propositional settings, propositional languages remain typically not expressive enough for a number of applications, especially when spatial information must be dealt with. In order to fill the gap, we consider a (limited) first-order logical setting, expressive enough for representing and reasoning about information modeled as half-spaces from metric affine spaces. In this setting, we define a family of distance-based majority merging operators which includes the propositional majority operator ΔdH,Σ. We identify a subclass of interpretations of our representation language for which the result of the merging process can be computed and expressed as a formula.

Belief merging is often described as the process of defining a base which best represents the beliefs of a group of agents (a profile of belief bases). The resulting base can be viewed as a synthesis of the input profile. In this paper another view of what belief merging aims at is considered: the epistemic view. Under this view the purpose of belief merging is to best approximate the true state of the world. We point out a generalization of Condorcet's Jury Theorem from the belief merging perspective. Roughly, we show that if the beliefs of sufficiently many reliable agents are merged then in the limit the true state of the world is identified. We introduce a new postulate suited to the truth tracking issue. We identify some merging operators from the literature which satisfy it and other operators which do not.

We address the problem of merging qualitative constraints networks (QCNs). We point out a merging algorithm which computes a consistent QCN representing a global view of the input set of (possibly conflicting) QCNs. This algorithm is generic in the sense that it does not depend on a specific qualitative formalism. The efficiency of our method comes from the fact that it merges locally the constraints of the input QCNs bearing on the same pairs of variables. We define several constraint merging operators in a way to ensure that the induced QCNs merging operator satisfies some expected properties from a logical standpoint.

In the propositional setting, a well-studied family of merging operators are distance-based ones: the models of the merged base are the closest interpretations to the given profile. Closeness is, in this context, measured as a number resulting from the aggregation of the distances to each base of the profile. In this work we define a new familly of propositional merging operators, close to such distance-based merging operators, but relying on a set-theoretic definition of closeness, already at work in several revision/update operators from the literature. We study a specific merging operator of this family, obtained by considering set-product as the aggregation function.

We extend the knowledge compilation map introduced by Darwiche and Marquis with new propositional fragments obtained by applying closure principles to several fragments studied so far. We investigate two closure principles: disjunction and implicit forgetting (i.e., existential quantification). Each introduced fragment is evaluated w.r.t. several criteria, including the complexity of basic queries and transformations, and its spatial efficiency is also analyzed.

We introduce and study qualitative multiple outcomes games. These games are noncooperative games with qualitative utilities (i.e., values over an ordinal scale), strictly qualitative uncertainty and possible coordination. By strictly qualitative uncertainty, we mean that when there is a set of possible events, the probability of each event is unknown. Coordination is a way offered to the players to remove uncertainty. Qualitative multiple outcomes games is a model for a number of multi-agent problems where agents have minimal information about the interaction effects and where probabilites are unavailable. Among them is multi-agent planning where autonomous planning agents do not share the same goals, and have to generate plans that interact with those of others in a way they cannot unilaterally predict or control.

This paper is centered on a family of propositional multivalued logics, based on bilattices. The semantics of such logics relies on a set of “truth values,” with two orderings that give the set a bilattice structure. Many interesting inference relations can be defined on these grounds, especially paraconsistent ones and/or nonmonotonic ones. The focus is laid on Belnap's fundamental bilattice logic FOUR, with four “epistemic truth values,” which proves sufficient for the purpose of inference. We show how the bilattice can be associated with a second biordinal structure, which no longer is bilatticial but bipolar. We show how additional inference relations in the logic FOUR can be obtained by exploiting the two preorders associated with this structure. © 2008 Wiley Periodicals, Inc.

Merging operators aim at defining the beliefs/goals of a group of agents from the beliefs/goals of each member of the group. Whenever an agent of the group has preferences over the possible results of the merging process (i.e., the possible merged bases), she can try to rig the merging process by lying on her true beliefs/goals if this leads to better merged base according to her point of view. Obviously, strategy-proof operators are highly desirable in order to guarantee equity among agents even when some of them are not sincere. In this paper, we draw the strategy-proof landscape for many merging operators from the literature, including model-based ones and formula-based ones. Both the general case and several restrictions on the merging process are considered.

Two families of conciliation processes for intelligent agents based on an iterated merge-then-revise change function for belief profiles are introduced and studied. The processes from the first family are sceptical in the sense that at any revision step, each agent considers that her current beliefs are more important than the current beliefs of the group, while the processes from the other family are credulous. Some key features of such conciliation processes are pointed out for several merging operators; especially, the stationarity issue, the existence of consensus and the properties of the induced iterated merging operators are investigated.

We present new prudent semantics within Dung's theory of argumentation. Under such prudent semantics, two arguments cannot belong to the same extension whenever one of them attacks indirectly the other one. We argue that our semantics lead to a better handling of controversial arguments than Dung's ones. We compare the prudent inference relations induced by our semantics w.r.t. cautiousness; we also compare them with the inference relations induced by Dung's semantics.

Independence -- the study of what is relevant to a given problem of reasoning -- has received an increasing attention from the AI community. In this paper, we consider two basic forms of independence, namely, a syntactic one and a semantic one. We show features and drawbacks of them. In particular, while the syntactic form of independence is computationally easy to check, there are cases in which things that intuitively are not relevant are not recognized as such. We also consider the problem of forgetting, i.e., distilling from a knowledge base only the part that is relevant to the set of queries constructed from a subset of the alphabet. While such process is computationally hard, it allows for a simplification of subsequent reasoning, and can thus be viewed as a form of compilation: once the relevant part of a knowledge base has been extracted, all reasoning tasks to be performed can be simplified.

We propose a perspective on knowledge compilation which calls for analyzing different compilation approaches according to two key dimensions: the succinctness of the target compilation language, and the class of queries and transformations that the language supports in polytime. We then provide a knowledge compilation map, which analyzes a large number of existing target compilation languages according to their succinctness and their polytime transformations and queries. We argue that such analysis is necessary for placing new compilation approaches within the context of existing ones. We also go beyond classical, flat target compilation languages based on CNF and DNF, and consider a richer, nested class based on directed acyclic graphs (such as OBDDs), which we show to include a relatively large number of target compilation languages.

This paper presents new complexity results for propositional closed world reasoning (CWR) from tractable knowledge bases (KBs). Both (basic) CWR, generalized CWR, extended generalized CWR, careful CWR and extended CWR (equivalent to circumscription) are considered. The focus is on tractable KBs belonging to target classes for exact compilation functions: Blake formulas, DNFs, disjunctions of Horn formulas, and disjunctions of renamable Horn formulas. The complexity of inference is identified for all the forms of CWR listed above. For each of them, new tractable fragments are exhibited. Interestingly, the restricted classes of formulas we consider are target classes for exact compilation functions, i.e., every KB can be turned into an equivalent formula from any of these classes. Accordingly, our results suggest knowledge compilation as a valuable, practical approach to deal with the complexity of CWR in some situations.

In this paper, a notion of novelty of a formula for a concept w.r.t. a deductive database is investigated from a logical point of view. Intuitively, a formula is new for a concept when inserting the formula together with some additional information in the database allows us to infer an instance of the concept (or its negation) from the resulting database, while this proves impossible when only the additional information is inserted. First, this notion is analysed in the framework of first-order Herbrand monotonic databases. A decision procedure is provided, based on a prime implicants characterization. Then, novelty is investigated in the context of non-monotonic—completed—databases. Actually, four types of novelty are put forward to capture various intuitions about the relations between novelty and forms of non-monotonicity. These types of novelty are proved incomparable in the general case and their decision problems are discussed. Finally, possible applications of novelty in the database field are presented.

Reasoning about time in presence of incomplete information is central in a wide range of artificial intelligence applications. For this purpose, time must be accounted for while reasoning about assumptions. To deal with the hypothetical dimension of inference, De Kleer's assumption-based truth maintenance approach proved valuable in many situations. However, it cannot handle temporally-qualified assertions. This paper contributes to fill the gap. It addresses the problem of performing assumption-based truth maintenance in a window-based temporal logic.>

Many researches in artificial intelligence have been devoted so far to logic-based abductive inference. However, as far as one knows, the problem of characterizing metatheoretic properties of abduction has not been addressed till now. The author contributes to filling this gap. Abductive inference is abstractly considered a relation between a theory, an observation, a preference criterion and a hypothesis. Metatheoretic properties of this relation are pointed out and discussed.

Much research has been devoted to diagnosis, where two main approaches have been pointed out: the empirical association-based diagnostic approach and the model-based diagnostic one. Both approaches can be characterized by the kind of knowledge that has to be specified and the diagnostic method that has to be used. However, it seems particularly difficult in real-world applications to obtain a complete description of the faulty (dually, correct) behavior of a system. This incompleteness of description is the reason why deductive reasoning alone is generally insufficient to point out the actual diagnosis. Deduction only allows one to generate some possible partial diagnoses. The latter must be selected and completed to get closer to the actual diagnosis. Both selection and completion require hypothetical reasoning and can be characterized by some preference criteria. The authors' contribution is twofold. A new diagnostic method based on deduction and abduction is then proposed, which is sufficiently flexible to deal with multiple knowledge representations.>

Abduction is the process of generating the best explanation as to why a fact is observed given what is already known. A real problem in this area is the selective generation of hypotheses that have some reasonable prospect of being valid. The author proposes the notion of skeptical abduction as a model to face this problem. After providing a definition of abductive reasoning, skeptical abduction and specific abduction are compared in a logical framework. The mechanism of abductive reasoning in propositional logic is investigated and its generalization to first-order logic is discussed.>