Yes, though I think anyone who knows Haskell already understands it can express this kind of thing more concisely than C++ :)
On Sat, Sep 22, 2012 at 6:34 AM, Ben Goertzel <[email protected]> wrote: > 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/1658954-f53d1a3f > Modify Your Subscription: https://www.listbox.com/member/?&; > Powered by Listbox: http://www.listbox.com ------------------------------------------- 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
