A Proof Editor for Propositional Temporal Logic

Pages 27
Views 5

Please download to get full document.

View again

of 27
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Description
Report No. STAN-CS A Proof Editor for Propositional Temporal Logic Ross Casley Department of Computer Science Stanford University Stanford, CA A PR,OOF EDITOR FOR PROPOSITIONAL TEMPORAL LOGIC
Transcript
Report No. STAN-CS A Proof Editor for Propositional Temporal Logic Ross Casley Department of Computer Science Stanford University Stanford, CA 94305 A PR,OOF EDITOR FOR PROPOSITIONAL TEMPORAL LOGIC Ross Casley 1. Introduction 1.l Ontlinc of this Report This r(~sc\i~~(~ll wils stll)l)ort,c~tl ill l);t.rt, 1)~ t,llr* Nikt,iollikl Scicncc~ Folllltl;lt,io~l ll~ldcr gr;l.llt DCR.- &I Z~~hlis~~, Sy~~~l~olics il.ll(l S,yml)olic*s X00 iir( t,l*iltl(~llli~rks of Syuholics, h(:. 1 2. PTL Users Manual 2.1 Terminology In this ~~mn~~al tlw tcrxu f~rmdu is applitd ttr any PTL formula, whcthcr it occurs as a single line of tlic proof, or as a part of a larger formida. The term uddc formula is used to restrict mc~anillg to ii. formula 1Jia.t forms a line of the proof. l)y The t,crni conjunction always rcfus the A Si duly, opmator. a called conjuncts. two or more siil~forndas arc joined is a forxuiil;~ consis tilig of two or Iiior(: &junc ts joind by the v 2.2 Example of Using PTL Thcb bst8 introduction to PTL is 1)~ cxarr~plc. I-Icre I giv(g iristriict.ions for coiist~riictirrg a proof of ()p op. The r(mlcr is cncormgccl to follow thca instructions whiltb running PTL. Even if this is not, pssiblc, (10 not, skip this see tiou; t,lic* lmsic: op~~rat,ioxis usctl to rim PTL arc not rqm~td clscwhcrc. Marc tlctail on the PTL ~OI~~II~~II~S is give later ill this chapter. If PTL is Ilot iil~ *~l(ly l()il(i( (l, gjvcx t,htb lisp (:olll1llilll(l (load C : ross ptl system-def ). Lisp will WS~O~I~ wit11 a. ql~cstpioxl cncling: load all 5 of them? (Y, N, S). You sl1011ht type Y. (If this qumticm (lit1 llrbt, il.])j)c'il.r, I Tr, wils i\.lr(\;l.~l,y loil(\~*(l ZI.U(~ ~OII (:il.tl c*ont,imlc~.) _ Crwtin!l (1 NCUJ Fik Crd~c ib I~VW lilt to hold t,hct proof. Thcb filch GLIB 1~ givoxl iwly ltikill(, but tlic cxtvlisi0n shoiild 1)~. ptl. This ~~xt,cnsiou CIISUI CS t,hibt, ZIllil(:s will il.11 t,orll;ht,i(*dly ctcli tp t,h b film iu PTL IHO ~C. The SpGJ PTL c~~1i11ilil11(ls arc ody itvidill)lc for filth ctli tml in I TL tnoclc*. - III that first linct of this file WC will simldy ciclscril)c* the tl~~tl~lctiotl to follow. Of collrso, PTL clocks not rcqiiirc* that, this 1~ tlon~, it, is just, our choic*c* to (lo so. SO W( Willltt t,o imcd il lilic Collti~hi1lg so~t~c*tllirlt: like li(*fv~ is il. I)l.OOf Of c p 7 ()I). This lbritlgs 11s t,o t,li(- first, prol)lvit~, how I0 t,ypv 1,lw 1O~iC il.l S~llll)C~lS. The thrctcb qm:ial keys In;Lrkd with a s(1liilr(, circ.lc itxlcl t,ri;uigh ( ill1 110 llscd to cdc~r tllc IlIO lid opmdors 0, () illl(l 0 rc~spd,ivdy. Thc~ otllcr logic;\1 sy~z~l~ols :kr(* stil.lld;l.rtl on thcb 3600 kcylmml, iljlc1 ilix! t,,ypml iisiq t,hct s~in~)o~ I;cay. Ullfol t,llllilt,( l,~, t,llcb S~II~~)O~S (10 tlot, ;Lppt ;u ou thcx kcylmml, l)llt tllc4r positoion Cil.11 l)(* discov(~rd l)y tryping syllllbol-liol[b. Syliil~ol-(1 is t,lict A-sign, syylrilml-w is V, sy~iil~h-i( is -+ illl(l S,~tlll)ol-Y is 3. (3 illl(1 --f il.l ( cqiivd~~iit Wil.;YS to t,ylw ililplics.) I ll0 CiLl ilt (shift&) is llo1. tllt~ SiLIllV th CilC t,ctr il.s t,ll(\ il.lltl-sigll, A. 2 N OW typo thcb first fc w lines of the film SO ttllikt it ;kpp( :crs iks follows. (Note: the first, line tlisplil,yc~d is an attributc~ list for the file. It wiks crcatcd usiug the Zxr~acs commands, PTL Mode ikn(l Set PiL(:kagc. This line xmy.bc omitted if you wish.) -*- Mode: PTL; Package: USER -*- First a proof that Op 3 op. Proof is by contradiction Text such ils this may Lppar :knywh lrc in the file, and dots not affect the deduction. Now type the yrcmisc of thct tlc~duction. Since this is a proof by contradiction, the yrcxnise is Formulas that me prt of the proof arct distinguished from plain text 1)~ appearing on a IWW limb bcgixluiug with il line r~~wnh, which is au iut,cbgcbr followed 1)~ a co1011. Thcx lint nurrlbm GUI bc c*irtmd by typing it, or it mtl lx g(w(briltd i~llt~olliitt~i ~itll~ itsiiig the Siipcr-L cofnmaiid. Lint niunl~c~rs 1~c~~1 not 1)~ uiiiqiic~. difficult to read. After cnt,cgg tllcb forlrlulil. the file sl~oultl c:(jlltgl: Howcvcr proofs couti~iuing lul)lici~t~*d lhc IIIUII~WCS arc,a, Mode: PTL; Package: USER -*- First a proof that Op 3 op. Proof is by contradiction 1: -(OP ' OP) Thcrc ikr( now s( vc& wil.ys to proccccl. The strabcgy takcu hem is first to distrilmtc~ negations, tll( 11 ili)i)ly t,llv 0 rule t,o Ol~tilill ill1 c*xl)licit (:oiit,r;l(lic:tioli. The* PTL clcduction (:(bllllllii.ll ls :l.r( irlvok(*tl by giving il (:()lll~lli~n(l wllich specifics thct deduction rdv Ipo 1~ a.ppli~*d. Tllct ~~~~l~~~~~i~~~~l for distributing ncptious is Sltpr-N. Typv Super-N uow. 1 TL is IloW Wik.it,iIkg for yell tcb ClIooW il. forllda wing 1,11v II~oI~~~. T11c r~~~~tl~od Notice t1lil.t the IUO~SC cursor (:hiulg( s to il thick vmtical arrow, and ilist~id of poiiitiiig to intlividual (:lli~.ril(:t,~~rs on tllcb scrm~u, the IIIOUW piut,s to sl~l)fi)rlllul;rs occurring ill I;hc proof. A l~ollow box iblwil.ys surrounds the form&, to which t,hct XIIOIIG~~ is pointing. Clicking ik IIIOUSC lmtton SVlocts tllc) oiitlifid Slll~f0rlIIUliI.. * Move that IIIOUW so tllilt it points tm tll(b form&~ in lir~c 1. I~v :ilr( ful uot. to click OIIC of the IllOllSC l~llf~tolls. I l lr il.lwil.~s il.ssiiiil~ S l~liil.1~ tll(* IllOllS( j)oiill,s LO kilt Slllil.ll~ St possil)lv (;~l llllllil. siirroiiriclii~g t,llc inoiisc cursor. 111 lelic* ( XikllIj)l( foi IlIllliI., poiiitiiig t,lic~ iiiolts~~ cursor to tlic* 0 sign will oiitlin(* the fo~~iilllil op,; pointiug to 1JIC 3 sign will oiitliuct tllc formula ()p 3 op. II1 ~~~Il(TiLl, a Slll~forlIIlllit Cilll I (* outliiictl l)y poiutiug to its logicill operator. Whc*u pointing to ik formula, (~i~ :h of thcb three IIIOUSC l)uttons will h;~v~ ik diffcrmt c*ffc*ct. A [right] click il 1 Wil y. S ill)orts tllv COlIIlIIillld. Tll( CffCCt O f [lvft]nll(l [middl(~] clicks dcp~ud on the COllllllil.lld YOll gil.vc. For IllOSfp COIllltlilll~lS lollc rliiclcllc~ l~llt,toll ilhcbl4s tllc C0IllIlIitlI(l, illit tllc! 1Cft l)iibiaoii pc*rforius tliv m~ii4~d d~~du&m. TII(t iuvors+vi(lm) illforlllil.bioxl liiw ilt t,licb botehiii of t,llc? scram idwily! lists tllc lllrw.llilig Of ~ i1.cll liiolls( bllttol1. Typiug :~uythiug bc~siclcs OILC of tllc IXIOUSC 3 To conlplctc this deduction, outlinct the whole formula l(()p 1 Op): by pointing to the 1 op(\ra.tor. Click [left,] t 0 cornplctc tlic &Auction. PTL inserts the conclusion at the cud of the lmffcr, so the file uow cont;lins:,i)- Mode: PTL; Package: USER -*- First a proof that Op 3 op. Proof is by contradiction 1: -4OP ' OP) 2 : (]pho-p : By distributing - in 1 coiidusion rlc~rivccl. is written with a new line nuiiiber, cxplitiriiiig how the Cornmats are not, rcstrictd to formulas written by PTL. You can place\ comments on any foriiiiil;~ by typing a sc~iiricolon bcbforc tlicl comxilcnt. Tltc next step in this stmttbgy is to apply thct I rule to thtb subformula Oly of lincb 2. The 0 rule is invokd by the Super-E c~~~mmml. Supctr-E invokes the rule or the 0 rub, dcpmtlir~g 0x1 the main opadmr of that prcxnis(t choscr~ for it. Most, PTL C~IU~~I~S iuvokc one of scvmtl rules, dc~pcmtliiig on the prciniscs chosc~i. The Suf er-E COI~IU~I~ is invoked in exactly the same way as the Super-N cormuand. In fact WC must invoke this rule twice, itut1 the file fiually contans: -I- Mode: PTL; Package: USER -*- First a proof that Op 2 op. Proof is by contradiction 1: -(OP ' OP) 2 : Ophcl'p ; By distributing - in 1 3: OP * ('P A On-P, ; By the 17 rule from 2 4: OP * ('P A 0(-P * On-P)) : By the cl rule from 3 Whcrl il+ ~OII~XIKLII~ uses two (or morc) pr(~l~lis(~s, clicking [left] sclccts the lirst prmiis(~, but 110 tlcduction is pcrformd. The l~ollow box surrouldirq thcb first prmlis(~ rcumins cv(m whoa the mouse* is inovcd. A scconcl box surrounds thcb forlniila to which the mouse poiirts. l3oth boxes dis;lppilr ilft.cr tllc\ scyouc1 prciiiisc is s(*lc(ltd, all(l the dductioil rllidc. WIIPH you click [ltbft] tllcb 1)0x surrounding ~IIV first,.prctllliscb ~lr:l.,y dis;~~)l)~~i~r. This 11;qq)cas l)(yil.llsc i t8 is lacing siirroitnclcd twice otl(:( 1)~ 1,Iltn ldiltktbr tlli~.t follows t110 ~ll()~~sc i\.rol11itl, Ott \ it SCYO~IC~ tiulc by thcb tdinkcr that shows it 11;~s h-11 sc~lcc~d. I llcsc two tdinkcrs (:iluc( l (~a.ch other. 4 Siruply iii ant1 l)oth ldinkc*rs will 1~ visible. For the sitlll(* ldillkus ovdap 011 thc~ scrcon. lx'ilso11, JWll Illilly SW s11:d The Sllpm-R (*~I~~l~li\ll~l is llllllsllil1 in tllilt it gt~lcrittcs two lines in the proof. Th( first Ilcw liiic is the rcbsrilt of the t)ilsic rule, the s~:oild lint siiuplifics the first line. After teypiug Salpr-R, tllc llscr hmc sd(xcts as first pr(mis(~ thcb lcfturost occurrcncc of p. Thct sc~o1ic1 prcxuisc is the third occ1lrrcxm of p, which al)ycikrs as... A O( 11).... Do this xlow, and the followiug id li tioilit1 lillcls will il.p~m'ik. 5: OP fi ('P * 0(-P A 00-P)) A 6: FALSE (t-p A O(-TRUE A OU-p)) v OFALSE) ; By resolution from 4 : By simplifying This completes the proof, ant1 illnstratc~s ML important point. Somdin1os il forrmla is too long to fit COIIlfOrtilbly 011 il single lint. It Cilll t)c coiitiaric~cl OIlto ililotllct li,ic l)y splitting it So tl1ik.t 0110 of the conncctivt~s (A, V, 3, or -) il1)pt%i3 iit the end of the first lint\ (cxccpt for coxulucl~ts), or is ttlc first IloIl-lhmk dt;~r;~c:tc~r of the (:olltilllliltioii lixlcb. Formulas rl1a.y t)c corltimcd onto as IlI(t11y lilies ils Il~ C( SSil.1 ~ by using this colivcmtion 031 coach liiic. 2.3 Details of Selecting Forrnulas SCVCXd sit1li~tiolls did not arise in tllc ( XiLIll~lf given, lm t xrd to bc mciitio~id. In a Coii.jliii(:tioii, such ils A A U A C, poilitixtg tli(~ iiiousc to A will oiitliiic tlict A, pointing to cithm of the A signs ontlilios tlic wliolc cori.jnii(:tiori, A A L3 A C. Tlm(t is 110 wily to outline jllst il. piwc of tllc* forllld;t, sit,y A A I?. If this is Il( :( ssilry for thc~ proof, first 11s~ tllcb wc;~kt~allg rnlc tlc~scril~cd bvlow to cldlrc:c il IIPW f( rllllllil with A A I? r(~placixlg A A D A C. Then NW thcl 11cw forxllllli~ in it prmlisc. Sixuilibr Wxlllll(~nts i11)1)1,y to clis,jn~ic:tioiis. 111 il loill: proof, tw0 prciiiis(~s 1llil;Y t)(b SO far ii.[)int illibt t,ll(~;y Cil.llIlOt ili)l)vilr 011 tvll( SiLlllC scrwii. Dllt typiq i\. scrolling (~OIlllllil.llCl s1lc:ll ils Colltlwl- V il.1)orl.s tllct clc~tluct8iou COillllli\.ll(\. Tllc! solutioii is to WC* the ~s~~ scroiling (:()llllllilll(ls, hvokotl 1).y Iuoviilg tllct II~OI~SC to tlic~ left Imdcr of th %;lllil.cs scrwn. Scrolliiig this Wi\,y ttovs Ilot ii.l)ort il clc~tlrit~lioii ( olll~llh.lld. 2.4 How and When Formulas are Parsed l3(lfor(t il.lly forllld:l (:illl 1~ 11~~~1 i1.s tlr(t I)rcI~1isc of a (ldlu:tion, PTL lllilst I)il.rso it to (lctc~rmill(~ tllcl position of (~;d1 of its s~lt)li)rl~~di~s. Evc*ry f()l~~l~d~~. in il file is I);krsctl ~llc%il tllct file is r(*iul. (This will (:illls( il Ilc~t,i(*c~;ll l(~ (l(t1;l.y if ctxistitlg lilcbs with Itlilll,y fortllllliks ilr(x r( il(\.) NVW or ;dtc~rcd forumlas itit' IM.I?+Yl WllCVl il.lly of t,llc~ COllllllilllClS iiiitii~tirlpj it tlcductiori illt issid [)i1iywr is llo~l~lil.ll~ ( il.s( w1lsitivc, SO p illit P i\.l C tlisf8ilic*l. fol llllllils. r ll( ( OllStil.llt trllt i1.11(\ l;llsc fol lllllli\.s ill3 c*xc*cllbl.iolis I80 I,liis 1 1llt. lll1.v fo~llllliil. wibh kil( Ilil.lllC S tru0 illid f also, II0 lliil.lolbc*r 110~ c:;1.l)it;l.lixc~cl, will IN ( (lltivid( llt IV0 TRUE il.il(l FALSE rcyu:tivdy. Parsing is ill~il~il~lol~~~~1 if il S;YIltil.X u-for is folllld. Tlic cursor will 1~ p0:~itioird i~t tlic poiiit whcrct tllcb cmor Wi1.S follnd, ii.lltl ill1 terror lkl( SSiL~( will l)c givui iii tllca typo-iii window ilt t,liv l)ottofu of tltct scrml. Parsing IniLy 1)~ r(~stuud 1)~ isslling il clctll~ctictn (:r)llllllilll(l. The I)arsc r llliky S~SO t)c ixlvokd using the PiLEW IJiilh (super-1 ) COIIllllilll(l. This is usctful if you cq~:t to lid further errors in tlicb text. IJt\;l.ry c)l)(~riltors ilr( givrw thcb high& priority, follow4 11,~ A, t,llc ll V, th(~11 3. I lli~.t is, thcb for~llllli~ -ia A 13 V C 1) n is illtc~rprc~tcd ils (((-,A) A II) V C) This priority is il(:(:( l)t(\(l 0x1 input, but whcm PTL prints out foriliulq it insctrts a.tlditioni~.l p-~rcittlicsc~s so that tlir\ nlmning is clear. Tlic~ A and V qm2tors am tmatml as variadic, not biuary, so additional pamitli(3cs am never nccdcd within conjunctiolrs or disjunctions. 2.5 Dual Rules Each of the dctluction mlcs of propositional temporal logic has a corresponding (EUCLZ ruk. For cxamplc, the wcakcning rule allows you to replace a conjunction with positive polarity by one of its coujuncts. The dual of wcakcuiug allows you to rcplacc a rlisjurr,ction having nqntivc polarity by one of its disj~~~~~ts. 111 gcncml the dual rule cikll bc st;~tc*d by taking the statcnlcnt, of a rule and illt,c~rclti~rlging posit,ivc pohrity and nqptive polarity, A and V, 0 ant1 o, and true anti f&e. A proof containing dml rules can always bc* rcplaccd by a proof using oiily s t iuldartl rules, but the dual rule proof is soinc~tinics shorter and more clear. PTL implmnmts (lllikls of all the deduction rules. IIowt*vc~-, some of the rules art- unchaugcd W~~CIL duilli%( (l, and t,hcb I aud 0 ~I&*s ilrc &cildy tlu~l.1~. A du l.l rulcb is itpl)lit (l using the S~IUC :()II1IIliLn(l its the standitrtl rule. For ( xilll11)1~~, the rc5olu tioii :OllllnilIld ili)l)li(yl to il c:onjiixic: tion with psi t,ivc* pliwi ty uses tllc StiLt1d;trtl rule. Thrb siklllc co~n~~~and applied to a diyjunction with nogativc pditrity Uses the (IlliLl of resolution. 2.6 PTL Commands This 0111Ini~u(l rctpl;l : ts it sl~t)forlllllli~ of the existing forlllul;l by an cqaivalmt simpler formula. To simplify the whole forllluli~, simply sc*lcct the whole formula. Tllcx sillll)lific:;lt,iolrs usc~l arc 0 ocmrrf*u(*(3 of 17 7ub X.11(1 ffhc iux* rmiov~~d, lx plil(:illg tllc sllt~f0~tlllilil ColltaiIlillg tjt(*lll by illi qllivillc*llt forrllula. For (~xi~llll)l(~, A A II A I RI~E will IMYO~ILC A A II. l hc~rc~ il.r(: sin&r ~c~~~lil(:~ lli~ llt~s for othctr Op'l'iLt,OfS, 0 double Ilc~pp.tiOllS art rmmml, 1 Tf IIO sillli)lific:iltioll (:illl bc 1Iliulc, 110 n(*w liuc* is writtcbii to thcb file. This (:()llllllil.ud t ( l)lil(:( s ik c:oli,jlll~(:bioii 1)~ ik s~ii~sc~i~ of its (:olljllll(:t,s. A [l(*ft] click ikll(l il [mitltllc] (*lick hilv(s tlift mmt cblli-cts. [Left] on il coujuuct r( plil.(:(*s that whole coujunc-t iou b y timto fornmla. [Micltllc] ijl()ws you to sclcc:t morcb thiktl otw of the* coujtmcts to ;kppc;tr irk thcb fillill fonuula. W~LCI~ you click [~~~idcllc~] tliv conjunct will 1)~ outliucd, but you will still bcl itl)lt* to click c*ithcbr [~nitlcllc] or [h-f%] on othcbr coujuricts. Whc*u you (~v~~utlii~lly click [htft] il IlCW forlulllil c:olltaiilillg Olrly tllc sc~lm:tml (~0t~~juiic:t.s will b(b tlcdttcc~l. I ll( Clllil.1 Of tl IV wcb;l.k(bllit\g rnl(b will 1)~ INCV~ t,hcb sc~lm:tml forllluli1.s m tliqjuucts iustc i\d of c:oii,ju~ict,s. TtLV disjuuctioii ll1llst, IliLVC llcgiltiv(~ poliwity. You irulst soled a foixllllit whose outcrinost operator is a 1 or 3. If the optlrator k 1 (1~ Morgan s laws and nc~gatiou rulcbs for 1rda1 operators will bc applied to producct au (~ lllivdcnt, fornmla with ncgatims itppmriug ouly iktb the lowctst lcvc*l. That is, ut~gations will only 1~: applied to propositiolrnl variables. If the operator is , the forluula is rcplacccl by the orrctsl)ollding disjunction then the negation rules itrt' ilpplid rcq~catcdly to the result. For cxalnplc, selcctinbp 1A 13 will give the conclusion Av B. A simpler deduction is pcrfornd if this co~~~maxd is prcccdcd by a nunmic argument (that is, by prccctliug the coimnand 1)~ Control-l or Control-IT ). For negations, the negdion will only 1)~ piisl~ccl detail one lcvcl i~lstcild of b&g applied rccursivcly. Iiriplications will 1)~ replaced by the cyuivalcut cliqjuuct,ion, without any further application of the negilti()n rules. This (:()1~11ui~11(1 iulplcmcnts the basic rcsolu tion rule or its ltd. R.tdutiou is prcsentctl sylubolicdly in [ 11 as follows: R[A(u), B(T~)] t-+ A(tme) v B(fdse). A ldi ilil(l IV;\.lllliL idlow SCVCIXI occum~nccs of thct fornmla?l to bc r( plikd si1ll~llti~nc~~~llsly, 1)llt in PTL only one occurrcncc in coach of A and B llliky 1~ replaced. [Thcrc is a claugc r in doing this. Similar restrictions in otlicr logical systcriis &troy the Systw s c:c~lr~~ l ~t,cllc~ss. Wliilc wc :trc not niuch couc~m~t~d with conlplctcncss hcrc tlic user c:ollltl illwilys typ( t1lc rqiiird coucliisioii without usiiig il,lly tlduction c0~lllllilllds ilt0 id1 it is comfort~illg to know that, t,his sysl;c ~u is still compl~~tc?. To see this, uotc that the c:onrplctc8xlc~ss proof iu 1 l] uses ouly th(n rc3trictcd rdc. This fi\.c:t wiks poiutc cl out 1);~ Micrtiu Al,;kdi.] 1 11( lls( l IIIllSf, C110(~S(8 1;)llr li~lvlll1lil.s. First C~IOOS(~ I,WO forlllllli~s ils th(* (:()lljllll(*ts A ikilt 13. I llc!, lllil,~ t)c CllOS(~ll iii Rlly odor. YOll lllily dloos(~ two (TOll*jllllCts withiu tlic Sil.lll conjuiictioii, or - YOU can C~OOSC* two W~~O~C for1nlllils to 1)~ A a~ 1 B. After choosing A illltl B, tllc* ldiukcr thi~t outlirm tllc forluula, you ILrc poiutiug to will change to a solid ldiukcr. The uc xt, two forludas chos~~u ikr( the occurrmccs of u those foruiulas within A i1.11~1 D tllikt il.r(i to 1)~ r( l)lil.(:(*(l 1)~ trt/t! ~ltl ~~~ZSC. The% first forluulil chosen will 1~ rc~pl:~ :c!d by tm!,!*h* scw~llcl by jill?rc. The tlducd formda will 1)~ ;dtld at the) cud of the\ lmffcr. A pplyiug tllis rule is firirly tdious. I lrc* Ilc X tr ~ ~~llllllil.lld tl~~sc:ril~c~cl is ii.11 tlt,tc lllpt to simplify this Imk. This co~unmu(l is a.11 ;dt~r~~~~tiv~* to the resolution (:o1lllni~n l of thcl previous section. Instcacl of choosirig four focl~llllils,,yoii arc ouly rquird to choosc~ two. Thcs~ two forluulas must both be occurr(*nccs of tllc* sillil( f()rllllllil, iktl(l thcly arc tilk( n as the itmbr fonuulas of the clcduction (called 71 iu tlicl prcgous scdim). This IIIIIS~ bc a colljunction, and the corljnncts containing the sclcctzd formulas arc taken as A alld B. If thcb sc~lcctttd formulas arc in diffcrcnt lines, then those lines arc takctn as A ;txd B. The two sclectcd formulas must have diffcrcnt polarities. The formula having positive polarity will bc rcplaccd by j&e, and that other will hc IY plilc( d by true in the conclusion. This is often the deduction that is desired. For c~xnmplc, sclccting the two occurrences of P in P and (P CJ) WI 11 result in the conclusion Q. Also, sclccting the two occurrc~nces of CL in n A :C A la will rcbsult in j~~lsc. Thclrca is obviously no guarantee that this is always a usttful dc~dnction. This command adds two formulas at the end of the buffer. The first is the rcsolvcnt. It will bc followed immcdiatcly by its simplification. The dual resolution rule is also implcmc~nted. The formula that has negative polarity is still rcplaccd by true and the formula with negative polarity by false. The six binary modality rules (IJO, 00, 03, 00, 00 and 00) and their duals are all inl~)l~~xrl~~xltc~d by a single command. The rulcb to apply is sclectcd dopcnding on the modal operators appearing in the choscbn formu- 1il.S. For all rules tbxccpt IO that order in which the formulas to bc rcsolvcd upon arc chosen is almost irrclcvant to the conclusion drawn. (The* 00 and 00 rnlcs will 1liLVC tliffcrc~nt, but cvplivident, conclusions if their prcmiscs are chosc~n in a diffcrcrnt order.) For the 00 rule, if the first choice is I2171 and that second is DO, the conclusion is (CITL A v). The two unary modality rules (O and 0) arc also implcmcntzd by a singlcb command. (Thcx key binding can 1)~ rcmcmbcrcd by mcm,ally associating sup~~r-e with ( xl)and modal operator.) Th( appropriate: rule is chosc~n according to the opcbrator of the ~lcctctl formula. Thcsc two rules arc duals of OIIC another. e 1 11~ induction rnlc or its (Illa. is
Advertisements
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks
SAVE OUR EARTH

We need your sign to support Project to invent "SMART AND CONTROLLABLE REFLECTIVE BALLOONS" to cover the Sun and Save Our Earth.

More details...

Sign Now!

We are very appreciated for your Prompt Action!

x