Let *S* be a semigroup and let c in *S*. On *S* we can define a new binary

operation as follows: for all *x* and *y* in *S*, we have *x+y:=xcy.* It is clear that

(*S*,+) is a semigroup called a variant of* S*.

Let *a,b* in S. We say that *a* and *b* are conjugate if there exist *x,y* in

An automaton semigroup is defined as the semigroup generated by the action of a Mealy automaton. An automatic structure for a semigroup (a concept which emerged in the late 1990s as a generalization of automatic structures for groups as studied by Epstein et al.) describes a semigroup in terms of a regular language of normal forms and synchronous rational relations that describe right-multiplication of elements by generators in terms of those normal forms.

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.

*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.