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):