Friday 15 June 2012

Theorem linker

 

THEOREM LINKER

v 0.5

Description

Theorem Linker creates graphs to depict dependencies between theorems in papers.

With a paper written using LaTeX, Theorem Linker will:
  1. Find all theorem types (ex: lemma, corollary, theorem, or anything using the \newtheorem{} command)
  2. Find all theorems and their respective proofs in the paper
  3. Inside each proof, find all references to other theorems
  4. Create a graph with vertices to represent all the different theorems, and directed edges to represent all references.
A path highlighted in red describes the longest path in the graph.
Two folders are created:
  • SingleLevel, which contains a graph for each theorem in the paper, each graph displaying only the direct references to and from the specific theorem
  • MultiLevel, also containing one graph for each theorem, and each graph showing all ancestor and descendant theorems of the specific theorem.

All graphs are files written in a .dot file (to be opened with programs such as Graphviz or OmniGraffle) that will display each theorem as a node, with directed edges to describe the relations between the theorems.

There is a package (thmlinker.sty) available for download to be used alongside a LaTeX paper. The package allows two commands and an environment to be used when writing a paper.
  • \noref{} is used for making references in a proof, where a reference shouldn't be explicitly written out, for stylistic or other reasons
  • \delref{} is similar to \noref, only with delref, references are checked by the LaTeX compiler. Using delref ensures that there are no typos in silent references, however its disadvantage is sometimes it can cause formatting errors when not being used in a paragraph of text
  • \begin{proofblock} and  \end{proofblock} can be put around any block of text to create a "proof" environment for a theorem. This is useful for wrapping previous proofs in a paper that did not use \begin{proof} or did not have it defined. It can also be use to designate what a theorem a proof is referring to if they are not in order. Simply use \begin{proofblock}[label], where "label" is the label of the theorem you wish the proof to belong to.
    NOTE \begin{proofblock} does not provide any formatting at the beginning or ends of a proof. This allows it to be used easily in conjunction with other pre-existing environments.

 

Source code

Download Latest Version of Theorem Linker! 
thmlinker.sty package for tex documents
thmlink is a program written in C, and is compiled with gcc 

 

 License 

Theorem Linker is distributed under the GPL v3.0.
Feel free to use this program on any papers you have written, or alongside with any you will write.

 

Directions

  1. Compile .tex paper using a LaTeX compiler (so that .aux file will be produced)
  2. Compile thmlink program if it hasn't been done already (see readme file)
  3. run thmlink with the .tex paper as an argument (see readme file)
  4. Open .dot graph file (with Graphviz or OmniGraffle) to see produced graph.

 

Notes

While Theorem Linker can handle  many different papers, they should be written similar to the outline seen in 'Example Usage' to guarantee that it will work.
All theorems should have a label. A label is needed when making a reference, however it should be there even when there is no reference to a theorem. It will help make the graph more understandable to anyone reading it.

 

Example Usage

Here is an example document (be sure to download thmlinker.sty and put it in the same folder) to try to use thmlink on. In the end, a graph such as this should be produced:


A document can be written in a form like this to work:


\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}

...
 
\begin{document}

...

\begin{lemma} \label{firstlem}
Lemma description
\end{lemma}
...

\begin{proof}
proof of the previous lemma
\end{proof}

\begin{thm}
\label{theoremA}
Theorem description
\end{thm} 

\begin{proof}
proof of theorem, with references \ref{firstlem}
\end{proof}

...

\end{document}

Contact

Nicolas Lefebvre

No comments:

Post a Comment