3
$\begingroup$

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.

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ Is there a limitation to the kind of statements you are using? The problem might very well be undecidable. $\endgroup$
    – quicksort
    Dec 24, 2017 at 20:26
  • $\begingroup$ Diophantine equations are algorithmically unsolvable, and your problem seems to be even more general. $\endgroup$
    – chi
    Dec 24, 2017 at 22:38
  • $\begingroup$ 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. $\endgroup$
    – James Hollis
    Dec 24, 2017 at 23:50
  • $\begingroup$ 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? $\endgroup$
    – Harr
    Dec 25, 2017 at 1:10

1 Answer 1

Reset to default
1
$\begingroup$

So, there are two possibilities, depending on how complex your statements are.

If your statements are relatively simple, then there's a good chance they fit in what is decidable with Satisfiability Modulo Theories. It's basically a way of taking a SAT solver and integrating it with a solver for a specific theory, for example, theory of linear arithmetic. Here is a list of common theories.

If your statements are too complex, then reducing these equations to a normal form becomes undecidable. This is because there are ways to encode logic and computation in arithmetic, so determining the equivalence of some formulas can be equivalent to solving arbitrary logical equations.

The decidability of your problems depends heavily on whether you're using integers or reals, linear or non-linear arithmetic, etc. As was mentioned in the comments, if you can encode arbitrary Diophantine equations, then you're definitely undecidable.

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Interesting, thanks - so what about coming at this semantically, how might I algorithmically check for equivalence between statements then? is there some standard method for checking? $\endgroup$
    – Harr
    Jan 22, 2018 at 16:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.