%0 Journal Article %J Topoi. An International Reiew of Philosophy %D In Press %T The semantics of untrustworthiness %A Primiero, Giuseppe %A Kosolosky, Laszlo %X

We o er a formal treatment of the semantics of both complete and incomplete mistrustful or distrustful information transmissions. The se- mantics of such relations is analysed in view of rules that dene the be- haviour of a receiving agent. We justify this approach in view of human agent communications and secure system design. We further specify some properties of such relations.

%B Topoi. An International Reiew of Philosophy %G eng %R http://dx.doi.org/10.1007/s11245-013-9227-2 %0 Journal Article %J Electronic Notes in Theoretical Computer Science %D 2014 %T J-Calc: A typed lambda calculus for Intuitionistic Justification Logic %A Pouliasis, Konstantinos %A Primiero, Giuseppe %X

In this paper we offer a system J-Calc that can be regarded as a typed λ -calculus for the {→,&\#8869;} fragment of Intuitionistic Justification Logic. We offer different interpretations of J-Calc, in particular, as a two phase proof system in which we proof check the validity of deductions of a theory Τ based on deductions from a stronger theory Τ' and computationally as a type system for separate compilations. We establish some first metatheoretic results.

%B Electronic Notes in Theoretical Computer Science %V 300 %P 71–87 %G eng %R 10.1016/j.entcs.2013.12.012 %0 Generic %D 2013 %T Alleged assassins: realist and constructivist semantics for modal modification %A Jespersen, Bjørn %A Primiero, Giuseppe %X

Modal modifiers such as Alleged oscillate between being subsective and being privative. If individual a is an alleged assassin (at some parameter of evaluation) then it is an open question whether a is an assassin (at that parameter). Standardly, modal modifiers are negatively defined, in terms of failed inferences or non-intersectivity or non-extensionality. Modal modifiers are in want of a positive definition and a worked-out logical semantics. This paper offers two positive definitions. The realist definition is elaborated within Tichý’s Transparent Intensional Logic (TIL) and builds upon Montague’s model-theoretic semantics for adjectives as representing mappings from properties to properties. The constructivist definition is based on an extension of Martin-Löf’s Constructive Type Theory (CTT) so as to accommodate partial verification. We show that, and why, “a is an alleged assassin” and “Allegedly, a is an assassin” are equivalent in TIL and synonymous in CTT.

%B Logic, Language, and Computation %S Lecture Notes in Computer Science %I Springer %V 7758 %P 94–114 %G eng %R 10.1007/978-3-642-36976-6_8 %0 Journal Article %J Philosophical Studies %D 2013 %T Offline and online data: on upgrading functional information to knowledge %A Primiero, Giuseppe %X

This paper addresses the problem of upgrading functional information to knowledge. Functional information is defined as syntactically well-formed, meaningful and collectively opaque data. Its use in the formal epistemology of information theories is crucial to solve the debate on the veridical nature of information, and it represents the companion notion to standard strongly semantic information, defined as well-formed, meaningful and true data. The formal framework, on which the definitions are based, uses a contextual version of the verificationist principle of truth in order to connect functional to semantic information, avoiding Gettierization and decoupling from true informational contents. The upgrade operation from functional information uses the machinery of epistemic modalities in order to add data localization and accessibility as its main properties. We show in this way the conceptual worthiness of this notion for issues in contemporary epistemology debates, such as the explanation of knowledge process acquisition from information retrieval systems, and open data repositories.

%B Philosophical Studies %V 164 %P 371–392 %G eng %R http://dx.doi.org/10.1007/s11098-012-9860-4 %0 Journal Article %J Minds and Machines %D 2013 %T A taxonomy of errors for information systems %A Primiero, Giuseppe %X

We provide a full characterization of computational error states for information systems. The class of errors considered is general enough to include human rational processes, logical reasoning, scientific progress and data processing in some functional programming languages. The aim is to reach a full taxonomy of error states by analysing the recovery and processing of data. We conclude by presenting machine-readable checking and resolve algorithms.

%B Minds and Machines %V 24 %P 249–273 %G eng %R 10.1007/s11023-013-9307-5 %0 Journal Article %J Logique et Analyse %D 2012 %T A contextual type theory with judgemental modalities for reasoning from open assumptions %A Primiero, Giuseppe %X

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.

%B Logique et Analyse %V 55 %P 579–600 %G eng %0 Conference Proceedings %B Logic and Engineering of Natural Language Semantics 9 (LENLS 9-2012) %D 2012 %T A formal approach to vague expressions with indexicals %A Martens, Liesbeth %A Primiero, Giuseppe %X

In this paper, we offer a formal approach to the scantily investigated problem of vague expressions with indexicals, in particular including the spatial indexical `here' and the temporal indexical `now'. We present two versions of an adaptive fuzzy logic extended with an indexical, formally expressed by a modifier as a function that applies to predicative formulas. In the first version, such an operator is applied to non-vague predicates. The modified formulas may have a fuzzy truth value and fit into a Sorites paradox. We use adaptive fuzzy logics as a reasoning tool to address such a paradox. The modifier enables us to off er an adequate explication of the dynamic reasoning process. In the second version, a different result is obtained for an indexical applied to a formula with a possibly vague predicate, where the resulting modified formula has a crisp value and does not add up to a Sorites paradox.

%B Logic and Engineering of Natural Language Semantics 9 (LENLS 9-2012) %I Japanese Society for Artificial Intelligence %P 37-51 %G eng %0 Report %D 2012 %T Intuitionistic Logic of Proofs with dependent proof terms %A Primiero, Giuseppe %X

The basic logic of proofs extends the usual propositional language by expressions of the form "s is a proof of A", for any proposition A. In this paper we explore the extension of its intuitionistic fragment to a language including expressions of the form "t is a proof of B, dependent from sbeing a proof of A". We aim at laying down a ground comparison with equivalent constructions present in theories of dependent types, especially those similarly based on the Brouwer-Heyting-Kolmogorov semantics. We further translate this extended language to a natural deduction calculus which allows for a double interpretation of the construction on which a proof term may depend: as actually proven, or valid assumption, or as possibly proven, locally true assumption. We show meta-theoretical properties for this calculus and explain normalisation to a language with only unconditional proofs. We conclude by stating the characterization of our calculus with standard intutionistic logic of proofs

%B Preprint Series of the Isaac Newton Institute for Mathematical Sciences %G eng %0 Journal Article %J Journal of Applied Logic %D 2012 %T A modal type theory for formalizing trusted communications %A Primiero, Giuseppe %A Taddeo, Mariarosaria %X

This paper introduces a multi-modal polymorphic type theory to model epistemic processes characterized by trust, defined as a second-order relation affecting the communication process between sources and a receiver. In this language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgement. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous version of a type theory, in which we show the embedding of the modal operators into standard group knowledge operators.

%B Journal of Applied Logic %V 10 %P 92–114 %G eng %R 10.1016/j.jal.2011.12.002 %0 Conference Proceedings %B Third Workshop in the Philosophy of Information %D 2012 %T Reasoning with computer-assisted experiments in mathematics %A De Mol, Liesbeth %E Primiero, Giuseppe %E Allo, Patrick %B Third Workshop in the Philosophy of Information %I Koninklijke Vlaamse Academie van België door Wetenschappen en Kunsten %P 80-92 %G eng %0 Journal Article %J The Reasoner %D 2012 %T Report 'International Conference on History and Philosophy of Computing' (HAPOC) %A De Mol, Liesbeth %A Primiero, Giuseppe %B The Reasoner %V 6 %P 7-8 %G eng %0 Generic %D 2012 %T Type-Theoretical Dynamics. Exploring Belief Revision in a Constructive Framework %A Primiero, Giuseppe %E Rahman, Shahid %E Primiero, Giuseppe %E Marion, Mathieu %X

In the present paper a dynamics for type theory is introduced. The formalization provides epistemic explanations for the basic notions of belief state and belief set by referring to assertion conditions for type-theoretical judgements; it interprets expectations in terms of default assumptions for such a structure and it adapts the usual revision operations and the analogous of the Ramsey test. The model, restricted to operations of revision, merging and information preference, provides a constructive type-theoretical approach to epistemic dynamics.

%B The realism-antirealism debate in the age of alternative logics %I Springer %P 191–212 %G eng %R 10.1007/978-94-007-1923-1_11 %0 Journal Article %J Minds and Machines %D 2011 %T Giovanni Sommaruga (ed): Formal Theories of Information: From Shannon to Semantic Information Theory and General Concepts of Information (Review) %A Primiero, Giuseppe %B Minds and Machines %V 21 %P 119-122 %G eng %R 10.1007/s11023-011-9228-0 %0 Report %D 2011 %T A multi-modal type system and its procedural semantics for safe distributed programming %A Primiero, Giuseppe %X

In this paper we present a multi-modal polymorphic type system for a computational interpretation of programs with distributed resources. Polymorphism induces a distinction between programs whose code is safe at location, and programs whose value is safe overall. We formulate judge- mental modalities to express such distinction and use their introduction and elimination rules to express mobility of code and values within a net- work. The syntactic formulation is completed by a procedural semantics interpreted over states of an abstract machine for which a standard sound- ness result is given in the form of a type safety theorem.

%B Intuitionistic Modal Logic and Applications Workshop (IMLA11), Nancy %G eng %0 Generic %D 2011 %T On the necessity of (sometimes) being synthetic. Comment on Poggiolesi. %A Primiero, Giuseppe %E Allo, Patrick %E Primiero, Giuseppe %B Third Workshop in the Philosophy of Information %I Koninklijke Vlaamse Academie van België %C Brussels %P 63-68 %G eng %0 Journal Article %J The Reasoner %D 2011 %T Report 3rd Workshop in the Philosophy of Information %A Allo, Patrick %A Primiero, Giuseppe %B The Reasoner %V 1 %P 6-7 %G eng %0 Conference Paper %B Proceedings of the Computability in Europe 2010 Conference %D 2010 %T Constructive contextual modal judgments for reasoning from open assumptions %A Primiero, Giuseppe %E Ferreira, F %E Guerra, H %E Mayordomo, E %E Rasga, J %X

Dependent type theories using a structural notion of context are largely explored in their applications to programming languages, but less investigated for knowledge representation purposes. In particular, types with modalities are already used for distributed and staged computation. This paper introduces a type system extended with judgmental modalities internalizing epistemically different modes of correctness to explore a calculus of provability from refutable assumptions.

%B Proceedings of the Computability in Europe 2010 Conference %I Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores %G eng %0 Conference Paper %B Electronic Proceedings of the Federated Logic Conference 2010 (Proof Systems for Program Logics Workshop) %D 2010 %T A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network. %A Primiero, Giuseppe %X

In this paper we present a multi-modal polymorphic constructive type theory for a computational interpretation of programs equipped with locations for data accessibility in the context of distributed processing.

%B Electronic Proceedings of the Federated Logic Conference 2010 (Proof Systems for Program Logics Workshop) %I Citeseer %G eng %0 Conference Paper %B Proceedings of the First International Workshop on Logic-Based Interpretation of Context: Modeling and Applications %D 2009 %T A constructive modal semantics for contextual verification %A Primiero, Giuseppe %X

This paper introduces a non-standard semantics for a modal version of constructive KT for contextual (assumptions-based) verification. The modal fragment expresses verifiability under extensions of contexts, enjoying adapted validity and (weak) monotonicity properties depending on satisfaction of the contextual data.

%B Proceedings of the First International Workshop on Logic-Based Interpretation of Context: Modeling and Applications %I CEUR-Workshop Proceedings %G eng %U http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-550/ %0 Journal Article %J Synthese (KRA Serie) %D 2009 %T An epistemic logic for becoming informed %A Primiero, Giuseppe %K Epistemic logic %K Logic of justification %K Modal logic %K Philosophy of information %X

Various conceptual approaches to the notion of information can currently be traced in the literature in logic and formal epistemology. A main issue of disagreement is the attribution of truthfulness to informational data, the so called Veridicality Thesis (Floridi 2005). The notion of Epistemic Constructive Information (Primiero 2007) is one of those rejecting VT. The present paper develops a formal framework for ECI. It extends on the basic approach of Artemov’s logic of proofs (Artemov 1994), representing an epistemic logic based on dependent justifications, where the definition of information relies on a strict distinction from factual truth. The definition obtained by comparison with a Normal Modal Logic translates a constructive logic for “becoming informed”: its distinction from the logic of “being informed”—which internalizes truthfulness—is essential to a general evaluation of information with respect to truth. The formal disentanglement of these two logics, and the description of the modal version of the former as a weaker embedding into the latter, allows for a proper understanding of the Veridicality Thesis with respect to epistemic states defined in terms of information.

%B Synthese (KRA Serie) %V 167 %P 363-389 %G eng %U http://dx.doi.org/10.1007/s11229-008-9413-8 %R 10.1007/s11229-008-9413-8 %0 Generic %D 2009 %T Epistemic Modalities %A Primiero, Giuseppe %E Primiero, Giuseppe %E Rahman, Shahid %X

I present an analysis of the notion of epistemic modalities, based on an appropriate interpretation of two basic constructivist issues: verification and epistemic agency. Starting from an historical analysis of conditions for judgments, I analyze first the reading of necessity with respect to apodictic judgements, and then that of possibility with respect to hypothetical judgement. The analysis results in a formal treatment of rules for judgemental modal operators, whose aim is to preserve epistemic states corresponding to verified and unverified assumptions in contexts. In the conclusion, further tracks of research are indicated for designing a semantic framework and defining multi-agents systems.

%B Acts of Knowledge: History, Philosophy and Logic %S Tributes %I College Publications %V 9 %P 207–232 %@ 978-1-904987-92-5 %G eng %0 Conference Paper %B Logic, Philosophy and History of Science in Belgium. Proceedings of the Young Researchers Days 2008 %D 2009 %T A note on constructive modalities for information %A Primiero, Giuseppe %E Weber, Erik %E Libert, Thierry %E Marage, Pierre %E Vanpaemel, Geert %B Logic, Philosophy and History of Science in Belgium. Proceedings of the Young Researchers Days 2008 %I Koninklijke Vlaamse Academie van België %C Brussel %G eng %0 Generic %D 2009 %T Prioritized Dynamic Retraction Function on Non-monotonic Information Updates %A Primiero, Giuseppe %E Carnielli, Walter A. %E Coniglio, Marcelo E. %E Loffredo D'Ottaviano, Itala M. %X

In this paper a model for updates on belief sets and retractions thereof is introduced using the standard format of Adaptive Logics. The core of the update retraction procedure is represented by abnormal expressions derivable in the language: they express updates with information con- tradicting previously derived contents. The adaptive strategy aims at restricting the validity of these formulas by focusing at each decreasing degree on the update which is the most rational to retract in order to re- store consistency as soon as possible. This work is related to the standard operations of retraction and withdrawal from the AGM-paradigm and the e ects of dynamic operations such as public announcement in Dynamic Epistemic Logic.

%B The Many Sides of Logic %I College Publications %C London %P 443-463 %G eng %0 Journal Article %J History and Philosophy of Logic %D 2009 %T Proceeding in abstraction: from concepts to types and the recent perspective on information %A Primiero, Giuseppe %X

This article presents an historical and conceptual overview on different approaches to logical abstraction. Two main trends concerning abstraction in the history of logic are highlighted, starting from the logical notions of concept and function. This analysis strictly relates to the philosophical discussion on the nature of abstract objects. I develop this issue further with respect to the procedure of abstraction involved by (typed) -systems, focusing on the crucial change about meaning and predicability. In particular, the analysis of the nature of logical types in the context of Constructive Type Theory allows elucidation of the role of the previously introduced notions. Finally, the connection to the analysis of abstraction in computer science is drawn, and the methodological contribution provided by the notion of information is considered, showing its conceptual and technical relevance. Future research shall focus on the notion of information in distributed systems, analysing the paradigm of information hiding in dependent type theories.

%B History and Philosophy of Logic %V 30 %P 257–282 %G eng %U http://dx.doi.org/10.1080/01445340902872630 %0 Generic %D 2009 %T Two type-theoretical approaches to privative modification %A Primiero, Giuseppe %A Jespersen, Bjørn %E Nakakoji, Kumiyo %E Murakami, Yohei %E McCready, Eric %X

In this paper we apply two kinds of procedural semantics to the problem of privative modification. We do this for three reasons. The first reason is to launch a tough test case to gauge the degree of substantial agreement between a constructivist and a realist interpretation of a procedural semantics; the second is to extend Martin-Lof's Type Theory to privative modification, which is characteristic of natural language; the third reason is to sketch a positive characterization of privation.

%B New Frontiers in Artificial Intelligence: JSAI-isAI 2009 Workshops %I Springer Verlag %C Berlin, Heidelberg %P 239–258 %@ 4-915905-37-3 C3004 %G eng %0 Conference Paper %B Fusion 2008: Proceedings of the 11th International Conference on Information Fusion %D 2008 %T Adaptive arbitration by variant counting on commutative bases with weights %A Primiero, Giuseppe %A Meheus, Joke %X

In this paper a new logical arbitration protocol for fusion of inconsistent information is designed. It defines a selection of models of a premise set in a multi-modal logic that uses the standard format of adaptive logics. The selected models are obtained by a counting procedure on the derivable data conflicting among the various sources. Peculiar of this approach is the definition of weights for commutative bases, in terms of the distinction between partially and fully supported information. The results obtained are compared to standard arbitration protocols and they extend previous work on the adaptive majority protocol.

%B Fusion 2008: Proceedings of the 11th International Conference on Information Fusion %I IEEE %G eng %R http://dx.doi.org/10.1109/ICIF.2008.4632371 %0 Journal Article %J Synthese (KRA Serie) %D 2008 %T Majority Merging by Adaptive Counting %A Primiero, Giuseppe %A Meheus, Joke %X

The present paper introduces a belief merging procedure by majority using the standard format of Adaptive Logics. The core structure of the logic ADM(c) (Adaptive Doxastic Merging by Counting) consists in the formulation of the conflicts arising from the belief bases of the agents involved in the procedure. A strategy is then defined both semantically and proof-theoretically which selects the consistent contents answering to a majority principle. The results obtained are proven to be equivalent to a standard majority operator for bases with partial support.

%B Synthese (KRA Serie) %V 165 %P 203–223 %G eng %R http://dx.doi.org/10.1007/s11229-008-9370-2 %0 Report %D 2008 %T A model for processing updates with inconsistent information on propositional databases %A Primiero, Giuseppe %X

In the present paper a model for information update on propositional databases is formulated using the standard format of Adaptive Logics. The core structure of the update procedure is represented by the ab- normal expressions of the language that formalize received information contradicting previous contents. The strategy de ned to restrict abnor- malities works by establishing, at each stage of the process, the most re- cent and reliable information, updating constantly the base and removing older data.

%I College Publications %G eng %0 Conference Paper %B Proceedings of the Workshop on Logic and Intelligent Interaction %D 2008 %T Quasi-merging and Pure-arbitration on Information for the family of Adaptive Logics ADM %A Primiero, Giuseppe %A Meheus, Joke %E van Benthem, Johan %E Pacuit, Eric %X

The present paper introduces two new information merging protocols for the family of adaptive logics ADM, for which majority merging has been defined in [19]. The new adaptive operators re ect the negotiation processes of quasi-merging and pure arbitration, known from the Integrity Constraints framework introduced in [13]. The Adaptive Variant Counting selection provides a result equivalent to the GMax family of merging operators: it selects a collective model for a multi-set of belief bases based on the number of disagreements verified by the various models according to a leximax function. The Adaptive Minimax Counting selection is a quasi-merging operator which applies a minimax function and it obtains a larger spectrum of possibilities than the previous selection: it simulates the behaviour of the Max family of operators from the Integrity Con- straints framework, avoiding some of its counterintuitive results.

%B Proceedings of the Workshop on Logic and Intelligent Interaction %G eng %0 Conference Paper %B A Meeting of the Minds, proceedings of the workshop on Logic, Rationality and Interaction %D 2007 %T Belief Merging based on Adaptive Interaction %A Primiero, Giuseppe %E van Benthem, Johan %E Shier, Ju %E Veltman, Frank %B A Meeting of the Minds, proceedings of the workshop on Logic, Rationality and Interaction %I College Publications %@ 978-1-904987-48-2 %G eng %0 Conference Paper %B Logica 2006 Yearbook %D 2007 %T On building abstract Terms in Typed Systems %A Primiero, Giuseppe %E Tomala, O %E Honzik, R %X

This paper offers some historical and conceptual remarks on the philosophical and logical procedures of abstraction, based on an account of the notions of concept and function. In order to provide a complete analyis, one should start by considering Plato’s theory of Ideas, which provides the first interpretation of “abstract terms” in the history of philosophy. The nature of the most general Forms, the related problem of the knowledge thereof, their connection to existing (concrete) objects, are the essential features of the Platonic theory of knowledge and of his metaphysics. The Platonic approach is grounded on the principle of conceptual priority of Ideas over their partecipations, the Forms existing separeted from all the particulars: the former are interpreted as standard particulars to which other particulars conform. Nonetheless, my investigation will start rather by Aristotle, who held first the relation of predication to be the basis for defining abstraction: from this I will try to consider some important ideas for the notion of abstraction in Type Systems.

%B Logica 2006 Yearbook %I Filosofia Publisher %G eng %0 Journal Article %D 2007 %T A modal language for contextual computations %A Primiero, Giuseppe %X

In this paper, we present a modal language for contextual computing, corresponding to the fragment of constructive ΚΤ with necessity and pos- sibility operators. We interpret absolute and contextual computations as difierent modes of verifying the truth of propositions. The semantics of the language L cc interprets absolute computations by a direct verification function valid in every state; contextual computations are interpreted in terms of a verification function valid under unverified information. Modal- ities are used to express extensions of contexts in order to de ne local and global validity. This semantics has a (weak) monotonicity property, de- pending on satisfaction of processes in contexts. In the corresponding axiomatic system cΚΤ a restricted version of the deduction theorem for globally valid formulas holds, soundness and completeness are proven and decidability is shown to hold for the necessitation fragment of the language by a restricted finite model property..

%8 June %G eng %0 Conference Paper %B Logica 2005 Yearbook %D 2006 %T Belief Revision in Constructive Type Theory %A Primiero, Giuseppe %E Bilkova, M %E Tomala, O %B Logica 2005 Yearbook %I Filosofia Publisher %G eng