How to Extract inconsistencies from predicate logic? I have a set of predicates and I want to compare them to make a filter and detect if there existe any duplication or a conflict
Exemple :


*

*∃x[P(x) ∧ S(x,Tom)] 

*∃x[P(x) ∧ S(x,Tom)] 

*∀x[C(x) -> ∃y [C(y) ∧ R(x,y)]] 

*∀x[C(x) -> ¬∃y [C(y) ∧ R(x,y)]]

*∀x[C(x) -> S(x)]

*¬∃x[C(x) ∧ ¬S(x)]


I want just to know if exist a solution to extract that:


*

*Rule 1 and 2 : are Duplicated

*Rule 3 and 4 : there is a Conflict

*Rule 5 and 6 : Mean the samething


Thinks
 A: Testing for Duplication (i.e syntactially being the exact same string) is of course straightforward: just take any two strings and go through them symbol by symbol.
Testing for Meaning the Same Thing is what is what is better known as testing for logical equivalence. As it turns out, yes, there is a test for equivalence in so far as that for any two statementa that are equivalent, the test will eventually be able to tell ... but unfortunately, the test may go into an infinite loop when presented with two statements that are not equivalent, and we cannot know beforehand how long the test may take, with the rather unfortunate consequence that if the test has been cranking away for, say, two days, we do not know whether that is because the two statements are ont equivalent, or whether it is because the statements are equivalent, but the test has not not figured that out!
Finally, Testing for Conflict, is better known as testing to see if two statements are logically contrary or inconsistent (i.e cannot both be true at the same time) or not (in which case they are logically consistent with each other). This test suffers from the same problem as the previous one: Yes, there is a test that for any two contrary statements will eventually be able to figure out that they are contrary, but again, for two statements that are not contrary, the test will go into an infinite loop, and we do not know how long the test might take.
For the last two Tests, then, the practical solution is to put a time-limit on the test. Thus, the test will be able to figure out that some pairs of statements are equivalent, and it will also be able to figure out that other pairs of statements are not equivalent, and it will figure out that some pairs are contrary, and it will figure out that some are not contrary, but for some pairs it will time out and you just don't get an answer as to whether they are equivalent or contrary.
P.s. If you want to know why all of this is the case, search for 'semi-decidability of first-order logic'
