305,557 research outputs found
Does every recursively enumerable set admit a finite-fold diophantine representation?
No full textThe Davis-Putnam-Robinson theorem showed that every partially computable m-ary function f(a_1, . . . , a_m) = c on the natural numbers can be specified by means of an exponential Diophantine formula involving, along with parameters a_1, . . . , a_m, c, some number k of existentially quantified variables. Yuri Matiyasevich improved this theorem in two ways: on the one hand, he proved that the same goal can be achieved with no recourse to exponentiation and, thereby, he provided a negative answer to Hilbert's 10th problem; on the other hand, he showed how to construct an exponential Diophantine equation specifying f which, once a_1, . . . , a_m have been fixed, is solved by at most one tuple of values for the remaining variables. This latter property is called single-foldness. Whether there exists a single- (or, at worst, finite-)fold polynomial Diophantine representation of any partially computable function on the natural numbers is as yet an open problem. This work surveys relevant results on this subject and tries to draw a route towards a hoped-for positive answer to the finite-fold-ness issue
“La vendetta allegra”. Adolfo Omodeo e la storia del Cattolicesimo dell’Ottocento
No full textIl saggio intende analizzare il rapporto altalenante dello storico Adolfo Omodeo per la storia religiosa dell'Ottocento, nel contesto culturale e politico in cui matura
Preface to the Proceedings of the 34th Italian Conference on Computational Logic (CILC 2019)
No full textThe 34th edition of the Italian Convention of Computational Logic (CILC 2019), the annual meeting of GULP (Gruppo ricercatori e Utenti Logic Programming), was hosted by the University of Trieste from June 19th to June 21st, 2019.
CILC was originally meant to be a forum for exchanging ideas and experiences between Italian researchers in the field of computational logic, however, in recent years, it has broadened its topics of interest also to a wide set of related areas spacing from verification of formal systems to knowledge representation.
The technical program of CILC 2019 features 37 presentations of as many high-quality papers; 27 of them are included in these proceedings and the remaining ones appeared or were submitted to other conferences, workshops or journals. Each of the submitted papers was evaluated by three reviewers and, according to their judgments, was either accepted or rejected for the presentation and publication in the proceedings.
The contributions address different topics related to computational logic, including verification and validation, temporal reasoning, description logics, formal methods in AI, knowledge representation, and constraint logic programming.
The program was also enriched by an ambassador talk “DigForASP: A European Cooperation Network for Logic-based AI in Digital Forensics” by Stefania Costantini, Francesca Alessandra Lisi, and Raffaele Olivieri and 3 tutorials:
– The SATisfiability problem and its impact
Agostino Dovier, Università degli Studi di Udine
– Multiagent Epistemic Planning
Enrico Pontelli, New Mexico State University
– Model checking: The interval way
Angelo Montanari, Università degli Studi di Udine
The following works were presented at CILC 2019, but are not included in this proceedings:
– Epistemic Answer Set Programming: a new perspective
Ezgi Iraz Su
– Extending ALC with the power-set construct
Laura Giordano and Alberto Policriti
– Accountable Protocols in Abductive Logic Programming
Marco Gavanelli, Marco Alberti, and Evelina Lamma
– Model Completeness, Covers and Superposition (Abridged Version)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, and
Andrey Rivkin
– Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, and Maurizio
Proietti
– An Ontology to Improve the First Aid Service Quality
Lorenzo De Lauretis and Stefania Costantini
– An ASP-based Approach for Optimizing DLV Evaluation
Carlo Allocca, Francesco Calimeri, Roberta Costabile, Alessio Fiorentino,
Nicola Leone, Marco Manna, Simona Perri, and Jessica Zangari
– Large Scale DLV: Preliminary Results
Nicola Leone, Carlo Allocca, Mario Alviano, Francesco Calimeri, Cristina
Civili, Roberta Costabile, Bernardo Cuteri, Alessio Fiorentino, Davide Fusc`a,
Stefano Germano, Giovanni Laboccetta, Marco Manna, Simona Perri, Kristian Reale, Francesco Ricca, Pierfrancesco Veltri, and Jessica Zangari
– A Process Algebra for (Delimited) Persistent Stochastic Non-Interference
Andrea Marin, Carla Piazza, and Sabina Rossi
– Accountability, Responsibility, and Robustness in Agent Organizations
Matteo Baldoni, Cristina Baroglio, and Roberto Micalizio
We would like to thank all the people who have contributed to the success of CILC 2019: the authors, the invited speakers, the program committee, the reviewers, and the participants. Special thanks go to both the President and the former President of GULP, Stefania Costantini and Agostino Dovier, and to the secretary of GULP, Fabio Fioravanti, for their support in the organization of the event
Omodeo Adolfo
No full textLa voce ricostruisce il contributo di Adolfo Omodeo alla tradizione politica del liberalismo italian
Adolfo Omodeo. Storiografia e pensiero politico
No full textIl libro propone una ricostruzione integrale del percorso teorico di Adolfo Omodeo, dai primi scritti sul cristianesimo antico alla peculiare concezione dello storicismo. Scritto anche sulla base del materiale inedito conservato presso l'archivio personale, il volume colloca la figura di Omodeo nel contesto dell'idealismo italiano della prima metà del secolo, con riferimento particolare alla filosofia di Gentile e di Croce
Polynomial-time satisfiability tests for boolean fragments of set theory
No full textWe recently undertook an investigation aimed at identifying
small fragments of set theory (which in most cases are sublanguages
of Multi-Level Syllogistic) endowed with polynomial-time satisfiability
decision tests, potentially useful for automated proof verification. Leaving
out of consideration the membership relator ∈ for the time being, in
this note we provide a complete taxonomy of the polynomial and the
NP-complete fragments involving, besides variables intended to range
over the von Neumann set-universe, the Boolean operators ∪, ∩, , the
Boolean relators ⊆, /⊆, =, /=, and the predicates ‘· = ∅’ and ‘Disj(·, ·)’,
meaning ‘the argument set is empty’ and ‘the arguments are disjoint
sets’, along with their opposites ‘· /= ∅’ and ‘¬Disj(·, ·)’
Croce e Adolfo Omodeo: l’altro autore della «Critica»
No full textDal 1928, quando apparve sulla «Critica» una recensione al libro di Luigi Russo (1892-1961) su Francesco De Sanctis e la cultura meridionale, fino al 1946, con l’articolo su Metodo dialettico e metodo naturalistico nella sto-ria, Adolfo Omodeo rappresentò (con la compagnia di pochi altri) il colla-boratore più stretto di Benedetto Croce, «e quasi l’uno dei due suoi autori» (Nuove pagine sparse, 1° vol., 1966, p. 54), nel diuturno lavoro per la picco-la rivista bimestrale dalla copertina arancione: la quale, come si sa, il 20 di tutti i mesi dispari uscì regolarmente, nonostante le minacce e le intimida-zioni, e contribuì non poco a orientare gli animi nel triste ventennio della dittatura fascista. Come Croce scrisse, ricordando il lungo sodalizio, si trat-tava di una «fraternità d’armi», di una «relazione quasi quotidiana», fatta dei semplici gesti dello «studiare allo stesso tavolo» (p. 57) e dello scambiarsi reciproche osservazioni su pensieri e scritti che l’uno porgeva all’altro. Si trattava, per altro, dell’incontro fra due personalità molto diverse, non solo per età (Croce era nato nel 1866, Omodeo il 18 agosto del 1889) ma anche per formazione e carattere: una differenza che l’amicizia non cancellò, tanto che, dissipate le nubi della guerra e del fascismo, nell’ultimo biennio (tra il 25 luglio del 1943 e la morte di Omodeo, il 28 aprile 1946) sfociò in un contrasto politico, destinato a toccare, oltre l’immediata azione pratica, an-che non secondari orientamenti ideali
Filippo Càssola e il circolo Adolfo Omodeo
No full textAppartiene all’eredità intellettuale e materiale di Filippo Càssola anche la creazione di un circolo politico, che egli scelse di chiamare con il nome di Adolfo Omodeo, autore di una storia magistrale del Risorgimento Italiano, ispiratore della vigorosa rinascita culturale dell’Italia antifascista e precoce anticipatore di una comunità europea. Nello spirito di questi ideali, Càssola, autorevole conoscitore delle libertà e dei diritti del mondo antico e moderno, come emerge da tutta la sua prestigiosa produzione scientifica, ispirò molti studiosi e appassionati ad occuparsi di argomenti orientati verso le problematiche civili e politiche più attuali, soprattutto in relazione ai delicati problemi della questione adriatica, del resto non ancora risolti.Belongs to the intellectual heritage and material of Filippo Càssola also the creation of a political circle, that he chose to call with the name “Adolfo Omodeo”, the author of a masterful history of the Italian Risorgimento, the inspirer of vigorous cultural rebirth of the anti-Fascist Italy and early anticipator of a European Community. In the spirit of these ideals, Càssola, authoritative connoisseur of the freedom and rights of the ancient world and modern, as emerges from the whole of its prestigious scientific production, inspired many scholars and enthusiasts to deal with topics oriented toward issues and civil and political more current, especially in relation to the delicate problems of the Questione Adriatica, the rest is not yet solved
Theory-specific automated reasoning
No full textIn designing a large-scale computerized proof system, one is often confronted with issues of two kinds: issues regarding an underlying logical calculus, and issues that refer to theories, either specified axiomatically or characterized by indication of either a privileged model or a family of intended models. Proof services related to the theories most often take the form of satisfiability decision or semi-decision procedures (in a sense, polyadic inference rules), while some of the services offered by the calculus (e.g., the Davis-Putnam propositional satisfiability checker) provide low-level mechanisms for integrating services of the former kind. Integration among services can ensure speed-up (i.e., lower number of steps) in the proofs, but it must always be legitimatized by a conservativeness result. Interoperability among proof checkers and autonomous theorem provers is another key point of integration.
In discussing these and related issues, this paper refers to Set Theory as the unifying background, and to a specific proof-checker based ona slightly unorthodox formalization of it as an arena for experimentation
Angelo Omodeo tecnocrate riformista. Bonifica integrale e Mezzogiorno al primo Congresso Veneto delle bonifiche (1922)
No full textIl saggio ricostruisce il contributo di Angelo Omodeo al primo Congresso veneto delle bonifiche avvenuto nel 1922L'intervento di Angelo Omodeo al convegno del 1922 intese mettere in luce le tesi innovative dell'ingegnere idrologo sulla gestione delle acque nel Mezzogiorno e in Sardegna in particolare modo anche in relazione alle prospettive di sviluppo industriale che l'industria idroelettrica avrebbe potuto assicurare al Meridione d'Italia
- …
