arXiv subjects

Marco Pérez

Publications and source records attributed to Marco Pérez.

5 recordsLinked to original sources

arXiv2026

Towards Relating Ciao Assertions and LPTP Theorems

Abstract interpretation-based verification is a central component of the Ciao Prolog system, enabling expressive specifications of properties of programs, predicates, and execution states. Independently, the LPTP (Logic Programming Theorem Proving) framework offers a first-order logical formalism for expressing and proving properties of predicates. In this paper, we address a fundamental issue in relating these two frameworks: studying the translation of Ciao assertions into LPTP formulae and identifying a partial correspondence between assertion-based and logic-based specifications. We introduce a systematic translation scheme, characterize assertion classes according to their logical encodability, and propose approximation strategies and auxiliary constructs for non-translatable cases, and finally analyze the resulting soundness and completeness trade-offs. We argue that our proposal enables a tight integration of Ciao's assertion checking with LPTP-based deductive verification, thereby leveraging their complementary capabilities.

cs.PL↗

arXiv2014

Adjointness properties for relative extensions of disk and sphere chain complexes

We study the subgroup $\mathcal{E}xt^i_{\mathcal{C}}(\mathcal{F}; C, D)$ of $\mathcal{E}xt^i_{\mathcal{C}}(C,D)$ formed by those $i$-extensions of $C$ by $D$ in an Abelian category $\mathcal{C}$ which are ${\rm Hom}_{\mathcal{C}}(\mathcal{F},-)$-exact, and present a Baer-like description of this subgroup in terms of certain right derived functors of ${\rm Hom}_{\mathcal{C}}(-,-)$. We also study adjointness properties of these subgroups and the disk and sphere chain complex functors $\mathcal{C} \longrightarrow \textbf{Ch}(\mathcal{C})$, given by a collection of natural isomorphisms which generalize the corresponding adjointness properties proven by J. Gillespie for $\mathcal{E}xt^i(-,-)$.

math.CT↗

arXiv2014

Gorenstein Homological Dimensions and Abelian Model Structures

We construct new complete cotorsion pairs in the categories of modules and chain complexes over a Gorenstein ring $R$, from the notions of Gorenstein homological dimensions, in order to obtain new Abelian model structures on both categories. If $r$ is a positive integer, we show that the class of modules with Gorenstein-projective (or Gorenstein-flat) dimension $\leq r$ forms the left half of a complete cotorsion pair. Analogous results also hold for chain complexes over $R$. In any Gorenstein category, we prove that the class of objects with Gorenstein-injective dimension $\leq r$ is the right half of a complete cotorsion pair. The method we use in each case consists in constructing a cogenerating set for each pair. Later on, we give some applications of these results. First, as an extension of some results by M. Hovey and J. Gillespie, we establish a bijective correspondence between the class of differential graded $r$-projective complexes and the class of modules over $R[x] / (x^2)$ with Gorenstein-projective dimension $\leq r$, provided $R$ is left and right Noetherian with finite global dimension. The same correspondence is also valid for the (Gorenstein-)injective and (Gorenstein-)flat dimensions.

math.CT↗

arXiv2014

Homological dimensions and abelian model structures on chain complexes

We construct Abelian model structures on the category of chain complexes over a ring $R$, from the notion homological dimensions of modules. Given an integer $n > 0$, we prove that the left modules over a ringoid $\mathfrak{R}$ with projective dimension at most $n$ form the left half of a complete cotorsion pair. Using this result we prove that there is a unique Abelian model structure on the category of chain complexes where the exact complexes are the trivial objects and the complexes with projective dimension at most $n$ form the class of trivially cofibrant objects. In the paper "Cotorsion pairs in C($R$-Mod)", the authors construct an Abelian model structure on chain complexes, where the trivial objects are the exact complexes and the class of cofibrant objects is given by the complexes whose terms are all projective. We extend this result by finding a new Abelian model structure with the same trivial objects and where the cofibrant objects are given by the class of complexes whose terms are modules with projective dimension at most $n$. We also prove similar results concerning the flat dimension.

math.CT↗

arXiv2012

Degreewise n-projective and n-flat model structures on chain complexes

In the paper "Cotorsion Pairs in C(R-Mod)", the authors construct an abelian model structure on the category of chain complexes Ch(R), where the class of cofibrant objects is given by the class of degreewise projective chain complexes. Using a generalization of a well known theorem by I. Kaplansky, we generalize the method used in that paper in order to obtain, for each integer n>1, a new abelian model structure on Ch(R), where the class of cofibrant objects is the class of chain complexes whose terms have projective dimension smaller or equal than n (dw-n-projective complexes), provided the ring R is noetherian. We also present another method, based on the paper "Covers and Envelopes in Grothendieck Categories: Flat Covers of Complexes with Applications", to construct this model structure. This method also works to construct an abelian model structure whose cofibrant objects are the dw-n-flat complexes.

math.CT↗