Content deleted Content added
→Discussion: converted to ((cite)); added open-access url |
|||
Line 21:
==Discussion==
The [[decision problem]] for free theories is particularly important, as many theories can be reduced to it; the above example is the prototypical example of the theory of [[array data structure|arrays]], where 'select' and 'store' are the canonical array access functions.<ref>{{cite book| author=John McCarthy| chapter=Towards a Mathematical Science of Computation| title=IFIP Congress| year=1962| pages=21–28| publisher=North-Holland| url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.79.8613}}</ref>{{cn|reason=The given reference neither mentions 'array', nor 'store', nor 'select'. Apparently it doesn't handle the example.}}
Free theories can be solved by searching for [[common subexpression]]s to form the [[congruence closure]]. Solvers include [[satisfiability modulo theories]] solvers.
| |||