Consider the problem of writing a general inference engine in the spirit of Eurisko, Dyna etc., and then using it for automated theorem proving, presumably the flagship, or at least a major, application of such a system.
At the heart of automated theorem proving is the paramodulation inference rule. This can be written in e.g. C++ in on the order of a hundred lines of code. Can it be written as a declarative rule? Sort of. It certainly can for a human audience, e.g. // C | a = b, D | x(z) ?= y // -> (C | D | x(b) ?= y)/s // where s = unify(a, z) // and z not a variable But if you try to put this as a declarative rule in a rule-based inference engine, you immediately find that it needs pattern matching on arbitrarily deep subterms, which is something no pattern matching system I've ever heard of provides. Of course C++ doesn't either and that doesn't stop us implementing paramodulation anyway, and similarly we could implement it in e.g. Prolog in the same way, just doing recursion into the subterms by hand. But if we do that, we don't get to use the term indexing that is presumably one of the major features the inference engine would provide (in the same way automatic maintenance and use of table indexes one of the major features a relational database engine provides), so that would kind of defeat the purpose. So if we need super pattern matching, why not just implement that? Sure, we could do that. But as far as I can see, paramodulation is the only thing that would use that feature! Everything else I can think of that wants pattern matching, either only needs the usual surface level version of it, or can be expressed just about as easily in terms of paramodulation itself as in terms of super pattern matching. Which suggests it is best to just go ahead and have the inference engine provide paramodulation as the built-in feature. My question is, are there any counterexamples? Are there any rules or heuristics we would want to write, that would need super pattern matching (or even just regular pattern matching) but cannot readily be written in terms of paramodulation? ------------------------------------------- AGI Archives: https://www.listbox.com/member/archive/303/=now RSS Feed: https://www.listbox.com/member/archive/rss/303/21088071-c97d2393 Modify Your Subscription: https://www.listbox.com/member/?member_id=21088071&id_secret=21088071-2484a968 Powered by Listbox: http://www.listbox.com
