Uninterpreted function: Difference between revisions

Revision as of 10:30, 9 May 2012

Revision as of 21:56, 5 December 2012

Line 20:

==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>J. McCarthy, (1962) "Towards a mathematical science of computation." '''IFIP Congress.''', pp. 21–28</ref>.

Free theories can be solved by searching for [[common subexpression]]s to form the [[congruence closure]]. Solvers include [[satisfiability modulo theories]] solvers.

Line 31:

==References==

{{Reflist}}

{{Formalmethods-stub}}

[[Category:Specification languages]]

{{Formalmethods-stub}}