An automatic presentation (also called an FA-presentation) is a description of a relational structure using regular languages. The concept an FA-presentation arose in computer science, to fulfil a need to extend finite model theory to infinite structures. Informally, an FA-presentation consists of a regular language of abstract representatives for the elements of the structure, such that each relation (of arity $n$, say) can be recognized by a synchronous $n$-tape automaton.

Prover9 is the offspring of a automated theorem prover family for first order logic with equality that started with ”Otter” and ”EQP”. It is a widely used math tool but its outputs are cumbersome and difficult to understand. Xplain2 is a translator that intends to give a much more pleasent and comprehensible version of the proofs generated by Prover9 while trying to close the gaps between some holes left by its ancestor, the former Xplain.

This talk presents a webpage that, given a finite semigroup S as input, either by entering its multiplication table, presentation using Prover9 syntax, or GAP smallsemi ID, will return: the representative in the isomorphism class of S, whose vector is lexicographically the least; a basis for the variety var(S), if var(S) = var(B) for some variety whose identification system is available in the variety database. The repository includes presently all varieties generated by semigroups up to order five, and the non-finitely based semigroups of order six.

*The working mathematician is confronted often with a new model or a new theory whose connections with other parts of mathematics are not known. The goal of this project is to produce one Library of models, axiomatics and results that in the end will allow any mathematician to automatically find the connections to pats of the literature of his model or of his brand new theory.We use automated reasoning to carry this task out.*

This talk aims to show a prototype of an application that extends Prover9/Mace functionality by adding Python scripting.

These are the first results of an ongoing PhD thesis in Computational Algebra at Universidade Aberta.

The modular architecture will be introduced first, followed by a small demonstration of the application and how it can be easily extended with scripts.

A version running on a web server will also be demonstrated.

The systematic study of spherical tilings goes back to 1924 ([2], p.467) but

their combinatorial classification is yet an open problem. Our aim is the development of computational GeoGebra tools enhancing the research on spherical tilings.

The cyclic shift graph of a monoid is the graph whose vertices are the elements of the monoid and whose edges connect elements that differ by a cyclic shift. For several monoids arising from combinatorial objects like the plactic (Young tableaux) and the sylvester (binary search trees) two elements differ by a sequence of cyclic shifts if and only if they have the same number of each of its composing symbols (that is, the same evaluation). Therefore, the connected components of the cyclic graph for these monoids consist of the elements that have the same evaluation.

Currently there are several theorem provers, but their proof finding performance is highly sensitive to the problem we are working on.

GeoGebra, a software system for dynamic geometry and algebra in the plane, since its inception in 2001, has gone from a dynamic geometry software (DGS), to a powerful computational tool in several areas of mathematics. Powerful algebraic capabilities have joined GeoGebra, an efficient spreadsheet that can deal with many kinds of objects, an algebraic and symbolic calculation system and several graphical views that expand the possibility of multidimensional representations. The recent 3D features allow more intuitive interaction with three-dimensional objects.

This communication presents two packages, Ming and Collapse, that were created using Prover9/Mace4 as an oracle and one that manipulates Prover9's proof, sP9. Ming has the goal of finding the bases of a given set of axioms, Collapse search for a new axiom of a theory that substitutes a given set of axioms of that theory and SP9 tries to reduce the length of a Prover9 proof.