Content deleted Content added
m Dating maintenance tags: {{Clarify}} {{Cn}} |
|||
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.|date=May 2014}}
Free theories can be solved by searching for [[common subexpression]]s to form the [[congruence closure]].{{clarify|reason=Indicate about solving which problem in free theories the sentence is supposed to speak. E.g. to solve the satisfiability problem of conjunctions of equations, the Martelli-Montanari syntactic unification algorithm suffices, neither common subexpressions nor congruence closures are needed. Maybe, satisfiability of arbitrary boolean combinations of equations is meant?|date=May 2014}} Solvers include [[satisfiability modulo theories]] solvers.
== See also ==
| |||