|
A new formal framework for Stringology is proposed, which consists of
a three-sorted logical theory S designed to capture the
combinatorial reasoning about finite words. A witnessing theorem is
proven which demonstrates how to extract algorithms for constructing
strings from their proofs of existence. Various other applications of
the theory are shown. The long term goal of this line of research is
to introduce the tools of Proof Complexity to the analysis of strings.
A new formal framework for Stringology is proposed, which consists of
a three-sorted logical theory S designed to capture the
combinatorial reasoning about finite words. A witnessing theorem is
proven which demonstrates how to extract algorithms for constructing
strings from their proofs of existence. Various other applications of
the theory are shown. The long term goal of this line of research is
to introduce the tools of Proof Complexity to the analysis of strings.
|
