Publications

You can also find my articles here.

Preprints

Computing Certificates in Archimedean Univariate Saturated Quadratic Modules

Published in arXiv, 2026

A new symbolic algorithm to compute sums of squares multipliers (certificates) to witness the membership of non-negative univariate polynomials in a saturated univariate quadratic module is presented. Certificates are first computed in terms of natural generators introduced by Kuhlmann and Marshall for an Archimedean saturated quadratic module; natural generators can be easily read-off from a semialgebraic set. In the univariate case, an Archimedean quadratic module is also a preordering since it is closed under multiplication; certificates have different representations when a polynomial is viewed as a member in a quadratic module versus in a preordering An algorithm is given to compute certificates of natural generators in terms of the original generators; it uses a construction introduced by Kuhlmann, Marshall, and Schwartz known as the ``Basic Lemma’’, which splits the non-negative factors of generators. To compute a quadratic module certificate, certificates of products of natural generators are computed using a detailed case analysis based on the types of natural generators. An implementation of the algorithms proposed in Maple is also discussed. The certificates obtained using this implementation are compared with those generated by RealCertify. We discuss examples where RealCertify is unable to find certificates while the proposed method is successful.

Recommended citation: J. Castellanos Joo and D. Kapur, Computing certificates in archimedean univariate saturated quadratic modules, 2026. arXiv: 2605.18980 [cs.SC]
Download Paper

Computing Certificates of Strictly Positive Polynomials in Archimedean Quadratic Modules

Published in arXiv, 2025

New results on computing certificates of strictly positive polynomials in Archimedean quadratic modules are presented. The results build upon (i) Averkov’s method for generating a strictly positive polynomial for which a membership certificate can be more easily computed than the input polynomial whose certificate is being sought, and (ii) Lasserre’s method for generating a certificate by successively approximating a nonnegative polynomial by sums of squares. First, a fully constructive method based on Averkov’s result is given by providing details about the parameters; further, his result is extended to work on arbitrary subsets, in particular, the whole Euclidean space \(\mathbb{R}^n\), producing globally strictly positive polynomials. Second, Lasserre’s method is integrated with the extended Averkov construction to generate certificates. Third, the methods have been implemented and their effectiveness is illustrated. Examples are given on which the existing software package RealCertify appears to struggle, whereas the proposed method succeeds in generating certificates. Several situations are identified where an Archimedean polynomial does not have to be explicitly included in a set of generators of an Archimedean quadratic module. Unlike other approaches for addressing the problem of computing certificates, the methods/approach presented is easier to understand as well as implement.

Recommended citation: W. Shang, J. A. C. Joo, C. Mou, and D. Kapur, Computing certificates of strictly positive polynomials in archimedean quadratic modules, 2025. arXiv: 2503.11119 [math.AC].
Download Paper

Conference Papers

\(AXD\)Interpolator: A Tool for Computing Interpolants for Arrays with MaxDiff

Published in 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification (CAV 2021), 2021

Several approaches toward quantifier-free interpolation algorithms of theories involving arrays have been proposed by extending the language using a binary function skolemizing the extensionality principle. In FoSSaCS 2021, the last three authors studied the enrichment of the McCarthy’s theory of extensional arrays with a maxdiff operation. This paper discusses the implementation of the interpolation algorithm proposed in FoSSaCS 2021 using the Z3 API. The implementation allows the user to choose iZ3, Mathsat, or SMTInterpol as interpolation engines. The tool returns a formula in SMTLIB2 format, which allows compatibility with model checkers and invariant generators using such a format. We compare our algorithm with state-of-the-art interpolation engines. Our experiments using unsatisfiable formulæ extracted with the model checker UAutomizer show the feasibility of our tool. For that purpose, we used C programs from the ReachSafety-Arrays and MemSafety-Arrays tracks of SV-COMP.

Recommended citation: J. Castellanos Joo, S. Ghilardi, A. Gianola, and D. Kapur, “AXDInterpolator: A tool for computing interpolants for arrays with maxdiff”, in 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification (CAV 2021), CEUR-WS.org, vol. 2908, 2021, pp. 40–52.
Download Paper | Download Slides

A single proof of classical behaviour in da Costa’s \(C_n\) systems

Published in Electronic Notes in Theoretical Computer Science, 2015

A strong negation in da Costa’s systems can be naturally extended from the strong negation \(\neg\) of \(C_1\). In [Newton C. A. da Costa. On the theory of inconsistent formal systems. Notre Dame Journal of Formal Logic, 15(4):497–510, 10 1974] Newton da Costa proved the connectives \(\{\rightarrow, \land, \lor, \neg\}\) in \(C_1\) satisfy all schemas and inference rules of classical logic. In the following paper we present a proof that all logics in the \(C_n\) herarchy also behave classically as \(C_1\). This result tell us the existance of a common property among the paraconsistent family of logics created by da Costa.

Recommended citation: M. Osorio and J. Castellanos Joo, “A single proof of classical behaviour in da Costa’s Cn systems”, Electronic Notes in Theoretical Computer Science, vol. 315, pp. 3–16, Sep. 2015, ISSN: 1571-0661. DOI: 10.1016/j.entcs.2015.06.002
Download Paper

Journal Articles

Equivalence among \(RC\)-type paraconsistent logics

Published in Logic Journal of IGPL, 2017

In this article we review several paraconsistent logics from different authors to ‘close the gaps’ between them. Since paraconsistent logics is a broad area of research, it is possible that equivalent paraconsistent logics have different names. What we meant is that we provide connections between the logics studied comparing their different semantical approaches for a near future be able to obtain missing semantical characterization of different logics. We are introducing the term \(RC\)-type logics to denote a class of logics that extends \(C_\omega\) and satisfies the RC rule.

Recommended citation: M. Osorio and J. Castellanos Joo, “Equivalence among RC-type paraconsistent logics”, Logic Journal of IGPL, jzw065, Jan. 2017, ISSN: 1368-9894. DOI: 10.1093/jigpal/jzw065
Download Paper | Download Bibtex

Weakening and Extending \(\mathbb{Z}\)

Published in Logica Universalis, 2015

By weakening an inference rule satisfied by logic \(daC\), we define a new paraconsistent logic \(daC^{'}\), which is weaker than logic \(\mathbb{Z}\) and \(G^{'}3\), enjoys properties presented in \(daC\) like the substitution theorem, and possesses a strong negation which makes it suitable to express intutionism. Besides, \(daC^{'}\) helps to understand the relationships among other logics, in particular \(daC\), and \(PH1\).

Recommended citation: M. Osorio and J. Castellanos Joo. "Weakening and extending \mathbb{Z}" Logica Universalis, vol. 9, no 3, pp. 383-409, Aug. 2015, ISSN: 1661-8300. DOI: 10.1007/s11787-015-0128-6
Download Paper | Download Bibtex

Theses

Computing Certificates of Members in Archimedean Quadratic Modules in \(A[X]\) and Certifying the Emptiness in Inconsistent Monogenic Archimedean Quadratic Modules in \(A[X_1, ..., X_n]\)

Published in UNM Digital Repository, 2026

Polynomials have been found to be a powerful tool over hundreds of years for modeling problems in numerous applications in science, engineering, medicine, and other domains. In the context of formal methods, polynomials arise in modeling in aerospace software and robotics, cyber-physical and hybrid systems, autonomous vehicles and controllers based on neural networks.

Recommended citation: Castellanos Joo, Jose A.. "Computing Certificates of Members in Archimedean Quadratic Modules in A[X] and Certifying the Emptiness in Inconsistent Monogenic Archimedean Quadratic Modules in A[X_1, ..., X_n]." (2026). https://digitalrepository.unm.edu/cs_etds/144
Download Paper

Implementation of Uniform Interpolation Algorithms

Published in UNM Digital Repository, 2021

This thesis discusses algorithms for the uniform interpolation problem and presents their implementation for the following theories: (quantifier-free) equality with uninterpreted functions (EUF), unit two-variable per inequality (UTVPI), and theoretic aspects for the combination of the two previous theories. The uniform interpolation algorithms implemented in this thesis were originally proposed in (Kapur 2017). Refutational proof-based solutions are the usual approach of many interpolation algorithms (Fuchs et al. 2009; McMillan 2011; McMillan 2004). The approach taken in (Kapur 2017) relies on quantifier-elimination heuristics to construct a uniform interpolant using one of the two formulas involved in the interpolation problem. The latter makes it possible to study the complexity of the algorithms obtained compared to refutational-based solutions which rely on the efficiency of SMT solvers. It is not always possible to find a uniform interpolant for every formula in the combined theory of EUF and UTVPI (Calvanese et al. 2020). Hence, the thesis work implements an algorithm for a subset of formulas in the combined theory in which the existence of uniform interpolants is guaranteed. Additionally, the thesis work implements a Nelson-Oppen interpolation framework (Yorsh and Musuvathi 2005) to combine the uniform interpolating algorithms in previous sections. The implementation uses Z3 (Moura and Bjørner 2008) for parsing purposes and satisfiability checking in the combination component of the thesis. Minor modifications were applied to Z3’s enode data structure in order to label and distinguish formulas efficiently (i.e. distinguish A-part, B-part). The project can easily be integrated into the Z3 solver to extend its functionality for verification purposes using the Z3 plug-in module. The major results of the project are the following:

Recommended citation: Castellanos Joo, Jose A.. "Implementation of Uniform Interpolation Algorithms." (2021). https://digitalrepository.unm.edu/cs_etds/110
Download Paper

Revisitando \(C_1\)

Published in Bibliotecas UDLAP, 2014

Paraconsistent logic is a non-classical logic that formalizes inconsistent but non-trivial theories. Particular features from these systems allow one to describe non-explosive theories in the classical sense, i.e. anything follows from a contradiction, while keeping deducing information from contradictory propositions.

Recommended citation: Castellanos Joo, Jose A.. "Revisitando C_1" (2024). https://catarina.udlap.mx/u_dl_a/tales/documentos/lsi/castellanos_j_ja/
Download Paper