Showing 1–10 of 10 results for author: Maggesi, M

Mechanising Gödel-Löb provability logic in HOL Light

Authors: Marco Maggesi, Cosimo Perini Brogi

Abstract: We introduce our implementation in HOL Light of the metatheory for Gödel-Löb provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem prover for GL itself. The strategy we develop here to formalise the modal completeness proof overcomes the technical difficulty due to the non-compactness of GL and is an adaptation -- accordi… ▽ More We introduce our implementation in HOL Light of the metatheory for Gödel-Löb provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem prover for GL itself. The strategy we develop here to formalise the modal completeness proof overcomes the technical difficulty due to the non-compactness of GL and is an adaptation -- according to the formal language and tools at hand -- of the proof given in George Boolos' 1995 monograph. Our theorem prover for GL relies then on this formalisation, is implemented as a tactic of HOL Light that mimics the proof search in the labelled sequent calculus G3KGL, and works as a decision algorithm for the provability logic: if the algorithm positively terminates, the tactic succeeds in producing a HOL Light theorem stating that the input formula is a theorem of GL; if the algorithm negatively terminates, the tactic extracts a model falsifying the input formula. We discuss our code for the formal proof of modal completeness and the design of our proof search algorithm. Furthermore, we propose some examples of the latter's interactive and automated use. △ Less

Submitted 12 October, 2023; v1 submitted 7 May, 2022; originally announced May 2022.

Comments: Preprint of the paper published in Journal of Automated Reasoning 67 (3) 2023. Please refer to the published paper for the most up-to-date version. arXiv admin note: text overlap with arXiv:2102.05945

MSC Class: 68V15 (Primary) 03F45; 03B16 (Secondary) ACM Class: F.4.1; I.2.3

Journal ref: Journal of Automated Reasoning 67.3 (2023): 29

Universal Algebra in UniMath

Authors: Gianluca Amato, Matteo Calosci, Marco Maggesi, Cosimo Perini Brogi

Abstract: We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted gro… ▽ More We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories, and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by sketching some basic examples from algebra and propositional logic. △ Less

Submitted 22 January, 2025; v1 submitted 11 February, 2021; originally announced February 2021.

MSC Class: 68V15; 03B38; 03B35; 08A70 ACM Class: I.2.3; F.4.1

Journal ref: Math. Struct. Comp. Sci. 34 (2024) 869-891

A formal proof of modal completeness for provability logic

Authors: Marco Maggesi, Cosimo Perini Brogi

Abstract: This work presents a formalized proof of modal completeness for Gödel-Löb provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation, focusing on our choices in structuring proofs which make essential use of the tools of HOL Light and which differ in part from the standard strategies found in main textbooks covering the… ▽ More This work presents a formalized proof of modal completeness for Gödel-Löb provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation, focusing on our choices in structuring proofs which make essential use of the tools of HOL Light and which differ in part from the standard strategies found in main textbooks covering the topic in an informal setting. Moreover, we propose a reflection on our own experience in using this specific theorem prover for this formalization task, with an analysis of pros and cons of reasoning within and about the formal system for GL we implemented in our code. △ Less

Submitted 11 February, 2021; originally announced February 2021.

Extension and tangential CRF conditions in quaternionic analysis

Authors: Marco Maggesi, Donato Pertici, Giuseppe Tomassini

Abstract: We prove some extension theorems for quaternionic holomorphic functions in the sense of Fueter. Starting from the existence theorem for the nonhomogeneous Cauchy-Riemann-Fueter Problem, we prove that an $\mathbb{H}$-valued function $f$ on a smooth hypersurface, satisfying suitable tangential conditions, is locally a jump of two $\mathbb{H}$-holomorphic functions. From this, we obtain, in particula… ▽ More We prove some extension theorems for quaternionic holomorphic functions in the sense of Fueter. Starting from the existence theorem for the nonhomogeneous Cauchy-Riemann-Fueter Problem, we prove that an $\mathbb{H}$-valued function $f$ on a smooth hypersurface, satisfying suitable tangential conditions, is locally a jump of two $\mathbb{H}$-holomorphic functions. From this, we obtain, in particular, the existence of the solution for the Dirichlet Problem with smooth data. We extend these results to the continous case. In the final part, we discuss the octonian case. △ Less

Submitted 25 February, 2020; v1 submitted 27 September, 2019; originally announced September 2019.

Comments: 22 pages

MSC Class: 30G35

Bicategories in Univalent Foundations

Authors: Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide

Abstract: We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicabi… ▽ More We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics. △ Less

Submitted 15 August, 2022; v1 submitted 4 March, 2019; originally announced March 2019.

Comments: v1: 16 pages; v2: Veltri added as coauthor, extended version, 32 pages, list of changes given in Section "Publication history"; v3: final journal version to be published in Mathematical Structures in Computer Science; v4: fixed some typos that remain in the MSCS version

Journal ref: Mathematical Structures in Computer Science (MSCS), 2022

Modular specification of monads through higher-order presentations

Authors: Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi

Abstract: In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of `models', and they give a monadicity result which implies that this category has an initial object, which is the language p… ▽ More In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of `models', and they give a monadicity result which implies that this category has an initial object, which is the language presented by the pair. In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating (`higher-order') operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to $β$- and $η$-equalities. Such a 2-signature is hence a pair $(Σ,E)$ of a binding signature $Σ$ and a family $E$ of equations for $Σ$. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context. We associate, to each 2-signature $(Σ,E)$, a category of `models of $(Σ,E)$; and we say that a 2-signature is `effective' if this category has an initial object; the monad underlying this (essentially unique) object is the `monad specified by the 2-signature'. Not every 2-signature is effective; we identify a class of 2-signatures, which we call `algebraic', that are effective. Importantly, our 2-signatures together with their models enjoy `modularity': when we glue (algebraic) 2-signatures together, their initial models are glued accordingly. We provide a computer formalization for our main results. △ Less

Submitted 3 March, 2019; originally announced March 2019.

Comments: 17 pages

Journal ref: Formal Structures for Computation and Deduction (FSCD) 2019, LIPIcs Vol. 131, pp. 6:1-6:19

Some elementary remarks on lci algebraic cycles

Authors: Marco Maggesi, Gabriele Vezzosi

Abstract: In this short note, we simply collect some known results about representing algebraic cycles by various kind of "nice" (e.g. smooth, local complete intersection, products of local complete intersection) algebraic cycles, up to rational equivalence. We also add a few elementary and easy observations on these representation problems that we were not able to locate in the literature. In this short note, we simply collect some known results about representing algebraic cycles by various kind of "nice" (e.g. smooth, local complete intersection, products of local complete intersection) algebraic cycles, up to rational equivalence. We also add a few elementary and easy observations on these representation problems that we were not able to locate in the literature. △ Less

Submitted 14 December, 2016; originally announced December 2016.

Comments: Notes for students, 7 pages

On the quantum cohomology of Fano bundles over projective spaces

Authors: Vincenzo Ancona, Marco Maggesi

Abstract: In their paper "Quantum cohomology of projective bundles over $P^n$" (Trans. Am. Math. Soc. (1998)350:9 3615-3638) Z.Qin and Y.Ruan introduce interesting techniques for the computation of the quantum ring of manifolds which are projectivized bundles over projective spaces; in particular, in the case of splitting bundles they prove under some restrictions the formula of Batyrev about the quantum… ▽ More In their paper "Quantum cohomology of projective bundles over $P^n$" (Trans. Am. Math. Soc. (1998)350:9 3615-3638) Z.Qin and Y.Ruan introduce interesting techniques for the computation of the quantum ring of manifolds which are projectivized bundles over projective spaces; in particular, in the case of splitting bundles they prove under some restrictions the formula of Batyrev about the quantum ring of toric manifolds. Here we prove the formula of Batyrev on the quantum Chern-Leray equation for a large class of splitting bundles. △ Less

Submitted 16 December, 2000; v1 submitted 7 December, 2000; originally announced December 2000.

Comments: 5 pages, plain TeX. The mistaken identity (4), together with some statements, has been corrected

Minimal resolution of general stable vector bundles on $\PP^2$

Authors: Carla Dionisi, Marco Maggesi

Abstract: We study the general elements of the moduli spaces (\MM_{\PP^2} (r, c_1, c_2) ) of stable holomorphic vector bundle on $\PP^2$ and their minimal free resolution. Incidentally, a quite easy proof of the irreducibility of (\MM_{\PP^2} (r, c_1, c_2)) is shown. We study the general elements of the moduli spaces (\MM_{\PP^2} (r, c_1, c_2) ) of stable holomorphic vector bundle on $\PP^2$ and their minimal free resolution. Incidentally, a quite easy proof of the irreducibility of (\MM_{\PP^2} (r, c_1, c_2)) is shown. △ Less

Submitted 21 February, 2000; originally announced February 2000.

Comments: 8 pages, amslatex

MSC Class: 14F05; 14D20

On the quantum cohomology of blow-ups of projective spaces along linear subspaces

Authors: Marco Maggesi

Abstract: We give an explicit presentation with generators and relations of the quantum cohomology ring of the blow-up of a projective space along a linear subspace. We give an explicit presentation with generators and relations of the quantum cohomology ring of the blow-up of a projective space along a linear subspace. △ Less

Submitted 29 August, 2000; v1 submitted 27 October, 1998; originally announced October 1998.

Comments: Deeply revised with respect to the previous version of 1998