UnderstandingProofs

Proofs

A Proof is a subclass of aprove.verification.theoremprover.TerminationProofs.Proof, which itself extends the inner abstract class DefaultProof inside the aprove.prooftree.Proofs.Proof interface. It is responsible for providing the output for certificates and the end user after the analysis. Typically, each processor has a corresponding inner proof class that extends this.

Key Methods to Override in a Problem Class

1. export()

This method describes how to export the proof to the final proof output for the user. It should contain all important information that is necessary for the user to understand the proof of the corresponding processor, such as what rules have been eliminated and why. Most importantly, it should contain a citation if the processor was published somewhere (including a master or bachelor thesis).

Example:

@Override
public String export(final Export_Util eu, final VerbosityLevel level) {
    if (this.rhs == null) {
        return eu.export("The TRS is right-ground and all right-hand sides can only be evaluated finitely often. Thus, the TRS is terminating "+ eu.cite(Citation.RIGHTGROUND)+".");
    } else {
        return eu.export("The term "+this.rhs+" can be rewritten to "+this.result+". Thus, the TRS is not terminating.");
    }
}

2. Proof Output for Certificates

If you're working with proof certificates, you'll need to implement additional methods to generate the syntax for a proof certificate. If you are not working with proof certificates, you can ignore such methods.