A common practice of ML systems development concerns the training of the same model under different data sets, and the use of the same (training and test) sets for different learning models. The first case is a desirable practice for identifying high quality and unbiased training conditions. The latter case coincides with the search for optimal models under a common dataset for training. These differently obtained systems have been considered akin to copies. In the quest for responsible AI, a legitimate but hardly investigated question is how to verify that trustworthiness is preserved by copies. In this paper we introduce a calculus to model and verify probabilistic complex queries over data and define four distinct notions: Justifiably, Equally, Weakly and Almost Trustworthy which can be checked analysing the (partial) behaviour of the copy with respect to its original. We provide a study of the relations between these notions of trustworthiness, and how they compose with each other and under logical operations. The aim is to offer a computational tool to check the trustworthiness of possibly complex systems copied from an original whose behavour is known.

• Novel logic-based approach to data bias in machine learning predictions for defining and quantifying fairness based on the Ulam game. • New perspectives on the rule of constrained monotonicity valid in the play process of the Ulam game and its generalisation to weighted evidence. • Connection between the notion of correctability and levels of monotonicity satisfied by machine learning algorithms. • Novel game-theoretic framework of algorithmic fairness. In the present work, we develop a novel information-theoretic and logic-based approach to data bias in Machine Learning predictions and show its relevance in the specific context of fairness evaluation. We frame predictions made on biased data as Ulam games, which formalise key aspects of data-driven inference, and from which a variation of the rational non-monotonic consequence relation can be defined. We investigate this framework to model how differential levels of noise in input features impact Machine Learning predictions. To the best of our knowledge, this is the first game-theoretic formalisation of ML unfairness.

The algorithmic detection of disinformation online is currently based on two strategies: on the one hand, research focuses on automated factchecking; on the other hand, models are being developed to assess the trustworthiness of information sources, including both empirical and theoretical research on credibility and content quality.For debates among experts, in particular, it might be hard to discern (less) reliable information, as all actors by definition are qualified.In these cases, the use of trustworthiness metrics on sources is a useful proxy for establishing the truthfulness of contents.We introduce an algorithmic model for automatically generating a dynamic trustworthiness hierarchy among information sources based on several parameters, including fact-checking.The method is novel and significant, especially in two respects: first, the generated hierarchy represents a helpful tool for laypeople to navigate experts' debates; second, it also allows to identify and overcome biases generated by intuitive rankings held by agents at the beginning of the debates.We provide an experimental analysis of our algorithmic model applied to the debate on the SARS-CoV-2 virus, which took place among Italian medical specialists between 2020 and 2021.

Abstract In this paper we present the probabilistic typed natural deduction calculus TPTND, designed to reason about and derive trustworthiness properties of probabilistic computational processes, like those underlying current AI applications. Derivability in TPTND is interpreted as the process of extracting $n$ samples of possibly complex outputs with a certain frequency from a given categorical distribution. We formalize trust for such outputs as a form of hypothesis testing on the distance between such frequency and the intended probability. The main advantage of the calculus is to render such notion of trustworthiness checkable. We present a computational semantics for the terms over which we reason and then the semantics of TPTND, where logical operators as well as a Trust operator are defined through introduction and elimination rules. We illustrate structural and metatheoretical properties, with particular focus on the ability to establish under which term evaluations and logical rules applications the notion of trustworthiness can be preserved.

The notion of trustworthiness, central to many fields of human inquiry, has recently attracted the attention of various researchers in logic, computer science, and artificial intelligence (AI). Both conceptual and formal approaches for modelling trustworthiness as a (desirable) property of AI systems are emerging in the literature. To develop logics fit for this aim means to analyse both the non-deterministic aspect of AI systems and to offer a formalization of the intended meaning of their trustworthiness. In this work we take a semantic perspective on representing such processes, and provide a measure on possible worlds for evaluating them as trustworthy. In particular, we intend trustworthiness as the correspondence within acceptable limits between a model in which the theoretical probability of a process to produce a given output is expressed and a model in which the frequency of showing such output as established during a relevant number of tests is measured. From a technical perspective, we show that our semantics characterizes the probabilistic typed natural deduction calculus introduced in [12] and further extended in [13]. This contribution connects those results on trustworthy probabilistic processes with the mainstream method in modal logic, thereby facilitating the understanding of this field of research for a larger audience of logicians, as well as setting the stage for an epistemic logic appropriate to the task.

Abstract This paper shows how safety and liveness properties are not necessarily preserved by different kinds of copies of computational artefacts and proposes procedures to preserve them, which are consistent with ethical analyses on software property rights infringement. Safety and liveness are second-order properties that are crucial in the definition of the formal ontology of computational artefacts. Software copies are analysed at the level of their formal models as exact, inexact and approximate copies, according to the taxonomy in [3]. First, it is explained how exact copies are the only kind of copies that preserve safety and liveness properties, and how inexact and approximate copies do not necessarily preserve them. Secondly, two model checking algorithms are proposed to verify whether inexact and approximate copies actually preserve safety and liveness properties. Essential properties of termination, correctness and complexity are proved for these algorithms. Finally, contraction and expansion algorithmic operations are defined, allowing for the automatic design of safety- and liveness-preserving approximate copies. As a conclusion, the relevance of the present logical analysis for the ongoing debates in miscomputation and computer ethics is highlighted.

Review scores collect users’ opinions in a simple and intuitive manner. However, review scores are also easily manipulable, hence they are often accompanied by explanations. A substantial amount of research has been devoted to ascertaining the quality of reviews, to identify the most useful and authentic scores through explanation analysis. In this paper, we advance the state of the art in review quality analysis. We introduce a rating system to identify review arguments and to define an appropriate weighted semantics through formal argumentation theory. We introduce an algorithm to construct a corresponding graph, based on a selection of weighted arguments, their semantic distance, and the supported ratings. We also provide an algorithm to identify the model of such an argumentation graph, maximizing the overall weight of the admitted nodes and edges. We evaluate these contributions on the Amazon review dataset by McAuley et al. (2015), by comparing the results of our argumentation assessment with the upvotes received by the reviews. Also, we deepen the evaluation by crowdsourcing a multidimensional assessment of reviews and comparing it to the argumentation assessment. Lastly, we perform a user study to evaluate the explainability of our method, i.e., to test whether the automated method we use to assess reviews is understandable by humans. Our method achieves two goals: (1) it identifies reviews that are considered useful, comprehensible, and complete by online users, and does so in an unsupervised manner, and (2) it provides an explanation of quality assessments.

Abstract Information transmission in social networks is riddled with issues of reliability and trustworthiness. One of the main sources of disinformation can be traced back to agents—human or artificial—whose political or cultural agenda is guided by conspiracy theories. Modelling and understanding the behaviour of such agents within social networks is therefore crucial to approach the disinformation problem. In the present paper, we formulate the logic (un)SecureNDsim*, equipped with a proof-theory and a relational semantics in which negative trust relations are defined formalizing the attitude of paranoid agents, i.e. agents distrusting any information originating from the authority and thereby spreading what can be characterized as the content of conspiracy theories. The logic is implemented in a multi-agent simulation aimed at analysing the effects of conspiracy theorists in networks of agents. In particular, we analyse consensus reaching scenarios and the ability of paranoid agents to induce the spread of potentially false information.

The spread and exchange of information among people has been formally studied in the social sciences since the 1950s. The ways in which we do communicate has changed multiple times since. In particular, since the digitalization of communication methods, the speed of information exchange, the connectivity among people and with artificial agents, the reachability of information contents have all changed. Moreover, we now have an almost permanent record of what knowledge has been communicated, when, by whom. This novel status of information exchange has rapidly become a new field of studies on its own. The understanding of networked communication has thus become ubiquitous in multi-agent systems in AI, in epistemic-social logics and of course in social network analysis. Works that address this challenge are also split across these fields. This special issue is devoted to the theme of the ECAI workshop ‘Netreason: Reasoning About Social Networks’ (organized online on September...

Depth-Bounded Boolean Logics (DBBL for short) are well-understood frameworks to model rational agents equipped with limited deductive capabilities. These Logics use a parameter k>=0 to limit the amount of virtual information, i.e., the information that the agent may temporarily assume throughout the deductive process. This restriction brings several advantageous properties over classical Propositional Logic, including polynomial decision procedures for deducibility and refutability. Inspired by DBBL, we propose a limited-depth version of the popular ASP system \clingo, tentatively dubbed k-lingo after the bound k on virtual information. We illustrate the connection between DBBL and ASP through examples involving both proof-theoretical and implementative aspects. The paper concludes with some comments on future work, which include a computational complexity characterization of the system, applications to multi-agent systems and feasible approximations of probability functions.

Abstract Logics of design have been formulated until recently to offer systematic treatments of the way systems express the relation between resources, processes and their outputs. We present a logic of systems design which explicitly formalizes this relation as a decidable checking problem on resource access and define computable efficiency and optimality properties.

Defining identity for entities is a longstanding logical problem in philosophy, and it has resurfaced in current investigations within the philosophy of technology. The problem has not yet been explored for the philosophy of information, and of Computer Science in particular. This paper provides a logical analysis of identity and copy for computational artefacts. Identity is here understood as the relation holding between an instance of a computational artefact and itself. By contrast, the copy relation holds between two distinct computational artefacts. We distinguish among exact, inexact and approximate copies. We use process algebra to provide suitable formal definitions of these relations, using in particular the notion of bisimulation to define identity and exact copies, and simulation for inexact and approximate copies. Equivalence is unproblematic for identical computational artefacts at each individual time and for inexact copies; we will examine to which extent the formal constraints on identity criteria discussed in the literature are satisfied by our approach. As for inexact and approximate copy, they are intended as a weakening of the identity relation in that equivalence and other constraints on identity are violated. The proposed approach also suggests a computable treatment of identity and copy checking.

Software management systems need to preserve integrity by the handling, approval, tracking and execution of changes on the packages of the current installation profile. This is a problematic task, which needs to be accounted for both in terms of installation of new packages and removal of conflicti ng ones. While existing approaches are able to identify dependency satisfaction and conflicts, a broader and efficient approach can be formalised in terms of trust. Positive instances of trust are required by the identification of safely installable packages. Negative trust, a much less explored concept, can be useful to analyse the complementary issue of packages’ removal both in case of conflicts and of security issues. In this paper we develop a logic of negative trust with two aims: identifying packages that are undesirable in view of the current installation profile; and currently installed packages that become inconsistent with a new intended installation. The logic provides distinct procedures for the identification of either case. We illustrate properties of the calculus, provide a simple working example and offer a translation of the protocol to the Coq proof assistant for verification of its formal correctness.

Embedded systems such as Cyber-Physical Systems (CPS) are typically designed as a network of multiple interacting elements with physical input (or sensors) and output (or actuators). One aspect of interest of open systems is fidelity, or the compliance between physical figures of interest and their internal representation. High fidelity is defined as a stable mapping between actions in the physical domain and intended or expected values in the system domain and deviations from fidelity are quantifiable over time by some appropriate informative variable. In this paper, we provide a model for designing such systems based on a framework for trustworthiness monitoring and we provide a Jason implementation to evaluate the feasibility of our approach. In particular, we build a bridge between a standard publish/subscribe framework for CPS called MQTT and Jason to enable automatic reasoning about trustworthiness.

We consider security threats in software installation processes, posed by transitively trusted dependencies between packages from distinct repositories. To analyse them, we present SecureNDC, a Coq implemented calculus using an explicit trust function to bridge repository access and software package installation rights. Thereby, we resolve a version of the minimum install problem under trust conditions on repositories.

System integrity can be put at risk by unintentional transitivity of resource access. We present a natural deduction calculus for an access control model with an explicit trust function on resources. Its inference relation is designed to limit unintentionally transitive access from untrusted parties. We also offer results for ordered cut and normalization related to security and hint at a prototype implementation.