26 research outputs found
Complexity reduction and approximation of multidomain systems of partially ordered data
No full textTwo greedy algorithms for the synthesis and approximation of multidomain systems of partially ordered data are proposed. Given k input partially ordered sets (posets) on the same elements, the algorithms search for the optimally approximating partial orders, minimizing the dissimilarity between the generated and input posets, based on their matrices of mutual ranking probabilities. A general approximation algorithm is developed, together with a specific procedure for approximation over bucket orders, which are the natural choice when the goal is to “condense” the inputs into rankings, possibly with ties. Different loss functions are also employed, and their outputs are compared. A real example pertaining to regional well-being in Italy motivates the algorithms and shows them in action
POSetR: a new computationally efficient R package for partially ordered data
No full textIn this paper, we introduce POSetR, a new R package providing highly efficient routines for the treatment of partially ordered data. After motivating the need for a new package on posets, we describe the main functionalities of POSetR and give hints on its possible use
On Finding the Community with Maximum Persistence Probability
No full textThe persistence probability is a statistical index that has been proposed to
detect one or more communities embedded in a network. Even though its
definition is straightforward, e.g, the probability that a random walker
remains in a group of nodes, it has been seldom applied possibly for the
difficulty of developing an efficient algorithm to calculate it. Here, we
propose a new mathematical programming model to find the community with the
largest persistence probability. The model is integer fractional programming,
but it can be reduced to mixed-integer linear programming with an appropriate
variable substitution. Nevertheless, the problem can be solved in a reasonable
time for networks of small size only, therefore we developed some heuristic
procedures to approximate the optimal solution. First, we elaborated a
randomized greedy-ascent method, taking advantage of a peculiar data structure
to generate feasible solutions fast. After analyzing the greedy output and
determining where the optimal solution is eventually located, we implemented
improving procedures based on a local exchange, but applying different long
term diversification principles, that are based on variable neighborhood search
and random restart. Next, we applied the algorithms on simulated graphs that
reproduce accurately the clustering characteristics found in real networks to
determine the reliability and the effectiveness of our methodology. Finally, we
applied our method to two real networks, comparing our findings to what found
by two well-known alternative community detection procedures
A formal framework for synthesis and verification of logic programs
No full textLecture Notes in Computer Scienc
Synthesis of programs in abstract data types
No full textIn this paper we propose a method for program synthesis from constructive proofs based on a particular proof strategy, we call dischargeable set construction. This proof-strategy allows to build proofs in which active patterns (sequences of application of rules with proper computational content) can be distinguished from correctness patterns (concerning correctness properties of the algorithm implicitly contained in the proof). The synthesis method associates with every active pattern of the proof a program schema (in an imperative language) translating only the computational content of the proof. One of the main features of our method is that it can be applied to a variety of theories formalizing ADT's and classes of ADT's. Here we will discuss the method and the computational content of some principles of particular interest in the context of some classes of ADT's
ESBC: an application for computing stabilization bounds
No full textWe describe the application ESBC to perform the timing analysis of a combinatorial circuit. The circuit is described by formulas of Classical Logic and the delays of propagation of the signals in a gate are represented by a kind of valuation form semantics. ESBC computes the exact stabilization times at which the output signals stabilize
Modelling mercury dynamics in the food web of the Augusta Bay
No full textMercury (Hg) contamination represents a significant environmental and public health challenge, particularly in heavily industrialized marine areas. The Augusta Bay, one of the most polluted marine ecosystems in Southern Italy, exemplifies the urgent need for integrated approaches to understand and mitigate Hg impacts. This study is the first to apply a multi-scale modelling framework to address Hg contamination in this region. By integrating environmental processes, food web dynamics and human health impacts, our analysis provides a comprehensive knowledge of Hg pathways and region-specific risks. The framework combines three advanced models. The HR3DHG model reproduces the transport and transformation of Hg species in seawater and sediments, with outputs validated through experimental data collected during extensive field campaigns. The HR3DHG model outputs are then used as inputs for the INTFISH model, which accurately reproduces Hg concentrations in marine organisms of the Augusta Bay while accounting for feeding habits and ecological interactions. Finally, the BBD model addresses the human health dimension by simulating the internal dynamics of methylmercury and its inorganic metabolites in the human body under chronic exposure scenarios. The experimental data coming from the Augusta Bay and their comparison with the values measured in the Hyogo Prefecture (Japan) allowed us to confirm the robustness and relevance of our results (model validation). This innovative framework devised for the Augusta Bay, offers a powerful tool for assessing ecosystem and human health risks associated with Hg contamination, and supports interventions targeted to mitigate the impacts of Hg pollution in coastal areas
A space efficient implementation of a tableau calculus for a logic with a constructive negation
No full textA tableau calculus for a logic with constructive negation and an implementation of the related decision procedure is presented. This logic is an extension of Nelson logic and it has been used in the framework of program verification and timing analysis of combinatorial circuits. The decision procedure is tailored to shrink the search space of proofs and it is proved correct by using a semantical technique. It has been implemented in C++ language
How to Avoid the Formal Verification of a Theorem Prover
No full textThe purpose of this papers to show a technique to automatically certify answers coming from a nontrustable theorem prover. As an extreme consequence, the development of non-sound theorem provers has been considered and investigated, in order to evaluate their relative e#ciency on particular classes of di#cult theorems
