Hello.
On 07/04/18 01:45, Thomas Tuerk wrote:
> higher order matching is decidable, but has a very high complexity. (see
> e.g. "An introduction to decidability of higher-order matching", Colin
> Stirling, http://homepages.inf.ed.ac.uk/cps/newnewj.pdf). Higher order
> unification is undecidable, b
Hi,
higher order matching is decidable, but has a very high complexity. (see
e.g. "An introduction to decidability of higher-order matching", Colin
Stirling, http://homepages.inf.ed.ac.uk/cps/newnewj.pdf). Higher order
unification is undecidable, but matching is decidable. As I understand
it, HOL
