Content deleted Content added
→top: there are many decision problems for the free theory, unifications solves the sat. problem; specified/linked statement about 'other theories' |
→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>
Free theories can be solved by searching for [[common subexpression]]s to form the [[congruence closure]]. Solvers include [[satisfiability modulo theories]] solvers.
| |||