scienza. Conosci questa disciplina tra matematica e informatica che sta rivoluzionando la nostra vita quotidiana?

Fino al 6 luglio si terrà a Nancy un evento internazionale di ricerca con esperti mondiali di logica e pensiero automatico. L’occasione per spiegare questa specializzazione tra matematica e informatica.

Si tratta di un evento scientifico internazionale organizzato dagli scienziati dell’INRIA e si svolge fino al 6 luglio a Nancy. Esperti di livello mondiale in logica e ragionamento automatico lavorano presso l’Institute for Digital and Cognitive Management Sciences (IDMC).

L’opportunità di interessarsi a un entusiasmante campo di ricerca che ha applicazioni tangibili nella nostra vita quotidiana. Abbiamo posto la domanda a Stefan Merz, direttore della ricerca INRIA e leader del team Veridis.

È una specializzazione tra matematica e informatica. “Fornisce strumenti essenziali per risolvere problemi complessi in modo sistematico e rigoroso“, spiega Stefan Merz.
Il ragionamento automatizzato è un’area dell’informatica che tenta di fornire garanzie su ciò che un sistema o un programma farà o non farà mai. Questa affermazione si basa su prove matematiche.
Per risolvere problemi logici di aritmetica, matematica o geometria utilizziamo teoremi, deduzioni e quindi strategie logiche. Il ragionamento automatizzato utilizza i computer, che utilizzano gli stessi strumenti per risolvere problemi complessi.

La logica e il ragionamento automatico hanno diverse applicazioni in diversi campi. “È facile immaginare, in ambito aeronautico o ferroviario, la necessità di ottenere la certificazione prima di mettere in servizio il software. È importante garantire alcune proprietà correttive, ad esempio che due treni non occupino mai la stessa parte del binario, che la metropolitana si fermi davanti ai ponti o che due aerei mantengano sempre una distanza minima. Al livello più esigente di queste certificazioni, si raccomanda di utilizzare queste tecniche di prova formale per garantire queste proprietà. Abbiamo bisogno di queste tecnologie sofisticate e altamente automatizzate per questi sistemi critici“, spiega il direttore della ricerca dell’INRIA.

Le stesse tecniche vengono utilizzate in sistemi con elevati rischi finanziari, ad esempio nel sistema di archiviazione ed elaborazione online, il cloud. Le imprese devono garantire la disponibilità dei propri servizi, il che è vantaggioso anche per i sistemi bancari.

Nella programmazione, la logica viene utilizzata per scrivere algoritmi e programmi per computer. Il ragionamento automatico consente di verificare la correttezza dei programmi. Può essere utilizzato come parte di un’auto a guida autonoma per garantire sistemi di sicurezza che controllino l’elusione.

Un numero crescente di società di sviluppo software impiega specialisti in metodi formali assistiti da computer per verificare, in particolare utilizzando tecniche di ragionamento automatico, il corretto funzionamento di importanti componenti del computer. Motivo: qualsiasi anomalia può portare a gravi conseguenze.

“Alcuni esperti AE lavorano per GAFAM o per le agenzie spaziali NASA o ESA“, dice Stefan Merz.

Nell’anno 2024, la città di Nancy è stata scelta per ospitare questo evento internazionale. È organizzato da scienziati del Centro Inria e dell’Università della Lorena. I gruppi di ricerca dell’Università della Lorena e del Centro INRIIA sono all’avanguardia nel lavoro scientifico svolto in questo campo.

Organizzare una conferenza di questo tipo è fondamentale per continuare a rendere Nancy un posto forte nei metodi formali, nella verifica di sistemi complessi e nel ragionamento automatico.

Fino al 6 luglio verranno organizzati workshop e conferenze presso l’Istituto di scienze digitali e management cognition (IDMC) di Nancy.