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.
and
,or
,not
, $\leq$, $\geq$, =, with arithmetic expressions consisting of addition, subtraction and multiplication of integers and variables, if that helps? $\endgroup$