<p>The motivation you state for dealing with undecidability applies to decidable but hard problems as well. If you have a problem that is NP-hard or PSPACE-hard, we will typically have to use some form of approximation (in the broad sense of the term) to find a solution.</p>

<p>It is useful to distinguish between different notions of approximation. </p>

<ul>
<li>Numeric approximation: applies when you have a metric on the solution space and you can measure distance from the solution. This is the case for problems like #SAT, where you count solutions and can design an approximation algorithm that returns a value within $\varepsilon$ of the solution. </li>
<li>Probabilistic approximation: when you use a randomized algorithm you can give up certainty in the solution you will obtain every time you run the algorithm. You can move between randomness in the algorithm and randomness in the solution space by considering a probability distribution over solutions. Then the approximation here is that with some probability greater than $\delta$, you will obtain a correct solution.</li>
</ul>

<p>There are $(\varepsilon,\delta)$-algorithms for problems like ALLSAT which combine the two perspectives above. In the specific case of undecidable problems, or problems where there is no obvious metric and we do not want to use a randomized algorithm, there is a question of what notion of approximation to use. This problem arises specifically in the analysis of programs in optimizing compilers and in program verification. Determining complex properties of programs is either undecidable or computationally expensive, so some form of approximation is required. </p>

<p>Here is an example of a different notion of approximation.  Suppose you perform a computation like multiplying two large numbers and want to check if it the multiplication was correct. There are lots of heuristic techniques that are used in practice to check correctness without repeating the calculation again. You can check that the signs were multiplied to obtain the right sign. You can check whether the numbers have the right parity (even/odd number properties). You can use a more sophisticated check like <a href="http://en.wikipedia.org/wiki/Casting_out_nines" rel="nofollow">Casting out nines</a>. All these techniques have a common property that they can tell you if you made a mistake, but they cannot guarantee if you got the right answer. This property can be viewed as a logical approximation because you may be able to prove that the original calculation is wrong but you may not be able to prove that it is correct. </p>

<p>All the checks I have mentioned above are examples of a technique called abstract interpretation. Abstract interpretation makes completely rigorous a notion of logical approximation distinct from numeric and probabilistic approximations. The problem I described with analysis of a single calculation extends to the more complex case of analysis of a program. The literature on abstract interpretation has developed techniques and frameworks for approximate, logical reasoning about programs, and more recently about logics. The following references might be useful. </p>

<ol>
<li><a href="http://www.di.ens.fr/~cousot/AI/IntroAbsInt.html" rel="nofollow">Abstract Interpretation in a Nutshell</a> by Patrick Cousot, which is a simple overview.</li>
<li><a href="http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/lecture_13-abstraction1/Cousot_MIT_2005_Course_13_4-1.pdf" rel="nofollow">Overview of Abstraction</a> by Patrick Cousot, as part of his course. There is a very nice example of abstraction for determining properties of a boquet of flowers. The bouquet analogy includes fixed points and can be made completely mathematically precise. </li>
<li><a href="http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/" rel="nofollow">Course on Abstract Interpretation</a> by Patrick Cousot, if you want all the depth and details. </li>
<li><a href="http://www.di.ens.fr/~cousot/COUSOTpapers/JLP92.shtml" rel="nofollow">Abstract interpretation and application to logic programs</a>, Patrick Cousot and Radhia Cousot, 1992. Applies to logic programs, as per your request. The initial section also formalises the casting out nines procedure as an abstract interpretation.</li>
</ol>

<p>All of this has typically been applied to reason about computer programs. There has been fairly recent work on applying ideas from abstract interpretation to study decision procedures for logics. The focus has not been modal logic but satisfiability in propositional logic and quantifier-free first-order theories. (Since I have worked in this space, one paper below is mine)</p>

<ol>
<li><a href="http://www.cs.wisc.edu/wpis/papers/tr1699r.pdf" rel="nofollow">A generalization of Staalmarck's method</a> by Aditya Thakur and Thomas Reps, 2012. Gives a generalisation of Staalmarck's method to problems in program analysis.</li>
<li><a href="http://www.di.ens.fr/~cousot/COUSOTpapers/FoSSaCS-11.shtml" rel="nofollow">The reduced product of abstract domains and the combination of decision procedures</a>, Patrick Cousot, Radhia Cousot, and Laurent Mauborgne, 2011. This paper studies the Nelson-Oppen technique for combining decision procedures and shows that it can also be used for incomplete combinations, which is particularly interesting if you have undecidable problems.</li>
<li><a href="http://www.eecs.berkeley.edu/~vijayd/papers/2012/sas.pdf" rel="nofollow">Satisfiability Solvers are Static Analysers</a>, my paper with Leopold Haller and Daniel Kroening, 2012. Applies the lattice-based approximation view to characterise existing solvers. You could also look at <a href="http://www.eecs.berkeley.edu/~vijayd/talks/2013/unification.pdf" rel="nofollow">my slides on the topic</a>, instead.</li>
</ol>

<p>Now none of the papers above answers your specific question about attacking satisfiability problems which are undecidable. What these papers do is take an approximation-oriented view of logical problems that is not numeric or probabilistic. This view has been applied extensively to reason about programs and I believe it addresses exactly what you are asking.</p>

<p>To apply it to modal logic, I would suggest a starting point is to use algebraic semantics of Jonsson and Tarski or the later semantics of Lemmon and Scott. This is because abstract interpretation is formulated in terms of lattices and monotone functions, so Boolean algebras with operators are a convenient semantics to work with. If you want to start with Kripke frames, you can apply Jonsson and Tarski's duality theorem (which some may call Stone duality) and derive the algebraic representation. Thereafter, you can apply the theorems of abstract interpretation for logical approximation.</p>

CC BY-SA 3.0
2013-08-22T20:04:11.603Z
2013-08-29T04:29:16.243Z
2013-08-29T04:29:16.243Z
Vijay D
<p>It is known that many logic problems (e.g. satisfiability problems of several modal logics) are not decidable. There are also many undecidable problems in algorithm theory, e.g. in combinatorial optimization. But in practice heuristcs and approximate algorithms works well for practical algorithms. </p>

<p>So one can expect that approximate algorithms for logic problems can be suitable as well. However the only reseach trend along these lines I have managed to find is the max-SAT problem and its development was active in nineties.</p>

<p>Are there some other active research trends, workshops, keywords, good references for the use and development of approximate methods for modal logics, logic programming and so on?</p>

<p>If automated reasoning is expected to gain prominence in the future applications of computer science then one will have to be able to go beyond undecidability constraints of logics and approximate methods or heuristics can be natural path to follow, isn't it so?</p>

CC BY-SA 3.0
2013-08-28T04:07:04.597Z
"the only reseach trend along these lines I have managed to find is the max-SAT problem and its development was active in nineties." Actually, MAXSAT solvers are improving significantly these days: http://www.maxsat.udl.cat/12/solvers/index.html
Radu GRIGore
CC BY-SA 3.0
2013-11-24T16:26:06.777Z
After some studies now I am inclined to change my mind. The finite model theory should be the most prospective field for AI and applied logic. Logics that are based on infinite model theory maybe aesthetically nice but they lack two important connections with reality: 1) practical applications are always restricted by bounded resources (e.g. list of variables should be bounded); 2) the physical worl is necessarily bounded and more likely to be discrete as well (e.g. fundamental length and so on). So - now I don't understand the use of infinite model theories. THEY are the approximations.
TomR
CC BY-SA 3.0
2013-12-22T20:02:59.900Z
One other trend is "connection science" or neuro-symbolic integration - where the logic is used for stating problem and providing input and reading output of the computation, but the computation itself is performed by neural network. There is some discussion how powerful NN can be (e.g. some suggest that they can break the Turing limit only when realy numbers are used as weights but this can be discussed - e.g. it is open question whether real numbers exist in nature at all) but it is clrar that there should be prospects for using heuristic methods in logic and integration is one way.
TomR
<lo.logic><approximation-algorithms><undecidability>
Good reference about approximate methods for solving logic problems
TomR
# Good reference about approximate methods for solving logic problems

(Asked by: username_0 on 2013-08-22)

It is known that many logic problems (e.g. satisfiability problems of several modal logics) are not decidable. There are also many undecidable problems in algorithm theory, e.g. in combinatorial optimization. But in practice heuristcs and approximate algorithms works well for practical algorithms.

So one can expect that approximate algorithms for logic problems can be suitable as well. However the only reseach trend along these lines I have managed to find is the max-SAT problem and its development was active in nineties.

Are there some other active research trends, workshops, keywords, good references for the use and development of approximate methods for modal logics, logic programming and so on?

If automated reasoning is expected to gain prominence in the future applications of computer science then one will have to be able to go beyond undecidability constraints of logics and approximate methods or heuristics can be natural path to follow, isn't it so?

**Tags:** lo.logic, approximation-algorithms, undecidability
> **Comments:**
> **username_1**: "the only reseach trend along these lines I have managed to find is the max-SAT problem and its development was active in nineties." Actually, MAXSAT solvers are improving significantly these days: http://www.maxsat.udl.cat/12/solvers/index.html  
> **username_0**: After some studies now I am inclined to change my mind. The finite model theory should be the most prospective field for AI and applied logic. Logics that are based on infinite model theory maybe aesthetically nice but they lack two important connections with reality: 1) practical applications are always restricted by bounded resources (e.g. list of variables should be bounded); 2) the physical worl is necessarily bounded and more likely to be discrete as well (e.g. fundamental length and so on). So - now I don't understand the use of infinite model theories. THEY are the approximations.  
> **username_0**: One other trend is "connection science" or neuro-symbolic integration - where the logic is used for stating problem and providing input and reading output of the computation, but the computation itself is performed by neural network. There is some discussion how powerful NN can be (e.g. some suggest that they can break the Turing limit only when realy numbers are used as weights but this can be discussed - e.g. it is open question whether real numbers exist in nature at all) but it is clrar that there should be prospects for using heuristic methods in logic and integration is one way.  

---

## 1 answers

### Answer by username_2 on 2013-08-22. Score: 10

The motivation you state for dealing with undecidability applies to decidable but hard problems as well. If you have a problem that is NP-hard or PSPACE-hard, we will typically have to use some form of approximation (in the broad sense of the term) to find a solution.

It is useful to distinguish between different notions of approximation.

* Numeric approximation: applies when you have a metric on the solution space and you can measure distance from the solution. This is the case for problems like #SAT, where you count solutions and can design an approximation algorithm that returns a value within $\varepsilon$ of the solution.
* Probabilistic approximation: when you use a randomized algorithm you can give up certainty in the solution you will obtain every time you run the algorithm. You can move between randomness in the algorithm and randomness in the solution space by considering a probability distribution over solutions. Then the approximation here is that with some probability greater than $\delta$, you will obtain a correct solution.

There are $(\varepsilon,\delta)$-algorithms for problems like ALLSAT which combine the two perspectives above. In the specific case of undecidable problems, or problems where there is no obvious metric and we do not want to use a randomized algorithm, there is a question of what notion of approximation to use. This problem arises specifically in the analysis of programs in optimizing compilers and in program verification. Determining complex properties of programs is either undecidable or computationally expensive, so some form of approximation is required.

Here is an example of a different notion of approximation. Suppose you perform a computation like multiplying two large numbers and want to check if it the multiplication was correct. There are lots of heuristic techniques that are used in practice to check correctness without repeating the calculation again. You can check that the signs were multiplied to obtain the right sign. You can check whether the numbers have the right parity (even/odd number properties). You can use a more sophisticated check like [Casting out nines](http://en.wikipedia.org/wiki/Casting_out_nines). All these techniques have a common property that they can tell you if you made a mistake, but they cannot guarantee if you got the right answer. This property can be viewed as a logical approximation because you may be able to prove that the original calculation is wrong but you may not be able to prove that it is correct.

All the checks I have mentioned above are examples of a technique called abstract interpretation. Abstract interpretation makes completely rigorous a notion of logical approximation distinct from numeric and probabilistic approximations. The problem I described with analysis of a single calculation extends to the more complex case of analysis of a program. The literature on abstract interpretation has developed techniques and frameworks for approximate, logical reasoning about programs, and more recently about logics. The following references might be useful.

1. [Abstract Interpretation in a Nutshell](http://www.di.ens.fr/~cousot/AI/IntroAbsInt.html) by Patrick Cousot, which is a simple overview.
2. [Overview of Abstraction](http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/lecture_13-abstraction1/Cousot_MIT_2005_Course_13_4-1.pdf) by Patrick Cousot, as part of his course. There is a very nice example of abstraction for determining properties of a boquet of flowers. The bouquet analogy includes fixed points and can be made completely mathematically precise.
3. [Course on Abstract Interpretation](http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/) by Patrick Cousot, if you want all the depth and details.
4. [Abstract interpretation and application to logic programs](http://www.di.ens.fr/~cousot/COUSOTpapers/JLP92.shtml), Patrick Cousot and Radhia Cousot, 1992. Applies to logic programs, as per your request. The initial section also formalises the casting out nines procedure as an abstract interpretation.

All of this has typically been applied to reason about computer programs. There has been fairly recent work on applying ideas from abstract interpretation to study decision procedures for logics. The focus has not been modal logic but satisfiability in propositional logic and quantifier-free first-order theories. (Since I have worked in this space, one paper below is mine)

1. [A generalization of Staalmarck's method](http://www.cs.wisc.edu/wpis/papers/tr1699r.pdf) by Aditya Thakur and Thomas Reps, 2012. Gives a generalisation of Staalmarck's method to problems in program analysis.
2. [The reduced product of abstract domains and the combination of decision procedures](http://www.di.ens.fr/~cousot/COUSOTpapers/FoSSaCS-11.shtml), Patrick Cousot, Radhia Cousot, and Laurent Mauborgne, 2011. This paper studies the Nelson-Oppen technique for combining decision procedures and shows that it can also be used for incomplete combinations, which is particularly interesting if you have undecidable problems.
3. [Satisfiability Solvers are Static Analysers](http://www.eecs.berkeley.edu/~vijayd/papers/2012/sas.pdf), my paper with Leopold Haller and Daniel Kroening, 2012. Applies the lattice-based approximation view to characterise existing solvers. You could also look at [my slides on the topic](http://www.eecs.berkeley.edu/~vijayd/talks/2013/unification.pdf), instead.

Now none of the papers above answers your specific question about attacking satisfiability problems which are undecidable. What these papers do is take an approximation-oriented view of logical problems that is not numeric or probabilistic. This view has been applied extensively to reason about programs and I believe it addresses exactly what you are asking.

To apply it to modal logic, I would suggest a starting point is to use algebraic semantics of Jonsson and Tarski or the later semantics of Lemmon and Scott. This is because abstract interpretation is formulated in terms of lattices and monotone functions, so Boolean algebras with operators are a convenient semantics to work with. If you want to start with Kripke frames, you can apply Jonsson and Tarski's duality theorem (which some may call Stone duality) and derive the algebraic representation. Thereafter, you can apply the theorems of abstract interpretation for logical approximation.


---

