João Araújo

A forbidden substructure theorem characterizes a class of mathematical objects within an overclass through a list of forbidden substructures. One typical example of such a theorem is: a graph is bipartite if and only if it does not contain cycles of odd length. At the conference on Artificial Intelligence Theorem Proving (AITP) in 2020, Wesley Fussner presented a forbidden substructure theorem for lattices, found using a combination of AITP tools and proofs by hand; he concluded by conjecturing that it should be possible to develop a fully autonomous AITP tool capable of conjecturing and proving forbidden substructure theorems without human intervention. The goal of this paper is to answer that conjecture in the affirmative. After introducing the algorithm behind our tool, we demonstrate its power by proving many new forbidden substructure theorems. In particular, a recent paper provides the partially ordered set of all lazy magma (groupoid) varieties. Our tool, working in fully autonomous mode, managed to derive a forbidden substructure theorem for each inclusion in that paper. This tool is available to any mathematician on a free online website. The paper ends with a list of open problems.

[Context] Software requirements are mainly specified using natural language, which is prone to produce ambiguous specifications. This challenge becomes bigger when dealing with requirements that must comply with regulations, the so-called legal requirements. [Objectives] This work investigates the state of practice to tackle ambiguity of legal requirements. The goal is to identify the factors that help or harm ambiguity resolution of legal requirements in companies that need to comply with data protection laws. [Methods] A qualitative study, based on semi-structured interviews, was performed with twenty-two Brazilian IT professionals, from eighteen companies, to gather their views on how to deal with ambiguity resolution of legal requirements. The interview data were recorded, transcribed, and analyzed using qualitative coding techniques, including open and axial coding. [Results] Findings reveal that ambiguity resolution involves the participation of many actors, including the development team, customer, and specialized support areas (Legal, Ambiguity analysis, or Anonymity Sector), also considering the involvement of experienced team members and domain experts. This study also brings a set of factors that positively or negatively influence the quality of legal requirements specifications. [Conclusion] These positive and negative factors, the practices to elicit and specify legal requirements, as well as, the practices to reduce ambiguity in such requirements, can be used as a guide for companies concerned with data protection laws compliance.

This study enhances agile development by integrating BPMN modeling with automated functional requirements elicitation. It focuses on extracting user stories and Gherkin scenarios from BPMN process models using transformation patterns and templates. A tool was developed to automate this process, validated through qualitative expert evaluation, confirming its utility and accuracy. The approach enhances organizational communication and collaboration between business and information technology teams, improving efficiency in requirements elicitation. Future enhancements aim to broaden transformation patterns and tool functionalities to encompass additional BPMN artifacts. This study emphasizes innovation in bridging business process modeling and agile development, highlighting advancements in automating requirements elicitation.

Marginal subgroups, introduced by P. Hall, are characteristic subgroups induced by group words. The goal of this paper is to extend the notion to inverse semigroups. Our first main result establishes that these marginal subsemigroups are full inverse subsemigroups. We then examine the special case in which the word is the commutator, showing that the induced marginal inverse subsemigroup coincides with the metacenter, which is a normal inverse subsemigroup. In the process we prove some results about commutators in inverse semigroups and in Clifford semigroups. The paper concludes with several open problems.

Complete enumeration of finite models of first-order logic (FOL) formulas is pivotal to universal algebra, which studies and catalogs algebraic structures. Efficient finite model enumeration is highly challenging because the number of models grows rapidly with their size but at the same time, we are only interested in models modulo isomorphism. While isomorphism cuts down the number of models of interest, it is nontrivial to take that into account computationally. This paper develops a novel algorithm that achieves isomorphism-free enumeration by employing isomorphic graph detection algorithm nauty, cube-based search space splitting, and compact model representations. We name our algorithm cube-based isomorph-free finite model finding algorithm (CBIF). Our approach contrasts with the traditional two-step algorithms, which first enumerate (possibly isomorphic) models and then filter the isomorphic ones out in the second stage. The experimental results show that CBIF is many orders of magnitude faster than the traditional two-step algorithms. CBIF enables us to calculate new results that are not found in the literature, including the extension of two existing OEIS sequences, thereby advancing the state of the art.