It is known that first order logic is too general to be decidable. Adding axioms with special meaning (e.g. expressing notions such as necessity/obligation, provability, etc.) leads us to modal logics but some of them (especially multidimensional fusions or products of them) are undecidable too.

As I understand, then undecidability generally is created by quantifiers - it is quite hard to prove of refute formula, that should be valid in all worlds (if accessibility relation allow them).

The undecidability can be handled by several approaches: 1) lowering the expressivity of the logic or considering the less expressive fragments; 2) following ideas of max-SAT problems; 3) moving to approximate reasoning (probabilistic, fuzzy-logic, etc.).

All these approaches has this drawback: they tries to reformulate or make less relevant the original problem that was created as conscise and clear model of the real world problem.

Maybe there is better way how to approach such undecidable situations - simply by adding additional axioms that reflect the real-world situation. E.g. axiom can be added that the number of variables is bounded in the logic (there can be different axioms depending on how we model the reason why there are only finite number of instances of some class in the world - e.g. bounded resources, restricion by law, etc.).

So - the question is - is there some research trend that investigates the modal logics with aim - what axioms should be added to them the regain the decidability of logics (and according - the suitability for them for automated reasoning tasks, for use in autonomous systems)?



Your Answer

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