What is the best way to automatically proof that two first-order formulas F and G are equivalent?
The formulas have some restrictions compared to "full" first-order formulas:
- quantifier-free
- function-free
- implicitly universally quantified
I can transform those formulas in clause normal form and I have routines for unification for literals. However I'm not sure how to continue and if this problem is decidable.
As mentioned, to prove that F <=> G where both are closed (universally quantified) formulas, you need to prove F => G and also G => F. To prove each of these two formulas, you can use various calculi. I'll describe [resolution calculus]:
Under your conditions, all atomic formulas coming from F will be predicate symbols applied only to variables and all atomic formulas from G will be predicate symbols applied only toto skolem constants. So the resolution procedure will only produce substitutions that either map variables to other variables, or variables to those skolem constants. This implies that it can only derive a finite amount of distinct literals, and so the resolution procedure will always stop - it will be decidable.
You can also use automated tool for this purpose that will do all that work for you. I use The E Theorem Prover for such problems. As the input language I use the language of The TPTP Problem Library, which is easy to read/write for humans.
To give an example: Input file:
then I run
(
-tAuto
and-xAuto
do some auto-configurations, most likely not needed in your case), and the result iswhere the most important lines are