A carregar...
Publicação
AITP Methods for Maximizing Generality and Tractability of Classes of Algebras
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 2.67 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
This thesis was motivated by the search for new classes of algebras that maximize both
generality (the class contains many important examples) and tractability (the class allows
for deep structural theorems), combining algebra, automated reasoning, and large-scale
computation. A database of nearly 500 classes of algebras was autoformalized from the
literature and organized as a partially ordered set of inclusions. More than 80,000 theorems
were proved with automated theorem provers, many requiring non-trivial proofs. The
work also produced dozens new GAP packages.
In the process, group-theoretic constructions such as verbal and marginal subgroups
were extended to inverse semigroups and related structures, yielding new theorems.
The methods developed show how autoformalization and database techniques can
generate new algebraic classes and enable property transfer between them. The work
toward the original goal—identifying classes that maximize generality and depth—is
more than half complete, and we expect that this goal will soon be achieved, opening one
or more new areas of mathematics.
Esta tese foi motivada pela procura de novas classes de álgebras que maximizem tanto a generalidade (a classe contém muitos exemplos importantes) como a tratabilidade (a classe permite teoremas estruturais profundos), combinando álgebra, raciocínio automatizado e computação em grande escala. Uma base de dados com quase 500 classes de álgebras foi autoformalizada a partir da literatura e organizada como um conjunto parcialmente ordenado de inclusões. Foram demonstrados mais de 80 000 teoremas com recurso a demonstradores automáticos, muitos dos quais exigiram provas não triviais. O trabalho produziu também dezenas de novas bibliotecas GAP. No processo, construções de teoria de grupos, tais como subgrupos verbais e marginais, foram estendidas a semigrupos inversos e estruturas relacionadas, dando origem a novos teoremas. Os métodos desenvolvidos mostram como a autoformalização e as técnicas de bases de dados podem gerar novas classes algébricas e permitir a transferência de propriedades entre elas. O trabalho em direção ao objetivo inicial (identificar classes que maximizem a generalidade e a profundidade ) está mais de metade concluído, e espera-se que este objetivo seja em breve alcançado, abrindo uma ou mais novas áreas da matemática.
Esta tese foi motivada pela procura de novas classes de álgebras que maximizem tanto a generalidade (a classe contém muitos exemplos importantes) como a tratabilidade (a classe permite teoremas estruturais profundos), combinando álgebra, raciocínio automatizado e computação em grande escala. Uma base de dados com quase 500 classes de álgebras foi autoformalizada a partir da literatura e organizada como um conjunto parcialmente ordenado de inclusões. Foram demonstrados mais de 80 000 teoremas com recurso a demonstradores automáticos, muitos dos quais exigiram provas não triviais. O trabalho produziu também dezenas de novas bibliotecas GAP. No processo, construções de teoria de grupos, tais como subgrupos verbais e marginais, foram estendidas a semigrupos inversos e estruturas relacionadas, dando origem a novos teoremas. Os métodos desenvolvidos mostram como a autoformalização e as técnicas de bases de dados podem gerar novas classes algébricas e permitir a transferência de propriedades entre elas. O trabalho em direção ao objetivo inicial (identificar classes que maximizem a generalidade e a profundidade ) está mais de metade concluído, e espera-se que este objetivo seja em breve alcançado, abrindo uma ou mais novas áreas da matemática.