Publicação
Collapse. An AgITP tool for Equational Logic
| datacite.subject.fos | Ciências Naturais | |
| dc.contributor.advisor | Araújo, João | |
| dc.contributor.author | Duarte, Henrique Maria de Abreu Lopes e Teixeira | |
| dc.date.accessioned | 2026-03-24T19:36:13Z | |
| dc.date.available | 2026-03-24T19:36:13Z | |
| dc.date.issued | 2025-11-25 | |
| dc.description.abstract | The simplification of axiomatic systems is a fundamental challenge in computational algebra, with significant implications for equational reasoning and automated theorem proving. Reducing sets of axioms to their minimal forms, while preserving their equiva- lence , is both an intellectually stimulating and computationally demanding problem. This thesis presents Collapse, a novel tool built within the framework of Augmented Intelligence Theorem Proving (AgITP), expanding the ProverX ecosystem. The tool is designed to take as an input a set of axioms defining a class of algebras and produce a smaller, yet equivalent, set of axioms. This reduction process requires several algorithms and transformations to be applied in order to balance efficiency and accuracy. To validate its utility, the tool is applied to identify reduced bases for inverse semigroups—a classic yet non-trivial algebraic structure. The challenge lies in generalizing this approach to other well-documented classes of algebras. By automating the simplification process, Collapse offers a systematic method to streamline equational reasoning. | eng |
| dc.description.abstract | A simplificação de sistemas axiomáticos é um desafio fundamental na álgebra compu- tacional, com implicações significativas para o raciocínio equacional e a demonstração automática de teoremas. Reduzir conjuntos de axiomas às suas formas mínimas, man- tendo a equivalência, é um problema ao mesmo tempo intelectualmente estimulante e computacionalmente exigente. Esta dissertação apresenta o Collapse, uma ferramenta inovadora desenvolvida no âmbito de AgITP, expandindo o ecossistema ProverX. A ferramenta foi concebida para receber como entrada um conjunto de axiomas que define uma classe de álgebras e produzir um conjunto menor, mas equivalente, de axiomas. Este processo de redução exige a aplicação de diversos algoritmos e transformações para equilibrar eficiência e precisão. Para validar a sua utilidade, a ferramenta é aplicada na identificação de bases reduzidas para semigrupos inversos—uma estrutura algébrica clássica, mas não trivial. O desafio reside em generalizar esta abordagem para outras classes de álgebras bem documentadas. Ao automatizar o processo de simplificação, o Collapse oferece um método sistemático para otimizar o raciocínio equacional. | por |
| dc.identifier.uri | http://hdl.handle.net/10362/201797 | |
| dc.language.iso | eng | |
| dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | |
| dc.subject | Automated Theorem Proving | |
| dc.subject | Equational Logic | |
| dc.subject | Computational Algebra | |
| dc.subject | Axiom Simplification | |
| dc.title | Collapse. An AgITP tool for Equational Logic | eng |
| dc.type | master thesis | |
| dspace.entity.type | Publication | |
| thesis.degree.name | MASTER IN MATHEMATICS AND APPLICATIONS. SPECIALIZATION IN PURE MATHEMATICS |