Uninterpreted function: Difference between revisions

Revision as of 10:05, 15 August 2016

Revision as of 10:06, 15 August 2016

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>{{cite bookproceedings |last=McCarthy |first=John |year=1962 |title=IFIP Congress |chapter=Towards a Mathematical Science of Computation |publisher=North-Holland |chapter-url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.79.8613 |pages=21–28}}</ref>{{citation needed|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.