; TeX output 1999.05.26:1516 LfT rhtml: html:LBNDt G G cmr17The7tdecidabilitqyofguardedxedpsointlogiclύ &XQ cmr12EricrhGr adel(lύ l/%"V
cmbx10Abstractٜ/sK`y
cmr10GuardedxedpGointlogicsareobtainedbyaddingleastandgreatestxedpGoints
rtodtheguardedfragmentsofrst-orderlogicthatwererecentlyintroGducedbyAndrGekqa, rvqanBenthemandNGemeti.GuardedxedpGointlogicscanalsobGeviewedasthenat- ruralcommonextensionsofthemoGdal
b>
cmmi10-calculusandtheguardedfragments.aIna rjointfpapGerwithIgorW*alukiewicz,kcweprovedrecentlythatthesatisabilityproblems rforxguardedxedpGointlogicsaredecidableandcompletefordeterministicdoubleex- rpGonential{7time.mThatproofreliesonalternatingautomataontreesandonaforgetful rdeterminacy[theoremforgamesongraphswithunbGoundedbranching.9W*epresenthere ranelementaryproGofforthedecidabilityofguardedxedpGointlogicswhichisbasedon rguardedXobisimulations,Y6atreemoGdelpropertyforguardedlogicsandaninterpretation rintoUUthemonadicsecond-ordertheoryofcountabletrees."A r2N ff cmbx12Contentsύ rhtml:3"V
3
cmbx101lInttroYduction html:.2 rhtml:2lGuarded2xedpYointtlogics html: