÷ƒ’À; è TeX output 2000.11.02:1651‹ ÿÿÿÿ “ ým ‘# ïhtml:ï html:ŽŽ k ‘# ý• ïhtml:ï html:Ÿ,g‘ ˆ³ó1DÓít ½q G® cmr17ÜEm–ÿuNb‘ Š±edding›BÚDispla“y˜Calculi˜in“to˜LogicalŽŸ ‘:æF‘þ_ìramew›ÿuNorks–BÚ:‘mŸComparing“Tw˜elf“and“Isab‘ Š±elleŽŸ6 ’ „AAó#X«Q ff cmr12ÎJeremš›¼y–³/E.“Da˜wson‘YœŸúÆ=ïhtml:óKñ`y
cmr10²1ï html:ŽŽ’ ÿ éÎ,‘³/Ÿî ïhtml:ï html:ŽŽŽ¤™š‘wKó9ý ':
ó3
cmti10äDep›ÿp¹artment–êêof“Computer“Scienc˜e,“F‘ÿ)aculty“of“Engine˜ering“and“InformationŽ©
™š‘]…áT‘ÿ)e–ÿp¹chnolo“gy,›êêA¸\ustr“alian˜National˜UniversityŽŸ!ïhtml:ï html:ŸÞï’ —=%ÎRa‘ ȇjeev‘³/Gor›¼‘ùW}e‘YœŸúÆ=ïhtml:²2ï html:ŽŽ’ ì%Î,‘³/Ÿî ïhtml:ï html:ŽŽŽ¡‘.äA¸\utomate–ÿp¹d›êêR“e“asoning˜Gr“oup,˜Computer˜Scienc“es˜L“ab“or“atory,˜R“ese“ar“ch˜Scho“ol˜ofŽ¦‘ƒýInformation–êêScienc›ÿp¹e“and“Engine˜ering,“A¸\ustr˜alian“National“UniversityŽ¦’ ½SBandŽ¦‘ÖDep›ÿp¹artment–êêof“Computer“Scienc˜e,“F‘ÿ)aculty“of“Engine˜ering“and“InformationŽ¦‘]…áT‘ÿ)e–ÿp¹chnolo“gy,›êêA¸\ustr“alian˜National˜UniversityŽŸ!ïhtml:ï html:Ÿff‰ ffŒ Ÿšªó@ò"V
ó3
cmbx10ë@AbstractŽŸ™šó8Kñ`y
ó3
cmr10ãLogical–œframewš²!orks“are“computer“systems“whic˜h“allo˜w“a“user“to“formalise“mathemat-Ž¦ics–Sýusing“spšMÞecially“designed“languages“based“up˜on“mathematical“logic“and“Ch•²!urc“h'sŽ¦theory–3Ãof“t²!ypšMÞes.‘…õThey“can“b˜e“used“to“deriv²!e“programs“from“logical“sp˜ecications,Ž¦thereb•²!y›~guaran“teeing˜the˜correctness˜of˜the˜resulting˜programs.‘I$They˜can˜also˜bMÞeŽ¦used–¨to“formalise“rigorous“prošMÞofs“ab˜out“logical“systems.‘ÕžW‘ÿee“compare“sev²!eral“meth-Ž¦oMÞds–tbof“implemenš²!ting“the“displa˜y“(sequen˜t)“calculus“óCDF‰”
ó3
cmmib10ëCkë@RA“ãfor“relation“algebra“in“theŽ¦logical– )framewš²!orks“IsabMÞelle“and“Tw˜elf.‘ K&W‘ÿee“aim“for“an“implemen˜tation“enablingŽ¦us–¼Íto“formalise,›fwithin“the“logical“framew²!ork,˜proMÞof-theoretic“results“suc²!h“as“theŽ¦cut-elimination–¨¿theorem“for“ëCkë@RA‘{öãand“an²!y“assošMÞciated“increase“in“pro˜of“length.‘äèW‘ÿeeŽ¦discuss–¦fissues“arising“from“this“requiremen²!t.ŽŸ2"Ÿö‰™‘'™räKey‘Â4wor‘ÿp¹ds:‘·Oãlogical–z&framew²!orks,›‚ÿhigher-order“logics,˜proMÞof“systemsŽ¦‘'™rfor–¦frelation“algebra,“non-classical“logics,“automated“deduction,Ž¦‘'™rdispla²!y‘¦flogic.ŽŽŽŸDD‰ ffŒ Ÿff‰ ff $ Ÿ Ÿü^ÿóÙ“ R cmr7±1ŽŽ‘
²SuppGorted–UUbš¸ãy“an“Australian“Researc˜h“Council“Small“Researc˜h“Gran˜t.ŽŸ Ÿü^ÿ±2ŽŽ‘
²SuppGorted–UUbš¸ãy“an“Australian“Researc˜h“Council“Queen“ElizabšGeth“I˜I“F‘ÿ*ªello¸ãwship.ŽŽŸ( ‘&¦fóOp®0J
ó3
cmsl10ëOPreprinš²!t–¦fsubmitted“to“Elsevier“Preprin˜t‘v|û2“No˜v˜em˜bMÞer“2000ŽŽŒ‹ * “ ým ‘# ïhtml:ï html:ŽŽ k ‘# ý• ïhtml:ï html:Ÿ
óNÂÖN ff cmbx12ëN1Ž‘LËInŒÌtros3duction–ffand“Motiv‘ÿ™ationŽŸÕVóX«Q cmr12¹Logical–Êframewš¬rorks“are“computer“systems“whic˜h“allo˜w“a“user“to“formaliseŽ¤€ mathematics–Üusing“spšSŽecially“designed“languages“based“up˜on“mathematicalŽ¡logic–M³and“Ch•¬rurc“h's–M³theory“of“t¬rypšSŽes.‘ bThey“can“b˜e“used“to“deriv¬re“programsŽ¡from–´ological“spSŽecications,‘¿Gtherebš¬ry“guaran˜teeing“the“correctness“of“the“result-Ž¡ing–âprograms.‘ôIThey“can“also“bšSŽe“used“to“formalise“rigorous“pro˜ofs“ab˜out“logicalŽ¡systems.Ž©€ ‘ŸôRelation–1¡algebras“[ï)html:12ï html:Ž‘¿ø]“are“extensions“of“BošSŽolean“algebras;‘oNwhereas“Bo˜oleanŽ¡algebras–nmošSŽdel“subsets“of“a“giv¬ren“set,‘†ñrelation“algebras“mo˜del“binary“relationsŽ¡on–ta“givš¬ren“set.‘*CRelation“algebras“ha˜v˜e“opSŽerations“suc˜h“as“relational“compSŽo-Ž¡sition–bcand“relational“con•¬rv“erse,‘ÀRand–bcBošSŽolean“op˜erations“sucš¬rh“as“in˜tersectionŽ¡(conjunction)–¬wand“complemen¬rt“(negation).‘~NRelation“algebras“form“the“basisŽ¡of–ó¢relational“databases“[ï.html:6ï html:Ž‘ßü]“and“of“the“spšSŽecication“and“pro˜of“of“correctness“ofŽ¡programs,–ê¨particularly“in“the“st¬ryle“of“Mili“[ï%html:15ï html:Ž‘¿ø].Ž¦‘ŸôDisplaš¬ry–ÍÀLogic“[ï$html:1ï html:Ž‘ßü]“is“a“generalised“sequen˜t“framew˜ork“for“non-classical“logics,Ž¡based–žùon“the“Genš¬rtzen“sequen˜t“calculus“[ï#html:7ï html:Ž‘ßü].‘UÔIts“adv‘ÿXäan˜tages“include“a“genericŽ¡cut-elimination–Š8theorem,‘‚whicš¬rh“applies“whenev˜er“the“rules“for“the“displa˜y“cal-Ž¡culus–,0satisfy“certain,›|’easily“c•¬rhec“k“ed,˜conditions.‘ýxIt–,0is“an“extremely“generalŽ¡logical–4Àformalism,‘GFapplicable“to“man¬ry“(classical“and“non-classical)“logics“in“aŽ¡uniform›±w•¬ra“y˜[ï#html:10ï html:Ž–¿ø],‘F¯[ï4html:22ï html:Ž“].‘ôŽThe˜generalit•¬ry˜of˜the˜displa“y˜framew“ork˜means˜that˜es-Ž¡senš¬rtially–;9the“same“meta-lev˜el“proSŽofs“w˜ork“for“man˜y“dieren˜t“logics.‘þfA‘;
rigorousŽ¡mecš¬rhanical–…$formalisation“of“suc˜h“proSŽofs“is“then“widely“applicable“and“w˜orthŽ¡pursuing.‘ xšIn–U;this“papSŽer“wš¬re“discuss“the“implemen˜tation“of“óQDF‰”
cmmib10ëQuUóPÂÖN cmbx12ëPRA¹,“a“displa˜yŽ¡calculus–;for“relation“algebras,‘µßas“a“case“study“for“exploring“v‘ÿXäarious“methoSŽdsŽ¡for–ê¨sucš¬rh“a“mec˜hanical“formalisation“of“displa˜y“calculi“in“general.Ž¦‘ŸôDisplaš¬ry–ecalculi“extend“Gen˜tzen's“language“of“sequen˜ts“with“extra,‘2rcomplex,Ž¡ó·ág£ cmmi12¼n¹-ary–¸structural“connectivš¬res,‘|in“addition“to“Gen˜tzen's“sole“structural“connec-Ž¡tivš¬re,‘/Vthe–!™\comma".‘Ý´Whereas“Gen˜tzen“assumed“the“comma“to“bšSŽe“asso˜ciativ¬re,Ž¡comm•¬rutativ“e–H1and“inherenš¬rtly“pSŽoly-v‘ÿXäalen˜t,‘h¯displa˜y“calculi“mak˜e“no“suc˜h“implicitŽ¡assumptions.‘
èPropSŽerties–`Àsuc¬rh“as“these“are“explicitly“stated“as“structural“rules.Ž¡F‘ÿVor–a example,›~¾ëQuUëPRA¹-sequen¬rts“are“built“using“a“binary“comma,˜a“binary“semi-Ž¡colon,›\šand–unary“ó!",š
cmsy10¿“¹and“¿“¹structural“connectiv•¬res.‘°¿Th“us,˜whereas‘Gen“tzen'sŽ¡sequen¬rts›µ –†Å¿`“¹˜assume˜that˜ ˜and˜˜are˜comma-separated˜lists˜of˜form¬rulae,Ž¡ëQuUëPRA¹-sequen¬rts–ͼX‘sV¿`‘Ó¼Y›¡=¹assume“that“¼X‘öP¹and“¼Y˜¹are“complex“tree-lik¬re“structuresŽ¡built–ê¨from“form¬rulae“together“with“comma,“semicolon,“¿“¹and“¿¹.Ž¦‘ŸôThe–!?dening“feature“of“displaš¬ry“calculi“is“that“in“all“logical“in˜troSŽductionŽ¡rules,‘ìçthe–¹Aprincipal“formš¬rula“is“alw˜a˜ys“\displa˜y˜ed"“as“the“whole“of“the“righ˜t-Ž¡hand–‡Ÿor“left-hand“side.‘ÅF‘ÿVor“example,›®Ýthe“rule“(ëPLK¹-Ž‘ù_¿`‘`~_¹),˜shoš¬rwn“bSŽelo˜w“left,Ž¡is–ûòtš¬rypical“of“Gen˜tzen's“sequen˜t“calculi“lik˜e“ëPLK¹,“while“the“rule“(ëQuUëPRA¹-Ž‘$J¿`‘&}_¹)ŽŽŸ( ’ ä®2ŽŽŒ‹ v “ ým ‘# ïhtml:ï html:ŽŽ k ýŸ ‘# ¹shoš¬rwn–ê¨on“the“righ˜t“is“t˜ypical“of“displa˜y“calculi:ŽŸÈäŸ÷áÅ‘\´þ –UR¿`“¹¼;–ÿþPSŽ;“QŽ‘XþŸ[«‰ zà D=ÞŸ
ýι –UR¿`“¹¼;‘ÿþP‘Ln¿_‘ª¨¼QŽŽŽŽ’ v¹(ëPLK¹-Ž‘î3¿`–UR_¹)Ÿ÷áÅ‘4ã¼X‘FÕ¿`“¼PSŽ;‘ÿþQŽ‘03Ÿ[«‰ zà 8Š,Ÿ
ýÎX‘FÕ¿`“¼P‘Ln¿_‘ª¨¼QŽŽŽŽ‘iðr¹(ëQuUëPRA¹-Ž‘"=¿`“_¹)ŽŸ ](‘# In•¬rtuitiv“ely‘ÿV,‘ÚSto–Ö>use“this“displaš¬ry“calculus“rule“do˜wn˜w˜ards“on“a“sequen˜t“¼X‘ ñƒŸû¥2ó¾KÈ cmsy8À0Ž‘¿`‘UR¼Y‘œpŸû¥2À0Ž‘j©¹,Ž¤€ ‘# evš¬rerything–„$other“than“(¼PSŽ;‘ÿþQ¹)“m˜ust“bSŽe“mo˜v˜ed“in˜to“the“complex“structure“¼X‘u§¹onŽ¡‘# the–mÊleft“of“¿`¹,‘†Ãtherebš¬ry“displa˜ying“the“structure“(¼PSŽ;‘ÿþQ¹)“as“the“whole“of“the“righ˜t-Ž¡‘# hand–Zside.‘¾÷There“are“rules“whicš¬rh“enable“an˜y“giv˜en“structure“to“bSŽe“displa˜y˜ed.Ž¡‘# After–ãthe“rule“application“wš¬re“can“\undispla˜y"“the“mo˜v˜ed“material“bac˜k“to“itsŽ¡‘# original–ŠBpSŽosition“(revš¬rersing“the“displa˜y“steps“used),‘²)so“that“the“sole“purpSŽoseŽ¡‘# of–·Èthis“rule“is“to“\rewrite"“some“(¼PSŽ;‘ÿþQ¹)“to“¼P‘䃿_‘B½¼Q“¹somewhere“inside“¼Y‘œpŸû¥2À0Ž‘j©¹.‘'ëSee“[ï!html:9ï html:Ž‘ßü]Ž¡‘# for–ê¨a“full“accoun¬rt.Ž©€ ‘4ŸôIsabšSŽelle–@)is“an“automated“pro˜of“assistanš¬rt“[ï"html:17ï html:Ž‘¿ø].‘ Its“meta-logic“is“an“in˜tuition-Ž¡‘# istic–—Ýtš¬rypSŽed“higher-order“logic,‘¨lsucien˜t“to“suppSŽort“the“built-in“inference“stepsŽ¡‘# of–QEhigher-order“unication“and“term“rewriting.‘¿IsabSŽelle“accepts“inference“rulesŽ¡‘# of–Éthe“form“\from“¼ŸÌÌó|{Y cmr8º1Ž–À¼;›ÿþŸÌ̺2Ž“¼;˜:˜:˜:Ž‘Êœ;˜ŸÌÌó×2 cmmi8½nŽ‘¨P¼;‘ꦹinferŽ‘!°¼‘ ªO¹"–Éwhere“the“¼ŸÌ̽iŽ‘.g¹and“¼‘sܹare“expressionsŽ¡‘# of–jWthe“IsabSŽelle“meta-logic,›ŠCor“are“expressions“using“a“new“syn¬rtax,˜dened“b¬ryŽ¡‘# the–ãñuser,‘"Cfor“some“\ob‘ §ject“logic".‘$»An“IsabšSŽelle“user“can“enco˜de“a“particularŽ¡‘# calculus–aZ¿CŸÌ̽LŽ‘ ©2¹for“some“logic“¼L“¹as“an“\ob‘ §ject“logic"“b¬ry“using“these“rule“templatesŽ¡‘# to–8×encoSŽde“the“set“of“inference“rules“of“¿CŸÌ̽LŽ‘Gع.‘ #lF‘ÿVor“example,‘Œbif“¿CŸÌ̽LŽ‘€¯¹is“a“naturalŽ¡‘# deduction–„Œcalculus,›˜øthen“the“¼ŸÌ̽iŽ‘éf¹and“¼‘.Û¹will“bSŽe“form¬rulae“of“¼L¹,˜whereas“if“¿CŸÌ̽LŽ‘ Ìd¹is“aŽ¡‘# sequenš¬rt–ëÖcalculus,‘ì"then“the“¼ŸÌ̽iŽ‘P°¹and“¼‘–%¹will“bSŽe“sequen˜ts“of“¿CŸÌ̽LŽ‘Gع.‘