![]() |
Proof Format |
![]() |
AProVE Help System → Proof Output → | Proof Format |
AProVE is able to export the available proof information to different output formats. Depending on the format, the layout offers different features like links (HTML) or graph images (LaTeX and pdfLaTeX). Information about generating such files you find here.
This is the simplest output format. AProVE just generates a simple text file containing the relevant proof information. The layouts using the export dialog or the command line interface are identical.
A Hyper Text Markup Language file may be opened with a web browser. AProVE's Result Viewer also uses HTML to display the proof result. In the full proof view, links are available which enable navigating inside the proof.
A pdfLaTeX file requires the program "pdflatex" (please look at http://www.tug.org/applications/pdftex/ for more details). If You decide to export a proof result to a file "plus.tex", just call
pdflatex plus.texto generate a pdf file. The .png image files which are generated in the same directory are needed by pdflatex and will be superfluous after executing pdflatex. The pdf file itself may be opened with the Adobe Reader which You can download at http://www.adobe.com/products/acrobat/readstep2.html.
In this case, AProVE generates a LaTeX
file (see http://www.tug.org/
for different LaTeX distributions) and some dotty (.dot) files in the
same specified directory. Dotty files are graph representations of the
Strongly Connected Components which may be encountered in the given
program (see the description of Dependency
Pairs for more details).
By using the command
latex plus.texa device independent (dvi) file is generated.
xdvi -allowshell file.dvi.
dvips -R0 file.dviwhat will generate file.ps.