@article {4254511, title = {The semantics of untrustworthiness}, journal = {Topoi. An International Reiew of Philosophy}, year = {In Press}, abstract = {

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.

}, issn = {1316-5011}, doi = {http://dx.doi.org/10.1007/s11245-013-9227-2}, author = {Primiero, Giuseppe and Kosolosky, Laszlo} } @article {pouliasis2014j, title = {J-Calc: A typed lambda calculus for Intuitionistic Justification Logic}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {300}, year = {2014}, pages = {71{\textendash}87}, abstract = {

In this paper we offer a system J-Calc that can be regarded as a typed λ -calculus for the {{\textrightarrow},\&\#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 Τ{\textquoteright} and computationally as a type system for separate compilations. We establish some first metatheoretic results.

}, doi = {10.1016/j.entcs.2013.12.012}, author = {Pouliasis, Konstantinos and Primiero, Giuseppe} } @incollection {jespersen2013alleged, title = {Alleged assassins: realist and constructivist semantics for modal modification}, booktitle = {Logic, Language, and Computation}, series = {Lecture Notes in Computer Science}, volume = {7758}, year = {2013}, pages = {94{\textendash}114}, publisher = {Springer}, abstract = {

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{\'y}’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{\"o}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.

}, doi = {10.1007/978-3-642-36976-6_8}, author = {Jespersen, Bj{\o}rn and Primiero, Giuseppe} } @article {2006773, title = {Offline and online data: on upgrading functional information to knowledge}, journal = {Philosophical Studies}, volume = {164}, number = {2}, year = {2013}, pages = {371{\textendash}392}, abstract = {

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.

}, issn = {0031-8116}, doi = {http://dx.doi.org/10.1007/s11098-012-9860-4}, author = {Primiero, Giuseppe} } @article {primiero2013taxonomy, title = {A taxonomy of errors for information systems}, journal = {Minds and Machines}, volume = {24}, number = {3}, year = {2013}, pages = {249{\textendash}273}, abstract = {

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.

}, doi = {10.1007/s11023-013-9307-5}, author = {Primiero, Giuseppe} } @article {3094113, title = {A contextual type theory with judgemental modalities for reasoning from open assumptions}, journal = {Logique et Analyse}, volume = {55}, number = {220}, year = {2012}, pages = {579{\textendash}600}, abstract = {

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.

}, issn = {0024-5836}, author = {Primiero, Giuseppe} } @proceedings {martens2012formal, title = {A formal approach to vague expressions with indexicals}, journal = {Logic and Engineering of Natural Language Semantics 9 (LENLS 9-2012)}, year = {2012}, pages = {37-51}, publisher = {Japanese Society for Artificial Intelligence}, abstract = {

In this paper, we offer a formal approach to the scantily investigated problem of vague expressions with indexicals, in particular including the spatial indexical {\textquoteleft}here{\textquoteright} and the temporal indexical {\textquoteleft}now{\textquoteright}. 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.

}, author = {Martens, Liesbeth and Primiero, Giuseppe} } @article {Prim_Intu_lo, title = {Intuitionistic Logic of Proofs with dependent proof terms}, year = {2012}, abstract = {

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

}, author = {Primiero, Giuseppe} } @article {primiero2012modal, title = {A modal type theory for formalizing trusted communications}, journal = {Journal of Applied Logic}, volume = {10}, number = {1}, year = {2012}, pages = {92{\textendash}114}, abstract = {

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.

}, doi = {10.1016/j.jal.2011.12.002}, author = {Primiero, Giuseppe and Taddeo, Mariarosaria} } @proceedings {dereasoning, title = {Reasoning with computer-assisted experiments in mathematics}, journal = {Third Workshop in the Philosophy of Information}, year = {2012}, pages = {80-92}, publisher = {Koninklijke Vlaamse Academie van Belgi{\"e} door Wetenschappen en Kunsten}, author = {De Mol, Liesbeth}, editor = {Primiero, Giuseppe and Allo, Patrick} } @article {DeMol2012, title = {Report {\textquoteright}International Conference on History and Philosophy of Computing{\textquoteright} (HAPOC)}, journal = {The Reasoner}, volume = {6}, number = {1}, year = {2012}, pages = {7-8}, author = {De Mol, Liesbeth and Primiero, Giuseppe} } @incollection {primiero2012type, title = {Type-Theoretical Dynamics. {E}xploring Belief Revision in a Constructive Framework}, booktitle = {The realism-antirealism debate in the age of alternative logics}, year = {2012}, pages = {191{\textendash}212}, publisher = {Springer}, abstract = {

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.

}, doi = {10.1007/978-94-007-1923-1_11}, author = {Primiero, Giuseppe}, editor = {Rahman, Shahid and Primiero, Giuseppe and Marion, Mathieu} } @article {Primiero2011, title = {Giovanni Sommaruga (ed): Formal Theories of Information: From {S}hannon to Semantic Information Theory and General Concepts of Information (Review)}, journal = {Minds and Machines}, volume = {21}, number = {1}, year = {2011}, pages = {119-122}, issn = {0924-6495}, doi = {10.1007/s11023-011-9228-0}, author = {Primiero, Giuseppe} } @article {primiero2011multi, title = {A multi-modal type system and its procedural semantics for safe distributed programming}, year = {2011}, abstract = {

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.

}, author = {Primiero, Giuseppe} } @incollection {primieronecessity, title = {On the necessity of (sometimes) being synthetic. {C}omment on {P}oggiolesi.}, booktitle = {Third Workshop in the Philosophy of Information}, year = {2011}, pages = {63-68}, publisher = {Koninklijke Vlaamse Academie van Belgi{\"e}}, address = {Brussels}, author = {Primiero, Giuseppe}, editor = {Allo, Patrick and Primiero, Giuseppe} } @article {Allo2011, title = {Report 3rd Workshop in the Philosophy of Information}, journal = {The Reasoner}, volume = {1}, number = {5}, year = {2011}, pages = {6-7}, author = {Allo, Patrick and Primiero, Giuseppe} } @conference {1166760, title = {Constructive contextual modal judgments for reasoning from open assumptions}, booktitle = {Proceedings of the Computability in Europe 2010 Conference}, year = {2010}, publisher = {Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores}, organization = {Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores}, abstract = {

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.

}, author = {Primiero, Giuseppe}, editor = {Ferreira, F and Guerra, H and Mayordomo, E and Rasga, J} } @conference {primiero2010multi, title = {A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network.}, booktitle = {Electronic Proceedings of the Federated Logic Conference 2010 (Proof Systems for Program Logics Workshop)}, year = {2010}, publisher = {Citeseer}, organization = {Citeseer}, abstract = {

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.

}, author = {Primiero, Giuseppe} } @conference {810575, title = {A constructive modal semantics for contextual verification}, booktitle = {Proceedings of the First International Workshop on Logic-Based Interpretation of Context: Modeling and Applications}, year = {2009}, publisher = {CEUR-Workshop Proceedings}, organization = {CEUR-Workshop Proceedings}, abstract = {

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.

}, url = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-550/}, author = {Primiero, Giuseppe} } @article {Primiero2009a, title = {An epistemic logic for becoming informed}, journal = {Synthese (KRA Serie)}, volume = {167}, number = {2}, year = {2009}, pages = {363-389}, abstract = {

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.

}, keywords = {Epistemic logic, Logic of justification, Modal logic, Philosophy of information}, issn = {0039-7857}, doi = {10.1007/s11229-008-9413-8}, url = {http://dx.doi.org/10.1007/s11229-008-9413-8}, author = {Primiero, Giuseppe} } @incollection {771936, title = {Epistemic Modalities}, booktitle = {Acts of Knowledge: History, Philosophy and Logic}, series = {Tributes}, volume = {9}, year = {2009}, pages = {207{\textendash}232}, publisher = {College Publications}, abstract = {

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.

}, isbn = {978-1-904987-92-5}, author = {Primiero, Giuseppe}, editor = {Primiero, Giuseppe and Rahman, Shahid} } @conference {Primiero2009, title = {A note on constructive modalities for information}, booktitle = {Logic, Philosophy and History of Science in Belgium. Proceedings of the Young Researchers Days 2008}, year = {2009}, publisher = {Koninklijke Vlaamse Academie van Belgi{\"e}}, organization = {Koninklijke Vlaamse Academie van Belgi{\"e}}, address = {Brussel}, author = {Primiero, Giuseppe}, editor = {Weber, Erik and Libert, Thierry and Marage, Pierre and Vanpaemel, Geert} } @incollection {primieroprioritized, title = {Prioritized Dynamic Retraction Function on Non-monotonic Information Updates}, booktitle = {The Many Sides of Logic}, year = {2009}, pages = {443-463}, publisher = {College Publications}, address = {London}, abstract = {

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.

}, author = {Primiero, Giuseppe}, editor = {Carnielli, Walter A. and Coniglio, Marcelo E. and Loffredo D{\textquoteright}Ottaviano, Itala M.} } @article {734492, title = {Proceeding in abstraction: from concepts to types and the recent perspective on information}, journal = {History and Philosophy of Logic}, volume = {30}, number = {3}, year = {2009}, pages = {257{\textendash}282}, abstract = {

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.

}, issn = {0144-5340}, url = {http://dx.doi.org/10.1080/01445340902872630}, author = {Primiero, Giuseppe} } @incollection {802714, title = {Two type-theoretical approaches to privative modification}, booktitle = {New Frontiers in Artificial Intelligence: JSAI-isAI 2009 Workshops}, year = {2009}, pages = {239{\textendash}258}, publisher = {Springer Verlag}, address = {Berlin, Heidelberg}, abstract = {

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{\textquoteright}s Type Theory to privative modification, which is characteristic of natural language; the third reason is to sketch a positive characterization of privation.

}, isbn = {4-915905-37-3 C3004}, author = {Primiero, Giuseppe and Jespersen, Bj{\o}rn}, editor = {Nakakoji, Kumiyo and Murakami, Yohei and McCready, Eric} } @conference {GiJ:aavc, title = {Adaptive arbitration by variant counting on commutative bases with weights}, booktitle = {Fusion 2008: Proceedings of the 11th International Conference on Information Fusion}, year = {2008}, publisher = {IEEE}, organization = {IEEE}, abstract = {

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.

}, doi = {http://dx.doi.org/10.1109/ICIF.2008.4632371}, author = {Primiero, Giuseppe and Meheus, Joke} } @article {GiJ:mmac, title = {Majority Merging by Adaptive Counting}, journal = {Synthese (KRA Serie)}, volume = {165}, number = {2}, year = {2008}, pages = {203{\textendash}223}, abstract = {

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.

}, doi = {http://dx.doi.org/10.1007/s11229-008-9370-2}, author = {Primiero, Giuseppe and Meheus, Joke} } @article {primieromodel, title = {A model for processing updates with inconsistent information on propositional databases}, year = {2008}, institution = { College Publications}, abstract = {

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.

}, author = {Primiero, Giuseppe} } @conference {GiJ:qmpa, title = {Quasi-merging and Pure-arbitration on Information for the family of Adaptive Logics ADM}, booktitle = {Proceedings of the Workshop on Logic and Intelligent Interaction}, year = {2008}, abstract = {

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.

}, author = {Primiero, Giuseppe and Meheus, Joke}, editor = {van Benthem, Johan and Pacuit, Eric} } @conference {376586, title = {Belief Merging based on Adaptive Interaction}, booktitle = {A Meeting of the Minds, proceedings of the workshop on Logic, Rationality and Interaction}, year = {2007}, publisher = {College Publications}, organization = {College Publications}, isbn = {978-1-904987-48-2}, author = {Primiero, Giuseppe}, editor = {van Benthem, Johan and Shier, Ju and Veltman, Frank} } @conference {376590, title = {On building abstract Terms in Typed Systems}, booktitle = {Logica 2006 Yearbook}, year = {2007}, publisher = {Filosofia Publisher}, organization = {Filosofia Publisher}, abstract = {

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.

}, author = {Primiero, Giuseppe}, editor = {Tomala, O and Honzik, R} } @article {Primiero2007, title = {A modal language for contextual computations}, year = {2007}, month = {June}, abstract = {

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..

}, author = {Primiero, Giuseppe} } @conference {376594, title = {Belief Revision in Constructive Type Theory}, booktitle = {Logica 2005 Yearbook}, year = {2006}, publisher = {Filosofia Publisher}, organization = {Filosofia Publisher}, author = {Primiero, Giuseppe}, editor = {Bilkova, M and Tomala, O} }