Formalizing a Fragment of Combinatorics on Words

(Web Support)
Stepan Holub and
Robert Veroff

June 2017

This page provides Web support for *Formalizing a Fragment of Combinatorics
on Words*, presented at
Computability in Europe 2017.
In particular, we present proofs for two results described in the paper.

Commutation Lemma.

x * y = y * x -> (exists z (Power(x,z) & Power(y,z))).

Periodicity Lemma.
(Period(x,u) & Period(y,u) & -Shorter(u,x * y)) => x * y = y * x.

The proofs presented here were found with the automated theorem proving
program,
Prover9.
We include for each problem the relevant input and output files and also
a separate file with the proof from the output file.
### General Files

The shorter version of the axioms was used to help narrow two of the searches.
### Commutation Lemma

prover9 -f p9header axioms.in Goal01.in

### Periodicity Lemma

The file
Goal02.map describes how the proof is organized
into 9 parts run as follows.
# run with the full axiom set
prover9 -f p9header axioms.in Lemma_1.in
prover9 -f p9header axioms.in Lemma_2.in
prover9 -f p9header axioms.in Lemma_3.in
prover9 -f p9header axioms.in Lemma_4.in
prover9 -f p9header axioms.in Reform_1a.in
prover9 -f p9header axioms.in Reform_2a.in
prover9 -f p9header axioms.in Case1.in
# run with the shortened axiom set (to help narrow the search)
prover9 -f p9header axioms.short Case2a.in
prover9 -f p9header axioms.short Case2.in

9 sets of files (input, output, proof):
- Lemma_1.{in,
out,
pf}
- Lemma_2.{in,
out,
pf}
- Lemma_3.{in,
out,
pf}
- Lemma_4.{in,
out,
pf}
- Reform_1a.{in,
out,
pf}
- Reform_2a.{in,
out,
pf}
- Case1.{in,
out,
pf}
- Case2a.{in,
out,
pf}
- Case2.{in,
out,
pf}