On 19 mar, 03:24, Graham Cooper <grahamcoop...@gmail.com> wrote: > On Mar 19, 10:40 am, George Greene <gree...@email.unc.edu> wrote: > > > > > > > > > > > On Mar 18, 7:39 pm, Frederick Williams <freddywilli...@btinternet.com> > > wrote: > > > > I don't see how you will get far without modus ponens. > > > Well, I see your point that unless everything is going to be a direct > > instance of some single axiom, > > you have to have an inference rule that produces a consequence from an > > input. > > But the question still arises, why isn't that -> ? > > You sort of need modus ponens and a deduction theorem to get from > > A / B to A -> B, but doesn't it take more "variables" just to bridge > > that modality? > > > It just seems to me you are operating from a textbook with a framework > > that has > > not been presented to anyone who is not also reading that textbook, > > and that > > is ITself in need of some defense. > > If you want to forward chain or backward chain via inference rules > > you're going to need another syntax symbol than -> > > If not in the inference rule itself, then in a separate control module > which usually has modus ponens, cut elimination or resolution. > > MP can emulate those last 2 as inference rules. > > ----------- > > e.g. in PROLOG instead of > > not(not(X)) :- thm(X). > > use > > if( X , not(not(X))). > and > thm(R) :- if(L,R) , thm(L) [MP] > > --------------------- > > Both methods have a :- somewhere > > You just put thm(X) around a naked theorem X in PROLOG. > > Herc > --www.BLoCKPROLOG.com
Is your code microprolog compatible i just downloaded a ZX emulator?