A carregar...
Publicação
Collapse. An AgITP tool for Equational Logic
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 3.74 MB | Adobe PDF |
Orientador(es)
Resumo(s)
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.
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.
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.
Descrição
Palavras-chave
Automated Theorem Proving Equational Logic Computational Algebra Axiom Simplification