# What is example of Kahr formula $[\forall\exists\forall, (\omega, 1), (0)]$ and what to do if such undecidable formula is encountered in practice?

There are mentioned many classes of undecidable formulas in the book "The Classical decision problem" http://www.springer.com/la/book/9783540423249. Kahr formulae is one class of undecidable formuls and it can be expressed in prenex normal form by $[\forall\exists\forall, (\omega, 1), (0)]$.

There are two questions. 1) how to understand this notation and is it possible to see one example of Kahr formulae. 2) What to do if such formula is encountered in pratice? Is it possible to construct more general theory which affirms of refutes this formula? Maybe more creativity is required - there is no automatic proof available, but creative approach can yield some proof for this class? Maybe theory can not say anything about this formula and in practice the additional assumptions outside from the theory should be made (discovered) and then the truth value of the formula can be decided?

There is practical basis for this question. SWRL (semantic web rule language) is the combination of OWL and RuleML and generally it is not decidable. Therefore reasoners implement only decidable subsets of SWRL. But businesses encounter and will encounter SWRL expressions that are undecidable. What to do with such expressions? Can excessively creative mathematicians find proofs for individual expressions and businesses simply need to make more investments? Laws can be formalized in SWRL and what the Supreme Court judges will do if the decision of tha case depends on the affirmation or rejection of undecidable formula? What practical approaches can be made? Who should give the answer?

One approach is use of approximation methods, e.g. https://cstheory.stackexchange.com/questions/18716/good-reference-about-approximate-methods-for-solving-logic-problems but that works mostly for modal formules where the modal depth can be truncated. Maybe creative search for proofs can be the other answer, or not?