http://code.google.com/p/haskellatp/source/browse/trunk/Paramodulation.lhs?spec=svn2&r=2
is nice ;) On Sat, Sep 22, 2012 at 12:40 AM, Russell Wallace <[email protected]> wrote: > 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/212726-11ac2389 > Modify Your Subscription: https://www.listbox.com/member/?&; > Powered by Listbox: http://www.listbox.com -- Ben Goertzel, PhD http://goertzel.org "My humanity is a constant self-overcoming" -- Friedrich Nietzsche ------------------------------------------- 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
