Abstract We obtain, for the first time, a modular many-valued semantics for combined logics, which is built directly from many-valued semantics for the logics being combined, by means of suitable universal operations over partial non-deterministic logical matrices. Our constructions preserve finite-valuedness in the context of multiple-conclusion logics, whereas, unsurprisingly, it may be lost in the context of single-conclusion logics. Besides illustrating our constructions over a wide range of examples, we also develop concrete applications of our semantic characterizations, namely regarding the semantics of strengthening a given many-valued logic with additional axioms, the study of conditions under which a given logic may be seen as a combination of simpler syntactically defined fragments whose calculi can be obtained independently and put together to form a calculus for the whole logic, and also general conditions for decidability to be preserved by the combination mechanism.

Abstract Recent compositionality results in logic have highlighted the advantages of enlarging the traditional notion of logical matrix semantics, namely by incorporating non-determinism and partiality. Still, several important properties which are known to be computable for finite logical matrices have not been studied in the wider context of partial non-deterministic matrices (PNmatrices). In this paper, we study how incorporating non-determinism and/or partiality in logical matrices impacts on the computational properties of some natural problems regarding their induced logics and concretely their sets of theorems. We show that, while for some of these problems there is no relevant computational impact, there are problems whose computational complexity increases and still other problems that simply become undecidable. In particular, we show that the problem of checking whether the logics characterized by two finite PNmatrices have the same set of theorems is not decidable. This undecidability result explores the connection between PNmatrices and term-DAG-automata, where the universality problem is known to be undecidable. This link also motivates a final contribution, in the form of a pumping-like lemma, which can be used, in some cases, to show that a given logic cannot be characterized by a finite PNmatrix.

The spread of online reviews and opinions and its growing influence on people’s behavior and decisions boosted the interest to extract meaningful information from this data deluge. Hence, crowdsourced ratings of products and services gained a critical role in business and governments. Current state-of-the-art solutions rank the items with an average of the ratings expressed for an item, with a consequent lack of personalization for the users, and the exposure to attacks and spamming/spurious users. Using these ratings to group users with similar preferences might be useful to present users with items that reflect their preferences and overcome those vulnerabilities. In this article, we propose a new reputation-based ranking system, utilizing multipartite rating subnetworks, which clusters users by their similarities using three measures, two of them based on Kolmogorov complexity. We also study its resistance to bribery and how to design optimal bribing strategies. Our system is novel in that it reflects the diversity of preferences by (possibly) assigning distinct rankings to the same item, for different groups of users. We prove the convergence and efficiency of the system. By testing it on synthetic and real data, we see that it copes better with spamming/spurious users, being more robust to attacks than state-of-the-art approaches. Also, by clustering users, the effect of bribery in the proposed multipartite ranking system is dimmed, comparing to the bipartite case.

Abstract We propose and study a probabilistic logic over an algebraic basis, including equations and domain restrictions. The logic combines aspects from classical logic and equational logic with an exogenous approach to quantitative probabilistic reasoning. We present a sound and weakly complete axiomatization for the logic, parameterized by an equational specification of the algebraic basis coupled with the intended domain restrictions.We show that the satisfiability problem for the logic is decidable, under the assumption that its algebraic basis is given by means of a convergent rewriting system, and, additionally, that the axiomatization of domain restrictions enjoys a suitable subterm property. For this purpose, we provide a polynomial reduction to Satisfiability Modulo Theories. As a consequence, we get that validity in the logic is also decidable. Furthermore, under the assumption that the rewriting system that defines the equational basis underlying the logic is also subterm convergent, we show that the resulting satisfiability problem is NP-complete, and thus the validity problem is coNP-complete.We test the logic with meaningful examples in information security, namely by verifying and estimating the probability of the existence of offline guessing attacks to cryptographic protocols.

We study bribery resistance properties in two classes of reputation-based ranking systems, where the rankings are computed by weighting the rates given by users with their reputations. In the first class, the rankings are the result of the aggregation of all the ratings, and all users are provided with the same ranking for each item. In the second class, there is a first step that clusters users by their rating pattern similarities, and then the rankings are computed cluster-wise. Hence, for each item, there is a different ranking for distinct clusters. We study the setting where the seller of each item can bribe users to rate the item, if they did not rate it before, or to increase their previous rating on the item. We model bribing strategies under these ranking scenarios and explore under which conditions it is profitable to bribe a user, presenting, in several cases, the optimal bribing strategies. By computing dedicated rankings to each cluster, we show that bribing, in general, is not as profitable as in the simpler without clustering. Finally, we illustrate our results with experiments using real data.

We analyze a classical generalized probabilistic satisfiability problem (GGenPSAT) which consists in deciding the satisfiability of Boolean combinations of linear inequalities involving probabilities of classical propositional formulas. GGenPSAT coincides precisely with the satisfiability problem of the probabilistic logic of Fagin et al. and was proved to be NP-complete. Here, we present a polynomial reduction of GGenPSAT to SMT over the quantifier-free theory of linear integer and real arithmetic. Capitalizing on this translation, we implement and test a solver for the GGenPSAT problem. As previously observed for many other NP-complete problems, we are able to detect a phase transition behavior for GGenPSAT.

Fibring is a general mechanism for combining logics that provides valuable insight on designing and understanding complex logical systems. To date, most research on fibring has focused on its model and proof-theoretic aspects, and on transference results for relevant metalogical properties. But we are still far from understanding in full the way mixed reasoning emerges from the logics being combined, which is preventing us from having a fully satisfactory semantics for fibred logics and, consequently, limiting the usability of the general results obtained. In previous work, assuming no shared connectives, we have presented an effective characterization of mixed reasoning in terms of the component logics, taking only variables as hypotheses. Despite these restrictions, the result immediately proved to have very interesting applications. In this article, we extend our previous characterization of mixed reasoning for disjoint fibring to arbitrary non-mixed hypotheses. While still not completely satisfactory, as the characterization still cannot cover reasoning from mixed hypotheses, and even less fibred logics with shared connectives, the result again proves to be extremely useful. We illustrate its power by exploring two meaningful applications. To start with, we provide the first full characterization of conservativity for logics obtained by disjoint fibring, extending the partial results of Schechter (2011). Then, we take a semantic detour and use our characterization of mixed reasoning to show that (disjoint) fibring does not preserve finite (N)valuedness.

We propose an approach for defining labeled natural deduction systems for the class of Peircean branching temporal logics, seen as logics in their own right rather than as sub logics of Ockhamist systems. In particular, we give a system for the logic UB, i.e., the until-free fragment of CTL, and show that it is sound and complete. We also study normalization and discuss how derivations may reduce to a normal form using an appropriate management of proof contexts. Finally, we briefly discuss how to extend our system in order to capture full CTL.

Logical matrices are widely accepted as the semantic structures that most naturally fit the traditional approach to algebraic logic. The behavioral approach to the algebraization of logics extends the applicability of the traditional methods of algeb

The distributed temporal logic DTL is a logic for reasoning about temporal properties of discrete distributed systems from the local point of view of the system's agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. We present a sound and complete labelled tableaux system for full DTL. To achieve this, we first formalize a labelled tableaux system for reasoning locally at each agent and afterwards we combine the local systems into a global one by adding rules that capture the distributed nature of DTL. We also provide examples illustrating the use of DTL and our tableaux system.

DTL is a distributed temporal logic for reasoning about temporal properties of distributed systems from the local point of view of the system's agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. We present a sound and complete labeled tableaux system for future-time DTL. To achieve this, we first formalize a labeled tableaux system for reasoning locally at each agent, which provides a system for full future-time LTL, and afterwards we combine the local systems into a global one by adding rules that capture the distributed nature of DTL.

Much attention has been given recently to the mechanism of fibring of logics, allowing free mixing of the connectives and using proof rules from both logics. Fibring seems to be a rather useful and general form of combination of logics that deserves detailed study. It is now well understood at the proof-theoretic level. However, the semantics of fibring is still insufficiently understood. Herein we provide a categorial definition of both proof-theoretic and model-theoretic fibring for logics without terms. To this end, we introduce the categories of Hilbert calculi, interpretation systems and logic system presentations. By choosing appropriate notions of morphism it is possible to obtain pure fibring as a coproduct. Fibring with shared symbols is then easily obtained by coCarteisan lifting from the category of signatures. Soundness is shown to be preserved by these constructions. We illustrate the constructions within prepositional modal logic. Key words: Logic morphism, combination of logics, fibring, fibred semantics, preservation of soundness, modal logic.