The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Some kind of interface for abstracting congruence is required. This might look something like this:
interface Congruence {
public void unify(Expr lhs, Expr rhs);
public Expr toNormalForm(Expr e);
public Expr[] getAllEquivalents(Expr e);
}
This would be used within a given Proof.State to move any asserted truths into their normal form representation. This includes, for example, applying the range of existing simplifications.
The existing CongruenceClosure is then essentially responsible for deciding how and what to unify. It's not really clear exactly what it would really be responsible for. The key is that we need Congruence to be part of the Proof.State as other rules can infer new truths.
Some different implementations of Congruence are possible. For example:
Allocated formulae / expressions are considered to be normal form. This means, Congruence doesn't need to renormalise allocated items.
Maintain map from items to their normal form representations. In this case, formulae / expressions are presumed to be allocated. Then, we maintain a map from an item to its normal form representation based on its allocation index. The advantage of this is that it avoids a lot of potentially expensive work to simplify expressions. Instead, work is shifted onto the procedure for structrual equivalence testing.
Realistically, it would be nice to support both of the above implementations.
Some kind of interface for abstracting congruence is required. This might look something like this:
interface Congruence { public void unify(Expr lhs, Expr rhs); public Expr toNormalForm(Expr e); public Expr[] getAllEquivalents(Expr e); }This would be used within a given
Proof.Stateto move any asserted truths into their normal form representation. This includes, for example, applying the range of existing simplifications.The existing
CongruenceClosureis then essentially responsible for deciding how and what to unify. It's not really clear exactly what it would really be responsible for. The key is that we needCongruenceto be part of theProof.Stateas other rules can infer new truths.Some different implementations of
Congruenceare possible. For example:Congruencedoesn't need to renormalise allocated items.Realistically, it would be nice to support both of the above implementations.