UniCa UniCa News Avvisi Seminario - Doppio seminario di Logica & Informatica

Seminario - Doppio seminario di Logica & Informatica

Autore dell'avviso: Dipartimento di Matematica e informatica

08 maggio 2025
Giovedì 8 Maggio alle ore 15 in Aula II, si terrà un doppio seminario di Logica, su temi strettamente legati anche all’Informatica, ovvero proof-assistants e dimostrazione automatica.

---

Marco Maggesi (Università di Firenze), Explaining Universal Algebra to the computer: Formal Foundations and Emerging Directions

Abstract: Universal algebra reveals the common language behind mathematical structures such as groups, rings, and lattices by describing them solely through operations and equations. The first half of this talk surveys how those ideas have been formalised in proof assistants. The second half turns to ongoing work in univalent foundations: we show how displayed universal algebras, recently implemented in UniMath, assemble complex structures layer-by-layer and open new avenues for constructive mathematics and reusable code. The aim is an accessible overview linking classical intuition with cutting-edge formal tools.


Pierluigi Graziani (Università di Urbino Carlo Bo), How Heavy Is a Light-Looking Proof? Towards a Readability Criterion for Humans and Machines 

Abstract: Previous research has explored criteria for evaluating the simplicity and readability of geometric proofs generated by theorem provers, primarily from a human perspective. In particular, Graziani and Quaresma (2023) examined the simplicity and readability of proofs produced by theorem provers implementing the area method, introducing Geometrographic coefficients to quantify various aspects of proof complexity. Building upon their work, this study extends the analysis by investigating the computational effort involved in the proof process, specifically by measuring CPU time. The objective is to determine whether, within the context of proof generation, the hypothesised human effort corresponds with the machine’s measured computational workload. This comparison might offer valuable insights into improving the readability of machine-generated proofs by jointly taking human cognitive constraints and computational limitations into account.

Ultimi avvisi

Questionario e social

Condividi su:
Impostazioni cookie