UnderstandingProblems

Problems

A Problem is a subclass of the DefaultBasicObligation class. It is the structure that holds all the necessary information required to prove a specific property.

For example, when proving termination for a term rewriting system (TRS), a Problem class may contain attributes like:

• Rewrite rules: The list of rewrite rules.
• Rewrite strategy: The strategy used to prove termination.
• Start terms: A boolean stating whether we only consider basic start terms.

During the execution of AProVE, we create objects of these problem classes that we then analyze via processors.

Key Methods to Override in a Problem Class

When creating a new Problem class, you will need to override several key methods to ensure the correct functionality. Let us illustrate the most important methods by considering the QTRSProblem class representing ordinary term rewrite systems with some additional set of terms $Q$ (the meaning of $Q$ is irrelevant to understand the examples).

1. getStrategyName()

This method should return the name of the strategy that should be used to analyze the problem. The name returned should match the name of the corresponding strategy within the strategy file, see Understanding Strategy Evaluation and 'the Machine'.

Example:

@Override
public String getStrategyName() {
    if (this.getMaxArity() <= 1) {
        return "qsrs";
    } else {
        return "qtrs";
    }
}

2. getProofPurposeDescriptor()

This method should describe what we are attempting to prove. It returns a string that explains the objective of the proof.

Example:

@Override
public ProofPurposeDescriptor getProofPurposeDescriptor() {
    return new DefaultProofPurposeDescriptor(this, "Termination w.r.t. Q");
}

3. export()

This method describes how to export the problem to the final proof output. It should contain all important information that is necessary for the user to understand the problem, such as the current set of rewrite rules in the case of a TRS problem.

Example:

@Override
public String export(final Export_Util o) {
    final StringBuilder s = new StringBuilder();
    s.append(o.export("Q restricted rewrite system:"));
    s.append(o.cond_linebreak());
    if (this.R.isEmpty()) {
        s.append("R is empty.");
        s.append(o.linebreak());
    } else {
        s.append(o.export("The TRS R consists of the following rules:"));
        s.append(o.cond_linebreak());
        s.append(o.set(this.R, Export_Util.RULES));
        s.append(o.cond_linebreak());
    }

    if (this.Q.getTerms().isEmpty()) {
        s.append("Q is empty.");
        s.append(o.linebreak());
    } else {
        s.append(o.export("The set Q consists of the following terms:"));
        s.append(o.cond_linebreak());
        s.append(o.set(this.Q.getTerms(), Export_Util.RULES));
        s.append(o.cond_linebreak());
    }

    return s.toString();
}

4. equals()

The equals() method should be overridden to ensure that proofs can be reused if the same problem is encountered multiple times. This allows for efficient management of previously proven problems and avoids redundant computations.

Example:

@Override
public boolean equals(final Object oth) {
    if (this == oth) {
        return true;
    }

    if (oth == null) {
        return false;
    }

    if (oth.getClass() != this.getClass()) {
        return false;
    }

    final QTRSProblem other = (QTRSProblem) oth;
    if (!this.R.equals(other.R)) {
        return false;
    }

    return this.Q.equals(other.Q);
}

5. 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. Key methods include:

• getCPFInput()
• getCPFAssumption()

These methods are used to return the components needed to generate the proof certificate. If you are not working with proof certificates, you can ignore these methods.

BasicObligation

The most basic problem class within AProVE is a Basic(Proof)Obligation. Whenever you encounter such a class in AProVE, you can think of it as the skeleton of every problem class.