# Programmatically checking equivalence of statements

So as part of a theorem-prover/checker, I'm using Prolog to try to determine the equivalence of statements that have been parsed into tree form, e.g. $x=2$ is represented as eq(x,2), or $x=2 \land y\leq z$ if and(eq(x,2),leq(y,z)), and I want to determine if these statements are equal.

The way I'm currently (attempting) to do this is by trying to convert statements to some normal form, e.g. converting all greater-than statements to less-than statements, or eq(x,x) simplifies to true, and then statements would be compared syntactically to determine equivalence. However, this feels like it might be a tad tricky/complicated, and to some extent I'm a bit uncomfortable simply using syntax rather than semantics to determine whether they are the same.

Is there some standard way of solving determining these equivalences algorithmically, or perhaps can anyone think of a better alternative?

Much appreciated.

• Is there a limitation to the kind of statements you are using? The problem might very well be undecidable. – quicksort Dec 24 '17 at 20:26
• Diophantine equations are algorithmically unsolvable, and your problem seems to be even more general. – chi Dec 24 '17 at 22:38
• If you want to check theorems, you probably want to have a library of common ways to rearrange formula. The proof writer then has the ability to prove most equivalences if they have the knowledge/imagination to do so. I don't think this 'normal form' of yours really exists in the general case. – James Hollis Dec 24 '17 at 23:50
• Statements consist of standard booleans and, or, not, $\leq$, $\geq$, =, with arithmetic expressions consisting of addition, subtraction and multiplication of integers and variables, if that helps? – Harr Dec 25 '17 at 1:10

Regardless of decidability, your problem is definitely $NP$-hard. Suppose we could efficiently check if the normal form of problems were syntactically the same. Then we could efficiently solve 3SAT by checking if a boolean formula is equivalent to False.