ProofPrinter Class Reference

Class for rendering a proof in various formats. More...

#include <ProofPrinter.hpp>

Public Member Functions
	ProofPrinter ()
	Basic constructor.
	ProofPrinter (vector< StackItem > *_p)
	The constructor yuo want.
void	set_proof (vector< StackItem > *_p)
	Basic set method.
void	clear ()
	Basic set method.
void	make_LaTeX (const path &, const path &, const string &)
	Convert to LaTeX and store in the specified file.
void	make_Prolog (const path &)
	Convert to a form suitable for use by the Prolog proof checker and write to a file.

Detailed Description

Class for rendering a proof in various formats.

A proof is supplied as a stack of StackItem produced by StackProver.

At present, this class will render a proof as LaTeX, or in a Prolog-readable certificate format that can be passed through the Connect++ certificate checker.

It will be extended later if a standard format for connection calculus proof certificates is agreed – this discussion is ongoing.

Constructor & Destructor Documentation

ProofPrinter()

ProofPrinter::ProofPrinter ( vector< StackItem > *  _p )

inline

The constructor yuo want.

Parameters

_p	Pointer to the output of StackProver.

Member Function Documentation

make_LaTeX()

void ProofPrinter::make_LaTeX	(	const path &	path_to_file,
		const path &	path_to_input_file,
		const string &	matrix_as_latex
	)

Convert to LaTeX and store in the specified file.

Parameters

path_to_file	Path of file to store to
path_to_input_file	File for the problem being solved
matrix_as_latex	LaTeX formatted matrix

make_Prolog()

void ProofPrinter::make_Prolog

(

const path &

path_to_file

)

Convert to a form suitable for use by the Prolog proof checker and write to a file.

Parameters

path_to_file

Path for output file

set_proof()

void ProofPrinter::set_proof ( vector< StackItem > *  _p )

inline

Basic set method.

Parameters

_p	Pointer to the output of StackProver.

---

The documentation for this class was generated from the following files:

• ProofPrinter.hpp
• ProofPrinter.cpp