Giuseppe Primiero

In the context of deterministic scientific simulations, formal validity requirements have typically been defined to help us reason about the relationship between the mathematical model underlying the target system and the computational model used to simulate it. With machine learning simulations entering the picture, we argue that these formal requirements need to be reviewed, as the objects to which they apply have significantly changed. This is due to several reasons: the target system is no longer an available system object of investigation; the probabilistic mathematical model is abstracted from the target system through the mediation of the computational model, which however remains largely opaque to us due to its high complexity. For these reasons, we formulate weaker, probabilistic versions of the traditional relations of Simulation, Bisimulation, and Approximate Simulation. Accordingly, we define three corresponding validity criteria that capture a range of cases, from the strongest to the weakest, depending on the extent to which the machine learning model can be assumed to correctly represent its target system.

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 second edition of the BEWARE workshop, co-located with the AIxIA 2023 conference, was held in Rome on November 6, 2023. The workshop focused on the emerging ethical aspects of AI, particularly addressing Bias, Risk, Explainability, and the role of Logic and Logic Programming. The event brought together a diverse group of researchers and practitioners to discuss and explore solutions for ethical decision-making in AI. This year, the workshop saw significant participation, with 9 accepted high-quality submis- sions, 5 as long papers and 4 as short papers (out of a total of 11 submitted papers), rigorously peer-reviewed by our Program Committee.

The present paper formulates an Epistemic Constructive Definition of Information (ECDI), based on the rejection of the alethic nature ascribed to declarative objective semantic information (DOS). ECDI reformulates the principles holding for the non-alethic Standard Definition of Information (SDI), it is based on the Verificationist Principle of Truth and it refers to the typical constructive distinction between judgemental act and propositional content. The resulting framework defines two distinct and complementary epistemic acts: justifications and conditions of knowledge. Finally, the concept of information is formally presented within the syntactic-semantic method of Constructive Type Theory (CTT). © 2011 Elsevier B.V., All rights reserved.

Contextual type theories are largely explored in their applications to programming languages, but less investigated for knowledge representation purposes. The combination of a constructive language with a modal extension of contexts appears crucial to explore the attractive idea of a type-theoretical calculus of provability from refutable assumptions for non-monotonic reasoning. This paper introduces such a language: the modal operators are meant to internalize two different modes of correctness, respectively with necessity as the standard notion of constructive verification and possibility as provability up to refutation of contextual conditions. © 2013 Elsevier B.V., All rights reserved.

The widespread emergence of phenomena of bias is certainly among the most adverse impacts of new data-intensive sciences and technologies. The causes of such undesirable behaviours must be traced back to data themselves, as well as to certain design choices of machine learningMachine learning (ML) algorithms. The task of modelling bias from a logical point of view requires to extend the vast family of defeasible logicsDefeasible logic and logics for uncertain reasoningReasoninguncertain with ones that capture some few, fundamental properties of biased predictions. However, a logically grounded approach to machine learningMachine learning (ML) fairness is still at early stages in the literature. In this paper, we discuss current approaches to the topic, formulate general logical desiderata for logics to reason with and about bias, and provide a novel approach.

The notion of trust is a major player, in many epistemic and computational contexts. Such notion appears especially relevant in all those situations where verification or evaluation of knowledge is missing, not reachable or non-existent, and agents must rely on information received by others. This includes cases where expert knowers may not yet be able to ground their claims, and the public has to build an opinion by considering the dynamic of the information exchange. Formal logic approaches to this aim have been increasingly important and diverse in the last decades. A natural and important extension of such multi-agent contexts is where epistemic acts are performed under uncertainty, at several levels: the claims of the agents may be graded; information may reach agents with a certain degree of probability; and the degree of acceptance or rejection of the information received may not be binary. We present a multi-agent logic of negative trust applied to uncertain judgements. We offer a proof theory and a relational semantics for which standard soundness and completeness results hold.

Correctness is a major concern for logical systems, especially for its significance in computational settings. While establishing a norm for the correctness of computational procedures is a standard requirement, defining errors is a less investigated formal problem. In typed systems, in particular, errors are dealt with by rising execeptions and when their resolution fails, these are followed by abortion procedures. In distributed systems, this corresponds to error detection and service restart. More efficient error resolution strategies for code mobility failures in distributed computing can be defined by re-evaluation and re-addressing of resources in referentially transparent expressions. We formulate a substructural modal type system to analyse failure of mobile code and appropriate resolution strategies when abortion is not required. We provide local soundness and completeness results, analyse restricted structural properties, show reduction and expansion on failure states and offer a simple application of the language. Moreover, we design a state transition semantics and offer soundness and completeness results with respect to the proof theory.

The relation between logic and knowledge has been at the heart of a lively debate since the 1960s. On the one hand, the epistemic approaches based their formal arguments in the mathematics of Brouwer and intuitionistic logic. Following Michael Dummett, they started to call themselves `antirealists'. Others persisted with the formal background of the Frege-Tarski tradition, where Cantorian set theory is linked via model theory to classical logic. Jaakko Hintikka tried to unify both traditions by means of what is now known as `explicit epistemic logic'. Under this view, epistemic contents are introduced into the object language as operators yielding propositions from propositions, rather than as metalogical constraints on the notion of inference. The Realism-Antirealism debate has thus had three players: classical logicians, intuitionists and explicit epistemic logicians. The editors of the present volume believe that in the age of Alternative Logics, where manifold developments in logic happen at a breathtaking pace, this debate should be revisited. Contributors to this volume happily took on this challenge and responded with new approaches to the debate from both the explicit and the implicit epistemic point of view.

Some computational phenomena rely essentially on pragmatic considerations, and seem to undermine the independence of the specification from the implementation. These include software development, deviant uses, esoteric languages and recent data-driven applications. To account for them, the interaction between pragmatics, epistemology and ontology in computational artefacts seems essential, indicating the need to recover the role of the language metaphor. We propose a User Levels (ULs) structure as a pragmatic complement to the Levels of Abstraction (LoAs)-based structure defining the ontology and epistemology of computational artefacts. ULs identify a flexible hierarchy in which users bear their own semantic and normative requirements, possibly competing with the logical specification. We formulate a notion of computational act intended in its pragmatic sense, alongside pragmatic versions of implementation and correctness.

Current research in Explainable AI includes post-hoc explanation methods that focus on building transparent explaining agents able to emulate opaque ones. Such agents are naturally required to be accurate and trustworthy. However, what it means for an explaining agent to be accurate and trustworthy is far from being clear. We characterize accuracy and trustworthiness as measures of the distance between the formal properties of a given opaque system and those of its transparent explanantes. To this aim, we extend Probabilistic Computation Tree Logic with operators to specify degrees of accuracy and trustworthiness of explaining agents. We also provide a semantics for this logic, based on a multi-agent structure and relative model-checking algorithms. The paper concludes with a simple example of a possible application.

The process of completing, correcting and prioritising specifications is an essential but very complex task for the maintenance and improvement of software systems. The preservation of functionalities and the ability to accommodate changes are main objectives of the software development cycle to guarantee system reliability. Logical theories able to fully model such processes are still insufficient. In this paper we propose a full formalisation of such operations on software systems inspired by the Alchourrón–Gärdenfors–Makinson paradigm for belief revision of human epistemic states. We represent specifications as finite sets of formulas equipped with a priority relation that models functional entrenchment of properties. We propose to handle specification incompleteness through ordered expansion, inconsistency through ordered safe contraction and prioritisation through revision with reordering, and model all three in an algorithmic fashion. We show how the system satisfies basic properties of the AGM paradigm, including Levi’s and Harper’s identities. We offer a concrete example and complexity results for the inference and model checking problems on revision. We conclude by describing resilience and evolvability of software systems based on such revision operators.

In Information Systems development, resilience has often been treated as a non-functional requirement and little or no work is aimed at building resilience in end-users through systems development. The question of how values and resilience (for the end-user) can be incorporated into the design of systems is an on-going research activity in user-centered design. In this paper we evaluate the relation of values and resilience within the context of an ongoing software development project and contribute a formal model of co-design based on a significant extension of Abstract Design Theory. The formal analysis provides a full and clear-cut definition of the co-design space, its objectives and processes. On the basis of both, we provide an abstract definition of resilient system (for the end-user). We conclude that value-sensitive co-design enforces better resilience in end-users.

We present a multi-conclusion natural deduction calculus characterizing the dynamic reasoning typical of Adaptive Logics. The resulting system AdaptiveND is sound and complete with respect to the propositional fragment of adaptive logics based on CLuN. This appears to be the first tree-format presentation of the standard linear dynamic proof system typical of Adaptive Logics. It offers the advantage of full transparency in the formulation of locally derivable rules, a connection between restricted inference-rules and their adaptive counterpart, and the formulation of abnormalities as a subtype of well-formed formulas. These features of the proposed calculus allow us to clarify the relation between defeasible and multiple-conclusion approaches to classical recapture.

Computing, today more than ever before, is a multi-faceted discipline which collates several methodologies, areas of interest, and approaches: mathematics, engineering, programming, and applications. Given its enormous impact on everyday life, it is essential that its debated origins are understood, and that its different foundations are explained. On the Foundations of Computing offers a comprehensive and critical overview of the birth and evolution of computing, and it presents some of the most important technical results and philosophical problems of the discipline, combining both historical and systematic analyses. The debates this text surveys are among the latest and most urgent ones: the crisis of foundations in mathematics and the birth of the decision problem, the nature of algorithms, the debates on computational artefacts and malfunctioning, and the analysis of computational experiments. By covering these topics, On the Foundations of Computing provides a much-needed resource to contextualize these foundational issues. For practitioners, researchers, and students alike, a historical and philosophical approach such as what this volume offers becomes essential to understand the past of the discipline and to figure out the challenges of its future.

This paper contributes to the computer ethics debate on software ownership protection by examining the ontological, methodological, and ethical problems related to property right infringement that should come prior to any legal discussion. The ontological problem consists in determining precisely what it is for a computer program to be a copy of another one, a largely neglected problem in computer ethics. The methodological problem is defined as the difficulty of deciding whether a given software system is a copy of another system. And the ethical problem corresponds to establishing when a copy constitutes, or does not constitute, a property right infringement. The ontological problem is solved on the logical analysis of abstract machines, and the latter are argued to be the appropriate level of abstraction for software at which the methodological and the ethical problems can be successfully addressed.