%PDF-1.2 3 0 obj << /Length 4 0 R >> stream 1 0 0 1 162.77 749.51 cm BT /F82 20.66 Tf 0 0 Td[(Explaining)]TJ/F25 20.66 Tf 101.64 0 Td[(ALC)]TJ/F82 20.66 Tf 48 0 Td[(Subsumption)]TJ/F83 10.91 Tf -140.79 -27.75 Td[(Alex)-249(Bor)10(gida)]TJ/F43 7.97 Tf 61.4 3.96 Td[(1)]TJ/F83 10.91 Tf 0 -3.96 Td[(,)-1250(Enrico)-250(Franconi)]TJ/F84 10.91 Tf 101.22 0 Td[(and)]TJ/F83 10.91 Tf 23.93 0 Td[(Ian)-250(Horr)18(ocks)]TJ/F43 7.97 Tf 62.53 3.96 Td[(2)]TJ/F85 8.97 Tf -378.59 -36.95 Td[(Abstract.)]TJ/F86 8.97 Tf 42.37 0 Td[(Kno)25(wledge)-209(representation)-208(systems,)-209(including)-209(ones)-210(based)]TJ -42.37 -10.42 Td[(on)-392(Description)-390(Logics)-392(\050DLs\051,)-391(use)-392(e)16(xplanation)-391(f)10(acilities)-391(to,)-392(among)]TJ 0 -10.41 Td[(others,)-535(deb)21(ug)-536(kno)26(wledge)-535(bases.)-535(Until)-535(no)26(w)65(,)-536(such)-535(f)10(acilities)-534(were)]TJ 0 -10.41 Td[(not)-335(a)20(v)25(ailable)-335(for)-335(e)15(xpressi)27(v)15(e)-336(DLs,)-335(whose)-334(reasoning)-334(is)-336(an)-335(un-natural)]TJ 0 -10.41 Td[(refutation-based)-250(tableau.)-252(W)80(e)-252(of)25(fer)-252(a)-253(solution)-251(based)-252(on)-253(a)-253(sequent)-251(cal-)]TJ 0 -10.41 Td[(culus)-226(that)-227(is)-227(closely)-226(related)-226(to)-226(the)-227(tableau)-226(implementation,)-224(e)15(xploiting)]TJ 0 -10.41 Td[(its)-238(optimisations.)-235(The)-238(resulting)-236(proofs)-237(are)-238(pruned)-236(and)-238(then)-237(presented)]TJ 0 -10.41 Td[(as)-250(simply)-249(as)-249(possible)-249(using)-249(templates.)]TJ/F83 10.91 Tf 0 -26.21 Td[(1)-1000(Intr)18(oduction)]TJ/F86 8.97 Tf 0 -15.89 Td[(The)-349(usability)-347(of)-349(kno)26(wledge)-348(representation)-347(systems,)-348(including)-347(ones)]TJ 0 -10.41 Td[(based)-278(on)-277(Description)-277(Logics)-277(\050DLs\051)-277(is)-278(considerably)-276(enhanced)-277(by)-278(the)]TJ 0 -10.41 Td[(ability)-308(to)-309(e)15(xplain)-309(inferences)-307(to)-309(kno)25(wledge-base)-307(de)26(v)15(elopers)-308(who)-309(are)]TJ 0 -10.41 Td[(not)-291(f)10(amiliar)-291(with)-291(the)-291(implementation)-289(of)-291(the)-291(reasoner)-290([10].)-291(F)15(or)-291(DLs,)]TJ 0 -10.41 Td[(inferring)-249(subsumption)-248(relationships)-248(is)-250(a)-250(fundamental)-249(reasoning)-248(task,)]TJ 0 -10.41 Td[(and)-322(its)-322(e)15(xplanation)-321(is)-322(relati)26(v)15(ely)-322(natural)-321(for)-322(systems)-321(based)-321(on)-322(struc-)]TJ 0 -10.41 Td[(tural)-214(subsumption)-213(algorithms)-213([10].)-214(Ho)25(we)26(v)15(er)40(,)-214(such)-215(algorithms)-213(are)-214(un-)]TJ 0 -10.41 Td[(able)-262(to)-262(deal)-262(with)-262(a)-263(more)-261(comple)16(x)-262(language)-262(such)-261(as)]TJ/F71 8.97 Tf 185.77 0 Td[(ALC)]TJ/F86 8.97 Tf 19.08 0 Td[(.)-263(T)80(ableaux-)]TJ -204.85 -10.41 Td[(based)-382(systems,)-381(on)-382(the)-382(other)-382(hand,)-381(can)-382(deal)-382(with)]TJ/F71 8.97 Tf 183.28 0 Td[(ALC)]TJ/F86 8.97 Tf 22.51 0 Td[(\050and)-382(much)]TJ -205.79 -10.41 Td[(more)-234(comple)16(x)-234(languages\051,)-232(b)20(ut)-234(the)-234(reasoning)-233(method)-233(does)-233(not)-234(lead)-234(to)]TJ 0 -10.41 Td[(a)-305(natural)-303(e)15(xplanation)-303(of)-304(subsumption)-303(inferences)-302(because)-304(it)-304(is)-304(based)]TJ 0 -10.42 Td[(on)-452(a)-452(refutation/unsatisability)-448(approach;)-451(for)-452(e)16(xample,)-451(it)-452(w)10(ould)]TJ 0 -10.41 Td[(probably)-189(not)-190(be)-189(useful)-190(to)-190(ha)21(v)15(e)-190(the)-190(subsumption)]TJ/F71 8.97 Tf 167.75 0 Td[(8)]TJ/F70 8.97 Tf 5.12 0 Td[(R:)]TJ/F15 8.97 Tf 9.59 0 Td[(\050)]TJ/F70 8.97 Tf 3.59 0 Td[(C)]TJ/F71 8.97 Tf 7.22 0 Td[(u)]TJ/F70 8.97 Tf 6.16 0 Td[(D)]TJ/F15 8.97 Tf 7.85 0 Td[(\051)]TJ/F71 8.97 Tf 6.14 0 Td[(v)-286(8)]TJ/F70 8.97 Tf 14.85 0 Td[(R:C)]TJ/F86 8.97 Tf -228.27 -10.41 Td[(e)15(xplained)-227(by)-227(the)-228(f)11(act)-228(that)]TJ/F15 8.97 Tf 91.68 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(8)]TJ/F70 8.97 Tf 5.12 0 Td[(R:)]TJ/F15 8.97 Tf 9.59 0 Td[(\050)]TJ/F70 8.97 Tf 3.59 0 Td[(C)]TJ/F71 8.97 Tf 8.51 0 Td[(u)]TJ/F70 8.97 Tf 7.45 0 Td[(D)]TJ/F15 8.97 Tf 7.85 0 Td[(\051\051)]TJ/F71 8.97 Tf 8.47 0 Td[(u)-145(9)]TJ/F70 8.97 Tf 12.56 0 Td[(R:)]TJ/F71 8.97 Tf 9.6 0 Td[(:)]TJ/F70 8.97 Tf 6.14 0 Td[(C)]TJ/F86 8.97 Tf 9.26 0 Td[(is)-228(not)-227(satisable.)]TJ -174.18 -10.41 Td[(This)-343(problem)-342(is)-344(not)-343(restricted)-342(to)-344(DL-based)-342(systems:)-343(in)-343(other)-343(ar)20(-)]TJ -9.22 -10.41 Td[(eas)-310(of)-309(theorem)-309(pro)16(ving,)-310(there)-309(is)-310(a)-309(desire)-309(to)-310(pro)15(vide)-309(e)15(xplanations)-308(of)]TJ 0 -10.41 Td[(why)-378(theorems)-382(hold,)-383(yet)-383(the)-384(proof)-382(techniques)-382(\050e.g.,)-383(resolution\051)-382(are)]TJ 0 -10.41 Td[(not)-287(natural.)-285(The)-287(solution)-285(in)-287(such)-287(situations)-285([9,)-287(7])-286(has)-287(been)-286(to)-287(nd)]TJ 0 -10.41 Td[(w)10(ays)-351(to)-350(transform)-350(proofs)-350(from)-351(their)-350(original)-350(form)-350(into)-351(some)-350(more)]TJ 0 -10.41 Td[(natural)-402(form,)-402(such)-403(as)]TJ/F87 8.97 Tf 90.91 0 Td[(natur)16(al)-403(deduction)]TJ/F86 8.97 Tf 68.87 0 Td[(\050ND\051)-402(proofs.)-402(From)-402(the)]TJ -159.78 -10.41 Td[(be)15(ginning,)-334(ND)-335(proofs)-335(ha)20(v)16(e)-336(been)-335(claimed)-334(to)-336(be)-335(easier)-335(to)-335(present)-335(to)]TJ 0 -10.41 Td[(users,)-267(and)-266(natural)-266(language)-266(generation)-266(systems)-266(ha)21(v)15(e)-267(e)25(v)15(en)-267(been)-266(b)20(uilt)]TJ 0 -10.42 Td[(to)-202(produce)-200(sophisticated)-200(English)-200(output)-201(from)-201(ND)-201(proofs)-201(\050e.g.,)]TJ/F88 7.17 Tf 220.97 0 Td[(V)-62(E)-62(R)-62(B)]TJ/F86 8.97 Tf 20.9 0 Td[(-)]TJ/F88 7.17 Tf -241.64 -10.41 Td[(M)-62(O)-62(B)-62(I)-62(L)]TJ/F86 8.97 Tf 27.01 0 Td[(project)-211([8]\051.)-211(Related)-212(to)-212(ND)-211(proof)-212(systems)-211(are)]TJ/F87 8.97 Tf 161.9 0 Td[(sequent)-211(calculi)]TJ/F86 8.97 Tf 53.7 0 Td[(,)]TJ -242.84 -10.41 Td[(introduced)-273(by)-275(Gentzen.)-273(Such)-274(calculi)-274(axiomatise)-273(the)-274(entailment)-273(rela-)]TJ 0 -10.41 Td[(tion,)-249(which)-249(has)-250(an)-249(ob)15(vious)-249(parallel)-248(with)-249(the)-250(subsumption)-248(relation.)]TJ 9.22 -10.41 Td[(Ho)26(we)25(v)15(er)41(,)-319(most)-319(sequent)-318(calculi)-318(include)-318(reasoning)-317(rules)-319(and)-318(nota-)]TJ -9.22 -10.41 Td[(tion)-238(that)-239(are)-238(less)-238(than)-238(natural)-238(in)-239(the)-238(case)-238(of)-239(DLs,)-238(such)-238(as)-238(mo)15(ving)-238(for)20(-)]TJ 0 -10.41 Td[(mul)-273(from)-273(one)-273(side)-274(of)-273(the)-273(turnstile)-273(to)-273(the)-274(other)56(.)-274(Just)-273(as)-273(importantly)66(,)]TJ 0 -10.41 Td[(it)-222(is)-221(undesirable)-220(to)-222(ha)20(v)16(e)-222(an)-222(e)16(xplanation)-220(component)-221(that)-221(is)-221(dissociated)]TJ 0 -10.41 Td[(from)-287(the)-287(implementation)-285(of)-287(the)-287(reasoner)-286(\050the)-287(tableaux)-286(technique,)-286(in)]TJ 0 -10.41 Td[(our)-286(case\051.)-286(This)-286(is)-286(both)-286(because)-286(of)-286(ef)25(cienc)16(y)-286(and)-286(the)-286(possible)-285(de)25(via-)]TJ 0 -10.41 Td[(tion)-249(between)-249(implementation)-247(and)-250(e)16(xplanation)-249([14,)-249(10].)]TJ 9.22 -10.41 Td[(W)81(e)-289(propose)-287(using)-288(a)-288(slightly)-287(e)15(xtended)-287(tableaux)-287(algorithm)-287(that,)-288(by)]TJ -9.22 -10.42 Td[(k)10(eeping)-286(track)-286(of)-286(the)-286(undesirable)-285(steps)-286(in)41(v)20(olv)15(ed)-286(in)-286(both)-286(the)-287(reduc-)]TJ 0 -10.41 Td[(tion)-194(of)-193(the)-194(subsumption)-192(problem)-192(to)-194(an)-193(unsatisability)-192(problem)-193(allo)26(ws)]TJ 0 -10.41 Td[(the)-335(structure)-334(of)-335(the)-335(original)-335(subsumption)-333(inference)-334(to)-335(be)-335(preserv)16(ed)]TJ 0 -10.41 Td[(\050Section)-267(2\051.)-268(Interestingly)67(,)-268(the)-268(tableaux)-267(proof)-267(can)-268(be)-267(represented)-267(as)-268(a)]TJ ET -120.66 -569.2 245.08 0.8 re f 1 0 0 1 -120.66 -575.25 cm BT /F44 5.98 Tf 0 0 Td[(1)]TJ/F89 7.97 Tf 6.15 -2.81 Td[(Dept.)-249(of)-250(Computer)-250(Science,)-250(Rutgers)-250(Uni)25(v)15(ersity)65(,)-250(USA)]TJ/F90 7.97 Tf 0.83 -8.14 Td[(borgida@cs.rutgers.edu)]TJ/F44 5.98 Tf -6.98 -6.29 Td[(2)]TJ/F89 7.97 Tf 6.15 -2.82 Td[(Dept.)-249(of)-250(Computer)-250(Science,)-250(Uni)25(v)15(ersity)-250(of)-250(Manchester)40(,)-250(UK)]TJ/F49 7.97 Tf 0.83 -8.14 Td[(f)]TJ/F90 7.97 Tf 4.23 0 Td[(franconi)]TJ/F49 7.97 Tf 38.26 0 Td[(j)]TJ/F90 7.97 Tf 2.35 0 Td[(horrocks)]TJ/F49 7.97 Tf 38.26 0 Td[(g)]TJ/F90 7.97 Tf 4.23 0 Td[(@cs.man.ac.uk)]TJ/F86 8.97 Tf 168.7 542.77 Td[(sequence)-327(of)-329(rules)-327(in)-328(a)-329(simple)-327(v)25(ariant)-327(of)-328(the)-328(sequent)-328(calculus.)-327(Each)]TJ 0 -10.41 Td[(rule)-407(application)-406(in)-407(this)-406(sequent)-406(calculus)-406(can)-407(then)-406(be)-407(e)15(xplained)-406(in)]TJ 0 -10.41 Td[(terms)-273(of)-273(one)-273(or)-273(more)-272(steps)-273()-273(some)-272(optional)-272(steps)-273(are)-273(omitted)-272(when-)]TJ 0 -10.41 Td[(e)25(v)15(er)-340(possible,)-338(to)-339(produce)-339(a)-339(simpler)-339(proof)-339()-339(resulting)-338(in)-340(a)-339(parsimo-)]TJ 0 -10.41 Td[(nious)-250(yet)-249(understandable)-247(proof)-249(presentation)-248(\050Section)-249(3\051.)]TJ/F83 10.91 Tf 0 -28.6 Td[(2)-1000(Subsumption)-250(Pr)18(oofs)-249(with)-250(T)92(ableaux)]TJ/F86 8.97 Tf 0 -17.64 Td[(In)-453(order)-451(to)-453(solv)16(e)-452(a)]TJ/F87 8.97 Tf 76.44 0 Td[(subsumption)]TJ/F86 8.97 Tf 49.39 0 Td[(problem)-451(using)-452(a)-452(tableaux-based)]TJ -125.83 -10.41 Td[(procedure)-334()-335(which)-335(solv)16(es)-335(unsatisability)-333(problems)-333()-336(the)-334(subsump-)]TJ 0 -10.41 Td[(tion)-341(has)-341(to)-341(be)-340(reduced)-340(to)-341(an)-341(equi)26(v)25(alent)-341(satisability)-339(problem.)-340(That)]TJ 0 -10.41 Td[(is,)-401(if)-400(we)-400(w)10(ant)-400(to)-400(check)-399(that)-400(a)-400(concept)-400(e)16(xpression)]TJ/F70 8.97 Tf 188.84 0 Td[(C)]TJ/F86 8.97 Tf 10.81 0 Td[(is)-400(subsumed)]TJ -199.65 -10.41 Td[(by)-367(a)-367(concept)-366(e)15(xpression)]TJ/F70 8.97 Tf 92.23 0 Td[(D)]TJ/F86 8.97 Tf 7.85 0 Td[(,)-367(we)-367(should)-366(check)-366(whether)-366(the)-367(concept)]TJ/F70 8.97 Tf -100.08 -10.41 Td[(C)]TJ/F71 8.97 Tf 10.11 0 Td[(u)-322(:)]TJ/F70 8.97 Tf 15.18 0 Td[(D)]TJ/F86 8.97 Tf 11.2 0 Td[(is)-373(not)-373(satisable,)-372(since)]TJ/F70 8.97 Tf 87.37 0 Td[(C)]TJ/F71 8.97 Tf 11.88 0 Td[(v)]TJ/F70 8.97 Tf 11.83 0 Td[(D)]TJ/F86 8.97 Tf 11.21 0 Td[(if)25(f)]TJ/F70 8.97 Tf 11.59 0 Td[(C)]TJ/F71 8.97 Tf 10.1 0 Td[(u)-323(:)]TJ/F70 8.97 Tf 15.18 0 Td[(D)]TJ/F71 8.97 Tf 12.52 0 Td[(v)-521(?)]TJ/F86 8.97 Tf 19 0 Td[(.)-374(F)15(or)]TJ -227.17 -10.41 Td[(e)15(xample,)-249(in)-249(order)-250(to)-249(pro)15(v)16(e)-250(that)-13625(\0501\051)]TJ/F15 8.97 Tf 0 -13.7 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(>)-229(u)-228(8)]TJ/F78 8.97 Tf 22.53 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F71 8.97 Tf 32.85 0 Td[(t)-228(9)]TJ/F78 8.97 Tf 13.31 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051)]TJ/F49 7.97 Tf -228.47 -9.17 Td[(v)]TJ/F15 8.97 Tf 8.94 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.25 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051\051)]TJ/F46 7.97 Tf 10.75 0 Td[(;)]TJ/F86 8.97 Tf -166.85 -16.09 Td[(it)-259(is)-259(necessary)-257(to)-259(pro)15(v)16(e)-259(that)-259(the)-258(follo)26(wing)-259(concept)-257(does)-259(not)-258(ha)20(v)15(e)-258(an)15(y)]TJ 0 -10.41 Td[(model:)]TJ/F71 8.97 Tf 11.96 -10.41 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(>)-229(u)]TJ -35.92 -10.41 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F15 8.97 Tf 6.15 0 Td[(\050\050)]TJ/F71 8.97 Tf 7.16 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051)]TJ/F71 8.97 Tf 5.63 0 Td[(t)]TJ/F15 8.97 Tf 8.19 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051)]TJ/F71 8.97 Tf 7.17 0 Td[(u)]TJ -198.87 -10.41 Td[(:9)]TJ/F78 8.97 Tf 11.26 0 Td[(friend)]TJ/F70 8.97 Tf 28.25 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051)]TJ/F89 7.97 Tf 7.17 0 Td[(.)]TJ/F86 8.97 Tf -147.67 -10.41 Td[(Moreo)16(v)15(er)41(,)-401(tableaux)-400(algorithms)-399(typically)-400(transform)-399(the)-400(resulting)]TJ -9.22 -10.41 Td[(concept)-337(into)-338(ne)16(gation)-332(normal)-337(form)-337(using)-338(a)-337(combination)-336(of)-338(deMor)21(-)]TJ 0 -10.41 Td[(gan')60(s)-277(rules)-276(and)-276(modal)-276(normalisations)-274(\050e.g.,)]TJ/F71 8.97 Tf 157.56 0 Td[(:9)]TJ/F70 8.97 Tf 11.27 0 Td[(R:C)]TJ/F86 8.97 Tf 19.29 0 Td[(if)25(f)]TJ/F71 8.97 Tf 10.72 0 Td[(8)]TJ/F70 8.97 Tf 5.12 0 Td[(R:)]TJ/F71 8.97 Tf 9.6 0 Td[(:)]TJ/F70 8.97 Tf 6.14 0 Td[(C)]TJ/F86 8.97 Tf 7.22 0 Td[(\051)-277([4].)]TJ -226.92 -10.41 Td[(F)15(or)-297(e)15(xample,)-296(the)-297(abo)15(v)15(e)-297(concept)-296(w)10(ould)-296(be)-297(immediately)-296(transformed)]TJ 0 -10.42 Td[(into)-268(the)-267(follo)26(wing)-267(concept,)-266(which)-267(should)-267(be)-267(then)-267(check)11(ed)-268(for)-267(unsat-)]TJ 0 -10.41 Td[(isability:)]TJ/F71 8.97 Tf 11.96 -10.41 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(>)-229(u)]TJ -35.92 -10.41 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050\050)]TJ/F71 8.97 Tf 7.17 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F71 8.97 Tf 5.63 0 Td[(u)]TJ/F15 8.97 Tf 8.19 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051)]TJ/F71 8.97 Tf 7.17 0 Td[(u)]TJ -192.73 -10.41 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(u)-228(:)]TJ/F78 8.97 Tf 14.33 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051\051)]TJ/F89 7.97 Tf 7.16 0 Td[(.)]TJ/F86 8.97 Tf -153.81 -10.41 Td[(Thus,)-258(the)-258(structure)-257(of)-258(the)-258(original)-257(problem)-257(is)-258(completely)-257(lost,)-258(and)]TJ -9.22 -10.41 Td[(the)-319(e)15(xplanation)-317(of)-318(the)-318(proof)-318(steps)-318(generated)-317(by)-318(the)-319(tableaux)-317(proce-)]TJ 0 -10.41 Td[(dure)-245(w)11(ouldn')19(t)-245(be)-245(understandable)-242(by)-245(the)-244(user)55(.)-244(These)-244(problems)-244(can)-244(be)]TJ 0 -10.41 Td[(o)15(v)15(ercome)-249(using)-249(a)-250(combination)-247(of)]TJ/F87 8.97 Tf 122.01 0 Td[(lazy)-249(unfolding)]TJ/F86 8.97 Tf 53.3 0 Td[(and)]TJ/F87 8.97 Tf 15.19 0 Td[(ta)10(g)10(ging)]TJ/F86 8.97 Tf 27.22 0 Td[(.)]TJ -208.5 -10.41 Td[(Lazy)-191(unfolding)-190(is)-191(an)-191(optimisation)-189(technique,)-190(widely)-190(used)-191(in)-191(imple-)]TJ -9.22 -10.41 Td[(mented)-283(systems,)-282(that)-282(has)-283(the)-283(ef)25(fect)-282(of)-283(delaying)-282(the)-283(normalisation)-281(of)]TJ 0 -10.41 Td[(compound)-196(concepts)-196(until)-196(it)-197(is)-197(required)-196(by)-197(the)-197(progress)-196(of)-196(the)-197(tableaux)]TJ 0 -10.42 Td[(e)15(xpansion)-329([5].)-329(In)-330(the)-329(generation)-329(of)-329(the)-330(proof,)-329(the)-329(combination)-328(of)-330(a)]TJ 0 -10.41 Td[(normalisation)-260(and)-260(a)-261(subsequent)-260(e)15(xpansion)-259(rule)-261(corresponds)-259(to)-261(a)-261(sin-)]TJ 0 -10.41 Td[(gle)-295(proof)-295(step.)-295(F)16(or)-295(e)15(xample,)-294(normalising)]TJ/F71 8.97 Tf 150.61 0 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050)]TJ/F70 8.97 Tf 3.59 0 Td[(a)]TJ/F71 8.97 Tf 6.93 0 Td[(u)]TJ/F70 8.97 Tf 8.19 0 Td[(b)]TJ/F15 8.97 Tf 3.95 0 Td[(\051)]TJ/F86 8.97 Tf 6.23 0 Td[(to)]TJ/F71 8.97 Tf 9.63 0 Td[(:)]TJ/F70 8.97 Tf 6.14 0 Td[(a)]TJ/F71 8.97 Tf 7.24 0 Td[(t)-263(:)]TJ/F70 8.97 Tf 14.65 0 Td[(b)]TJ/F86 8.97 Tf 3.95 0 Td[(,)-295(fol-)]TJ -227.25 -10.41 Td[(lo)25(wed)-309(by)-309(an)-309(application)-308(of)-309(the)-309(tableaux)]TJ/F71 8.97 Tf 147.21 0 Td[(t)]TJ/F87 8.97 Tf 6.15 0 Td[(-rule)]TJ/F86 8.97 Tf 17.43 0 Td[(,)-309(w)10(ould)-309(be)-309(seen)-309(as)-309(a)]TJ -170.79 -10.41 Td[(single)-249(proof)-249(step)-250(e)16(xplained)-249(by)-249(some)-249(sort)-250(of)]TJ/F71 8.97 Tf 156.76 0 Td[(:u)]TJ/F87 8.97 Tf 12.29 0 Td[(-rule)]TJ/F86 8.97 Tf 17.43 0 Td[(.)]TJ -177.26 -10.41 Td[(Secondly)66(,)-354(by)-354(tagging)-353(the)-354(subsumer)-353(concept)]TJ/F70 8.97 Tf 163.18 0 Td[(D)]TJ/F86 8.97 Tf 11.03 0 Td[(during)-354(the)-353(initial)]TJ -183.43 -10.41 Td[(transformation)-248(of)-250(the)-250(subsumption)-249(problem)]TJ/F70 8.97 Tf 158.17 0 Td[(C)]TJ/F71 8.97 Tf 9.79 0 Td[(v)]TJ/F70 8.97 Tf 9.73 0 Td[(D)]TJ/F86 8.97 Tf 10.1 0 Td[(into)-250(the)-250(satisa-)]TJ -187.79 -10.41 Td[(bility)-279(problem)]TJ/F70 8.97 Tf 53.84 0 Td[(C)]TJ/F71 8.97 Tf 9.47 0 Td[(u)-251(:)]TJ/F70 8.97 Tf 14.54 0 Td[(D)]TJ/F50 5.98 Tf 7.86 3.81 Td[(y)]TJ/F86 8.97 Tf 3.93 -3.81 Td[(,)-279(where)]TJ/F50 5.98 Tf 29.16 3.81 Td[(y)]TJ/F86 8.97 Tf 6.44 -3.81 Td[(indicates)-278(the)-279(tagged)-279(concept,)-278(and)]TJ -125.24 -10.41 Td[(by)-193(consistently)-191(tagging)-192(all)-193(concepts)-191(deri)25(v)15(ed)-192(from)-193(it)-192(by)-193(applications)-191(of)]TJ 0 -10.41 Td[(tableaux)-293(rules,)-293(it)-294(is)-294(al)10(w)11(ays)-294(possible)-292(to)-294(determine)-293(whether)-292(a)-294(concept)]TJ 0 -10.41 Td[(in)-279(a)-279(particular)-277(stage)-278(of)-278(the)-279(tableaux)-277(w)10(as)-278(deri)25(v)15(ed)-278(from)-278(the)-278(subsumer)41(,)]TJ 0 -10.42 Td[(i.e.,)-250(its)-249(ne)15(gation)-244(plays)-249(the)-249(role)-249(of)-250(subsumer)-248(in)-250(the)-249(e)15(xplanation)-248(step.)]TJ 9.22 -10.41 Td[(W)80(e)-261(will)-261(assume)-260(an)-262(unlabelled)-259(\050often)-261(called)]TJ/F87 8.97 Tf 157.14 0 Td[(tr)15(ace)-261(based)]TJ/F86 8.97 Tf 44.15 0 Td[(in)-261(the)-261(DL)]TJ -210.51 -10.41 Td[(literature\051)-272(tableaux)-272(based)-273(procedure)-272(for)]TJ/F71 8.97 Tf 144.72 0 Td[(ALC)]TJ/F86 8.97 Tf 21.53 0 Td[([4],)-273(modied)-272(with)-272(the)]TJ ET endstream endobj 4 0 obj 19278 endobj 1 0 obj << /ProcSet [/PDF /Text] /Font << /F82 5 0 R /F25 6 0 R /F83 7 0 R /F43 8 0 R /F84 9 0 R /F85 10 0 R /F86 11 0 R /F71 12 0 R /F70 13 0 R /F15 14 0 R /F87 15 0 R /F88 16 0 R /F44 17 0 R /F89 18 0 R /F90 19 0 R /F49 20 0 R /F78 21 0 R /F46 22 0 R /F50 23 0 R >> >> endobj 2 0 obj << /Type /Page /Contents 3 0 R /Resources 1 0 R /MediaBox [0 0 595.27 841.89] /Parent 24 0 R >> endobj 27 0 obj << /Length 28 0 R >> stream 1 0 0 1 45.17 760.56 cm BT /F44 5.98 Tf 0 0 Td[(\050=\051)]TJ/F47 5.98 Tf 47.44 0 Td[(X)-280(;)-338(a)]TJ/F50 5.98 Tf 20.02 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(a)-202(;)-337(Y)]TJ/F44 5.98 Tf -76.09 -14.57 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(l)]TJ/F50 5.98 Tf 2.4 0 Td[(")]TJ/F44 5.98 Tf 3.82 0 Td[(\051)]TJ/F47 5.98 Tf 35.85 0 Td[(X)-280(;)-338(a)-202(;)]TJ/F50 5.98 Tf 21.48 0 Td[(:)]TJ/F47 5.98 Tf 4.98 0 Td[(a)]TJ/F50 5.98 Tf 8.07 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)-8545(X)]TJ/F50 5.98 Tf 65.92 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(a)-202(;)]TJ/F50 5.98 Tf 9.53 0 Td[(:)]TJ/F47 5.98 Tf 4.98 0 Td[(a)-202(;)-338(Y)]TJ/F44 5.98 Tf 48.55 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(r)]TJ/F50 5.98 Tf 3.66 0 Td[(")]TJ/F44 5.98 Tf 3.82 0 Td[(\051)]TJ -236.08 -14.58 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(l)]TJ/F50 5.98 Tf 2.4 0 Td[(?)]TJ/F44 5.98 Tf 5.76 0 Td[(\051)]TJ/F47 5.98 Tf 40.31 0 Td[(X)-280(;)]TJ/F50 5.98 Tf 11.94 0 Td[(?)-675(`)]TJ/F47 5.98 Tf 18.42 0 Td[(Y)-10684(X)]TJ/F50 5.98 Tf 78.72 0 Td[(`)-674(>)]TJ/F47 5.98 Tf 15.59 0 Td[(;)-338(Y)]TJ/F44 5.98 Tf 47.77 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(r)]TJ/F50 5.98 Tf 3.66 0 Td[(?)]TJ/F44 5.98 Tf 5.75 0 Td[(\051)]TJ -236.08 -14.57 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(l)]TJ/F50 5.98 Tf 2.4 0 Td[(^)]TJ/F44 5.98 Tf 4.98 0 Td[(\051)]TJ/F47 5.98 Tf 37.56 3.97 Td[(X)-280(;)-338(a)-202(;)-338(b)]TJ/F50 5.98 Tf 28.79 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ ET 47.82 -41.67 43.31 0.38 re f 1 0 0 1 48.08 -46.76 cm BT /F47 5.98 Tf 0 0 Td[(X)-280(;)-338(a)]TJ/F50 5.98 Tf 15.98 0 Td[(u)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F50 5.98 Tf 7.31 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ 39.97 7.01 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(a)-203(;)-337(Y)-3258(X)]TJ/F50 5.98 Tf 43.84 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(b)-203(;)-338(Y)]TJ ET 76.87 5.09 86.24 0.38 re f 1 0 0 1 98.6 0 cm BT /F47 5.98 Tf 0 0 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(u)]TJ/F47 5.98 Tf 4.98 0 Td[(b)-204(;)-337(Y)]TJ/F44 5.98 Tf 49.76 3.04 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(r)]TJ/F50 5.98 Tf 3.66 0 Td[(^)]TJ/F44 5.98 Tf 4.98 0 Td[(\051)]TJ -236.08 -14.58 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(l)]TJ/F50 5.98 Tf 2.4 0 Td[(:^)]TJ/F44 5.98 Tf 9.97 0 Td[(\051)]TJ/F47 5.98 Tf 6.13 3.98 Td[(X)-279(;)]TJ/F50 5.98 Tf 11.94 0 Td[(:)]TJ/F47 5.98 Tf 4.98 0 Td[(a)]TJ/F50 5.98 Tf 8.07 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)-3258(X)-280(;)]TJ/F50 5.98 Tf 35.77 0 Td[(:)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F50 5.98 Tf 7.31 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ ET -125.3 -9.48 96.2 0.38 re f 1 0 0 1 -103.97 -14.58 cm BT /F47 5.98 Tf 0 0 Td[(X)-280(;)]TJ/F50 5.98 Tf 11.95 0 Td[(:)]TJ/F44 5.98 Tf 4.98 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(u)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F44 5.98 Tf 3.28 0 Td[(\051)]TJ/F50 5.98 Tf 6.91 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ 51.09 7.02 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)-675(:)]TJ/F47 5.98 Tf 13.61 0 Td[(a)-202(;)]TJ/F50 5.98 Tf 9.53 0 Td[(:)]TJ/F47 5.98 Tf 4.98 0 Td[(b)-203(;)-338(Y)]TJ ET 98.6 5.1 53.53 0.38 re f 1 0 0 1 98.6 0 cm BT /F47 5.98 Tf 0 0 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)-675(:)]TJ/F44 5.98 Tf 13.61 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(u)]TJ/F47 5.98 Tf 4.99 0 Td[(b)]TJ/F44 5.98 Tf 3.27 0 Td[(\051)]TJ/F47 5.98 Tf 4.09 0 Td[(;)-337(Y)]TJ/F44 5.98 Tf 34.92 3.04 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(r)]TJ/F50 5.98 Tf 3.66 0 Td[(:^)]TJ/F44 5.98 Tf 9.96 0 Td[(\051)]TJ -236.08 -14.74 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(l)]TJ/F50 5.98 Tf 2.4 0 Td[(_)]TJ/F44 5.98 Tf 4.98 0 Td[(\051)]TJ/F47 5.98 Tf 16.1 3.98 Td[(X)-279(;)-338(a)]TJ/F50 5.98 Tf 20.01 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)-3258(X)-280(;)-337(b)]TJ/F50 5.98 Tf 43.08 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ ET -114.95 -9.64 86.24 0.38 re f 1 0 0 1 -93.23 -14.74 cm BT /F47 5.98 Tf 0 0 Td[(X)-280(;)-338(a)]TJ/F50 5.98 Tf 15.98 0 Td[(t)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F50 5.98 Tf 7.31 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ 61.44 7.02 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(a)-202(;)-338(b)-203(;)-338(Y)]TJ ET 98.34 5.1 43.31 0.38 re f 1 0 0 1 98.6 0 cm BT /F47 5.98 Tf 0 0 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(t)]TJ/F47 5.98 Tf 4.98 0 Td[(b)-204(;)-337(Y)]TJ/F44 5.98 Tf 49.76 3.04 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(r)]TJ/F50 5.98 Tf 3.66 0 Td[(_)]TJ/F44 5.98 Tf 4.98 0 Td[(\051)]TJ -236.08 -14.57 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(l)]TJ/F50 5.98 Tf 2.4 0 Td[(:_)]TJ/F44 5.98 Tf 9.97 0 Td[(\051)]TJ/F47 5.98 Tf 27.59 3.97 Td[(X)-280(;)]TJ/F50 5.98 Tf 11.95 0 Td[(:)]TJ/F47 5.98 Tf 4.98 0 Td[(a)-202(;)]TJ/F50 5.98 Tf 9.53 0 Td[(:)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F50 5.98 Tf 7.31 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ ET -103.97 -9.48 53.53 0.38 re f 1 0 0 1 -103.97 -14.57 cm BT /F47 5.98 Tf 0 0 Td[(X)-280(;)]TJ/F50 5.98 Tf 11.95 0 Td[(:)]TJ/F44 5.98 Tf 4.98 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(t)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F44 5.98 Tf 3.28 0 Td[(\051)]TJ/F50 5.98 Tf 6.91 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ 29.62 7.01 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)-675(:)]TJ/F47 5.98 Tf 13.61 0 Td[(a)-203(;)-337(Y)-3258(X)]TJ/F50 5.98 Tf 43.84 0 Td[(`)-675(:)]TJ/F47 5.98 Tf 13.61 0 Td[(b)-203(;)-338(Y)]TJ ET 77.26 5.09 96.2 0.38 re f 1 0 0 1 98.6 0 cm BT /F47 5.98 Tf 0 0 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)-675(:)]TJ/F44 5.98 Tf 13.61 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(t)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F44 5.98 Tf 3.28 0 Td[(\051)]TJ/F47 5.98 Tf 4.09 0 Td[(;)-337(Y)]TJ/F44 5.98 Tf 34.92 3.04 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(r)]TJ/F50 5.98 Tf 3.66 0 Td[(:_)]TJ/F44 5.98 Tf 9.96 0 Td[(\051)]TJ -236.08 -14.74 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(l)]TJ/F50 5.98 Tf 2.4 0 Td[(::)]TJ/F44 5.98 Tf 9.97 0 Td[(\051)]TJ/F47 5.98 Tf 36.96 3.97 Td[(X)-280(;)-338(a)]TJ/F50 5.98 Tf 20.01 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ ET -94.08 -9.65 44.5 0.38 re f 1 0 0 1 -94.08 -14.74 cm BT /F47 5.98 Tf 0 0 Td[(X)-279(;)]TJ/F50 5.98 Tf 11.94 0 Td[(::)]TJ/F47 5.98 Tf 9.97 0 Td[(a)]TJ/F50 5.98 Tf 8.07 0 Td[(`)]TJ/F47 5.98 Tf 8.62 0 Td[(Y)]TJ 64.98 7.01 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(a)-201(;)-338(Y)]TJ ET 98.59 5.09 44.5 0.38 re f 1 0 0 1 98.59 0 cm BT /F47 5.98 Tf 0 0 Td[(X)]TJ/F50 5.98 Tf 10.49 0 Td[(`)-674(::)]TJ/F47 5.98 Tf 18.59 0 Td[(a)-202(;)-337(Y)]TJ/F44 5.98 Tf 44.68 3.04 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(r)]TJ/F50 5.98 Tf 3.66 0 Td[(::)]TJ/F44 5.98 Tf 9.96 0 Td[(\051)]TJ -236.08 -14.58 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(l)]TJ/F56 5.98 Tf 2.4 0 Td[(3)]TJ/F44 5.98 Tf 5.18 0 Td[(\051)]TJ/F47 5.98 Tf 39.44 3.98 Td[(X)]TJ/F12 4.98 Tf 6.44 2.51 Td[(0)]TJ/F47 5.98 Tf 3.91 -2.51 Td[(;)-338(b)]TJ/F50 5.98 Tf 11.59 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ/F12 4.98 Tf 5.89 2.51 Td[(0)]TJ ET -98.1 -9.48 43.52 0.38 re f 1 0 0 1 -98.1 -14.58 cm BT /F47 5.98 Tf 0 0 Td[(X)-279(;)]TJ/F50 5.98 Tf 11.94 0 Td[(9)]TJ/F47 5.98 Tf 4.21 0 Td[(r)33(:b)]TJ/F50 5.98 Tf 12.85 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ 63.14 7.02 Td[(X)]TJ/F12 4.98 Tf 6.45 2.51 Td[(0)]TJ/F50 5.98 Tf 6.73 -2.51 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(b)-202(;)-338(Y)]TJ/F12 4.98 Tf 14.66 2.51 Td[(0)]TJ ET 98.59 5.1 43.52 0.38 re f 1 0 0 1 98.59 0 cm BT /F47 5.98 Tf 0 0 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)-676(8)]TJ/F47 5.98 Tf 12.84 0 Td[(r)33(:b)-203(;)-338(Y)]TJ/F44 5.98 Tf 54.89 3.04 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(r)]TJ/F56 5.98 Tf 3.66 0 Td[(2)]TJ/F44 5.98 Tf 5.02 0 Td[(\051)]TJ -236.08 -14.57 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(l)]TJ/F50 5.98 Tf 2.4 0 Td[(:)]TJ/F56 5.98 Tf 4.98 0 Td[(2)]TJ/F44 5.98 Tf 5.02 0 Td[(\051)]TJ/F47 5.98 Tf 32.12 3.97 Td[(X)]TJ/F12 4.98 Tf 6.45 2.51 Td[(0)]TJ/F47 5.98 Tf 3.91 -2.51 Td[(;)]TJ/F50 5.98 Tf 4.28 0 Td[(:)]TJ/F47 5.98 Tf 4.99 0 Td[(b)]TJ/F50 5.98 Tf 7.3 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ/F12 4.98 Tf 5.9 2.51 Td[(0)]TJ ET -101.08 -9.48 48.5 0.38 re f 1 0 0 1 -101.08 -14.57 cm BT /F47 5.98 Tf 0 0 Td[(X)-279(;)]TJ/F50 5.98 Tf 11.94 0 Td[(:8)]TJ/F47 5.98 Tf 9.19 0 Td[(r)33(:b)]TJ/F50 5.98 Tf 12.85 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ 58.16 7.01 Td[(X)]TJ/F12 4.98 Tf 6.45 2.51 Td[(0)]TJ/F50 5.98 Tf 6.73 -2.51 Td[(`)-674(:)]TJ/F47 5.98 Tf 13.61 0 Td[(b)-202(;)-338(Y)]TJ/F12 4.98 Tf 14.66 2.51 Td[(0)]TJ ET 98.59 5.09 48.5 0.38 re f 1 0 0 1 98.59 0 cm BT /F47 5.98 Tf 0 0 Td[(X)]TJ/F50 5.98 Tf 10.48 0 Td[(`)-675(:9)]TJ/F47 5.98 Tf 17.82 0 Td[(r)33(:b)-204(;)-337(Y)]TJ/F44 5.98 Tf 47.27 3.04 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(r)]TJ/F50 5.98 Tf 3.65 0 Td[(:)]TJ/F56 5.98 Tf 4.99 0 Td[(3)]TJ/F44 5.98 Tf 5.17 0 Td[(\051)]TJ/F94 7.97 Tf -209.88 -14.58 Td[(wher)36(e)]TJ/F46 7.97 Tf 25.17 0 Td[(X)]TJ/F50 5.98 Tf 7.58 2.82 Td[(0)]TJ/F89 7.97 Tf 4.48 -2.82 Td[(=)]TJ/F49 7.97 Tf 6.29 0 Td[(f)]TJ/F46 7.97 Tf 4.23 0 Td[(a)]TJ/F49 7.97 Tf 6.85 0 Td[(j)-296(8)]TJ/F46 7.97 Tf 9.41 0 Td[(r)29(:a)]TJ/F49 7.97 Tf 12.79 0 Td[(2)]TJ/F46 7.97 Tf 8 0 Td[(X)]TJ/F49 7.97 Tf 7.59 0 Td[(g)-236([)-236(f:)]TJ/F46 7.97 Tf 23.52 0 Td[(a)]TJ/F49 7.97 Tf 6.85 0 Td[(j)-295(:9)]TJ/F46 7.97 Tf 15.05 0 Td[(r)29(:a)]TJ/F49 7.97 Tf 12.79 0 Td[(2)]TJ/F46 7.97 Tf 8 0 Td[(X)]TJ/F49 7.97 Tf 7.59 0 Td[(g)]TJ/F89 7.97 Tf 4.23 0 Td[(,)]TJ/F94 7.97 Tf 3.99 0 Td[(and)]TJ/F46 7.97 Tf -148.45 -8.57 Td[(Y)]TJ/F50 5.98 Tf 6.79 2.81 Td[(0)]TJ/F89 7.97 Tf 4.48 -2.81 Td[(=)]TJ/F49 7.97 Tf 6.29 0 Td[(f)]TJ/F46 7.97 Tf 4.23 0 Td[(a)]TJ/F49 7.97 Tf 6.85 0 Td[(j)-296(9)]TJ/F46 7.97 Tf 9.41 0 Td[(r)29(:a)]TJ/F49 7.97 Tf 12.79 0 Td[(2)]TJ/F46 7.97 Tf 8 0 Td[(Y)]TJ/F49 7.97 Tf 6.79 0 Td[(g)-236([)-237(f:)]TJ/F46 7.97 Tf 23.52 0 Td[(a)]TJ/F49 7.97 Tf 6.85 0 Td[(j)-296(:8)]TJ/F46 7.97 Tf 15.06 0 Td[(r)29(:a)]TJ/F49 7.97 Tf 12.79 0 Td[(2)]TJ/F46 7.97 Tf 7.99 0 Td[(Y)]TJ/F49 7.97 Tf 6.79 0 Td[(g)]TJ/F95 7.97 Tf -117.08 -16.07 Td[(Figur)18(e)-250(1.)]TJ/F89 7.97 Tf 38.37 0 Td[(Rules)-250(for)]TJ/F49 7.97 Tf 31.44 0 Td[(ALC)]TJ/F86 8.97 Tf -146.58 -23.06 Td[(addition)-325(of)-325(lazy)-326(unfolding)-324(and)-325(tagging.)-325(As)-325(a)-326(notation)-325(for)-325(the)-325(proof)]TJ 0 -10.41 Td[(generated)-323(by)-325(the)-324(modied)-323(tableaux)-324(procedure,)-323(we)-324(introduce)-324(here)-324(a)]TJ 0 -10.41 Td[(simple)-346(sequent)-346(calculus.)-346(Sequent)-346(calculi)-346(for)]TJ/F71 8.97 Tf 164.87 0 Td[(ALC)]TJ/F86 8.97 Tf 22.19 0 Td[(can)-347(be)-347(obtained)]TJ -187.06 -10.41 Td[(from)-261(the)-261(modal)-260(logic)-261(literature)-260([3])-260(by)-261(e)15(xploiting)-260(the)-261(correspondence)]TJ 0 -10.41 Td[(between)]TJ/F71 8.97 Tf 32.86 0 Td[(ALC)]TJ/F86 8.97 Tf 22.06 0 Td[(and)-332(the)-331(multi-modal)-331(propositional)-330(logic)]TJ/F70 8.97 Tf 148.4 0 Td[(K)]TJ/F44 5.98 Tf 7.81 -1.39 Td[(\050)]TJ/F47 5.98 Tf 2.87 0 Td[(m)]TJ/F44 5.98 Tf 6.54 0 Td[(\051)]TJ/F86 8.97 Tf 3.38 1.39 Td[(,)-332(with)]TJ -223.92 -10.41 Td[(the)-253(subsumption)-251(relation)-252(being)-253(encoded)-252(as)-252(the)-253(entailment)-252(relation)-252(in)]TJ 0 -10.41 Td[(a)-297(sequent.)-295(Note)-296(that)-296(there)-296(ha)21(v)15(e)-297(already)-295(been)-296(attempts)-295(\050e.g.,)-296([13]\051)-296(to)]TJ 0 -10.41 Td[(produce)-338(sequent)-338(calculi)-339(for)-339(DLs)-338(based)-339(on)-339(such)-339(calculi)-338(from)-338(predi-)]TJ 0 -10.41 Td[(cate)-291(logic.)-291(Ho)26(we)25(v)15(er)41(,)-292(the)-291(result)-291(does)-290(not)-291(bear)-291(a)-292(direct)-290(relation)-291(to)-291(our)]TJ 0 -10.41 Td[(tableaux)-397(proof)-397(system,)-397(nor)-398(has)-397(it)-398(been)-398(used)-397(to)-398(generate)-397(short)-397(e)15(x-)]TJ 0 -10.42 Td[(planations.)-375(In)-376(order)-375(to)-376(de)25(vise)-376(the)-376(sequent)-375(notation,)-375(we)-376(e)15(xploit)-375(the)]TJ 0 -10.41 Td[(well)-336(kno)26(wn)-336(f)11(act)-336(that)-335(in)-336(classical)-335(logic)-335(it)-336(is)-336(possible)-334(to)-336(obtain)-335(a)-336(se-)]TJ 0 -10.41 Td[(quent)-211(proof)-212(directly)-210(from)-212(a)-212(standard)-210(tableaux)-211(satisability)-210(algorithm,)]TJ 0 -10.41 Td[(where)-250(applications)-248(of)-250(tableaux)-249(rules)-250(correspond)-249(with)-249(steps)-250(in)-250(the)-250(se-)]TJ 0 -10.41 Td[(quent)-378(proof,)-378(and)-378(clash)-379(detections)-377(correspond)-377(with)-378(termination)-377(ax-)]TJ 0 -10.41 Td[(ioms)-249(\050e.g.,)-249([12]\051.)]TJ 9.22 -10.41 Td[(The)-310(calculus)-309(is)-310(sho)26(wn)-310(in)-310(Figure)-310(1.)-310(Please)-309(note)-310(that)-310(the)-310(proposed)]TJ -9.22 -10.41 Td[(system)-208(is)-208(not)-208(strictly)-207(original)-207(\050see,)-208(e.g.,)-208([2]\051;)-207(what)-208(is)-208(important)-207(here)-208(is)]TJ 0 -10.41 Td[(the)-259(w)10(ay)-258(a)-259(sequent)-258(proof)-259(can)-258(be)-259(correlated)-258(with)-258(a)-259(tableaux)-258(procedure)]TJ 0 -10.41 Td[(for)]TJ/F71 8.97 Tf 12.8 0 Td[(ALC)]TJ/F86 8.97 Tf 19.07 0 Td[(,)-261(since)-260(all)-261(the)-260(implemented)-259(systems)-259(for)-261(e)15(xpressi)27(v)15(e)-261(Descrip-)]TJ -31.87 -10.41 Td[(tion)-251(Logics)-250(mak)10(e)-251(use)-251(of)-251(tableaux)-250(procedures.)-249(In)-251(order)-251(to)-251(parallel)-250(the)]TJ 0 -10.42 Td[(beha)21(viour)-298(introduced)-297(by)-299(lazy)-298(unfolding)-297(and)-298(tagging)-298(in)-299(the)-298(tableaux)]TJ 0 -10.41 Td[(calculus,)-372(weak)11(ening)-373(and)-373(ne)16(gation)-368(rules)-373(do)-373(not)-373(e)15(xist.)-372(If)-374(a)-373(ne)15(gation)]TJ 0 -10.41 Td[(rule)-343(is)-342(used)-343(in)-343(an)-342(e)15(xplanation)-341(of)-343(subsumption,)-341(this)-343(w)11(ould)-343(result)-342(in)]TJ 0 -10.41 Td[(shifts)-259(of)-258(subsumers)-258(to)-259(subsumees)-257(and)-259(vice)-258(v)15(ersa.)-259(On)-258(the)-259(other)-258(hand,)]TJ 0 -10.41 Td[(ne)25(w)-278(rules)-278(are)-278(introduced)-277(which)-278(e)15(xplicitly)-277(consider)-278(ne)16(gation)-273(in)-278(front)]TJ 0 -10.41 Td[(of)-340(e)25(v)16(ery)-340(construct.)-338(In)-339(order)-339(to)-340(parallel)-338(the)-340(beha)21(viour)-339(of)-339(the)]TJ/F71 8.97 Tf 220.98 0 Td[(8)]TJ/F86 8.97 Tf 5.12 0 Td[(-)-340(and)]TJ/F71 8.97 Tf -226.1 -10.41 Td[(9)]TJ/F87 8.97 Tf 5.12 0 Td[(-rules)]TJ/F86 8.97 Tf 24.37 0 Td[(in)-384(the)-383(tableaux)-383(calculus,)-383(the)-384(applicability)-382(condition)-382(of)-384(the)]TJ/F73 8.97 Tf -29.49 -10.41 Td[(2)]TJ/F86 8.97 Tf 6.76 0 Td[(-)-238(and)]TJ/F73 8.97 Tf 20.21 0 Td[(3)]TJ/F87 8.97 Tf 7.13 0 Td[(-rules)]TJ/F86 8.97 Tf 23.05 0 Td[(is)-239(e)15(xplicitly)-237(considered.)-236(The)-238(condition)-237(states)-238(that)-238(the)]TJ -57.15 -10.41 Td[(rule)-257(is)-258(applicable)-256(if)-257(all)-258(the)-257(homologous)-256(uni)26(v)15(ersal)-257(and)-257(e)15(xistential)-256(for)20(-)]TJ 0 -10.41 Td[(mul)-282(are)-283(gathered)-277(together)-281(on)-283(the)-283(left)-282(and)-283(right)-282(hand)-283(sides)-282(of)-283(the)]TJ 0 -10.41 Td[(sequent)-350(in)-351(the)-351(precondition;)-349(the)-350(rule)-351(is)-351(then)-350(applied)-350(only)-351(once.)-350(Of)]TJ 0 -10.42 Td[(course,)-249(additional)-248(termination)-248(axioms)-249(are)-249(also)-249(gi)25(v)15(en.)]TJ 9.22 -10.41 Td[(W)81(e)-322(will)-320(no)25(w)-321(see)-321(ho)26(w)-322(the)-320(tableaux)-320(algorithm)-320(w)10(ould)-321(demonstrate)]TJ -9.22 -10.41 Td[(the)-250(abo)16(v)15(e-mentioned)-248(subsumption)-247(\0501\051.)]TJ 9.22 -10.41 Td[(W)81(e)-344(w)10(ant)-344(to)-344(parallel)-343(the)-343(steps)-344(in)-344(the)-343(tableaux)-343(algorithm)-343(with)-343(the)]TJ -9.22 -10.41 Td[(corresponding)-318(sequent)-318(steps)-320(for)-319(the)-319(same)-319(proof)-319(\050Figure)-319(2\051.)-320(The)-319(se-)]TJ 0 -10.41 Td[(quent)-328(notation)-327(will)-329(be)-328(used)-328(in)-328(the)-329(ne)16(xt)-329(section)-327(to)-329(de)26(vise)-328(the)-328(e)15(xpla-)]TJ 0 -10.41 Td[(nation.)-321(The)-322(proof)-321(starts)-321(by)-322(pro)16(ving)-322(the)-321(unsatisability)-320(of)-322(the)-321(set)-322(of)]TJ 0 -10.41 Td[(concepts)]TJ/F71 8.97 Tf 0 -18.25 Td[(f)]TJ/F15 8.97 Tf 4.61 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.25 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(>)-228(u)-228(8)]TJ/F78 8.97 Tf 22.52 0 Td[(friend)]TJ/F70 8.97 Tf 28.25 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050\050)]TJ/F71 8.97 Tf 7.17 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F71 8.97 Tf 5.63 0 Td[(t)]TJ/F15 8.97 Tf 8.19 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.25 0 Td[(\051\051\051)]TJ/F70 8.97 Tf 10.75 0 Td[(;)]TJ/F71 8.97 Tf -250.53 -11.54 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.87 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051\051\051)]TJ/F50 5.98 Tf 10.75 4.26 Td[(y)]TJ/F71 8.97 Tf 3.93 -4.26 Td[(g)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F86 8.97 Tf -174.09 -18.28 Td[(An)-239(application)-238(of)-239(the)-239(tableaux)]TJ/F71 8.97 Tf 110.35 0 Td[(u)]TJ/F87 8.97 Tf 6.14 0 Td[(-rule)]TJ/F86 8.97 Tf 19.58 0 Td[(to)-239(the)-239(rst)-239(concept)-238(leads)-238(to)-239(the)]TJ -136.07 -10.41 Td[(set)]TJ/F71 8.97 Tf 263.01 661.2 Td[(f9)]TJ/F78 8.97 Tf 9.73 0 Td[(friend)]TJ/F70 8.97 Tf 28.25 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(>)]TJ/F70 8.97 Tf 7.16 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F15 8.97 Tf 6.15 0 Td[(\050\050)]TJ/F71 8.97 Tf 7.16 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051)]TJ/F71 8.97 Tf 5.63 0 Td[(t)]TJ/F15 8.97 Tf 8.19 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051)]TJ/F70 8.97 Tf 7.17 0 Td[(;)]TJ/F71 8.97 Tf -237.22 -11.54 Td[(:)]TJ/F15 8.97 Tf 6.15 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.87 0 Td[(t)]TJ/F78 8.97 Tf 8.2 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051\051)]TJ/F50 5.98 Tf 10.75 4.27 Td[(y)]TJ/F71 8.97 Tf 3.93 -4.27 Td[(g)]TJ/F70 8.97 Tf 4.61 0 Td[(:)]TJ/F86 8.97 Tf -174.09 -13.88 Td[(Because)-237(the)-237(concept)-236(triggering)-236(the)-237(tableaux)-236(rule)-237(w)10(as)-237(not)-237(tagged,)-236(this)]TJ 0 -10.41 Td[(corresponds)-235(to)-237(a)-236(sequent)-236(step)-236(using)-236(the)-236(\050)]TJ/F70 8.97 Tf 144.36 0 Td[(l)]TJ/F71 8.97 Tf 2.9 0 Td[(^)]TJ/F86 8.97 Tf 6.14 0 Td[(\051)-237(rule)-236(\050step)-236(2)-237(in)-236(Figure)-236(2\051.)]TJ -153.4 -10.41 Td[(The)-250(tableaux)-248(algorithm)-249(w)11(ould)-249(then)-250(normalise)]TJ/F71 8.97 Tf 44.53 -14.07 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.87 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051\051\051)]TJ/F50 5.98 Tf 10.75 4.31 Td[(y)]TJ/F86 8.97 Tf -196.63 -19.61 Td[(to)-372(gi)26(v)15(e)]TJ/F71 8.97 Tf 28.72 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.25 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(:8)]TJ/F78 8.97 Tf 11.26 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051\051)]TJ/F50 5.98 Tf 7.16 4.26 Td[(y)]TJ/F86 8.97 Tf 3.93 -4.26 Td[(,)-372(and)-371(apply)-370(the)]TJ/F71 8.97 Tf 59.4 0 Td[(9)]TJ/F87 8.97 Tf 5.12 0 Td[(-)]TJ -242.1 -10.41 Td[(rule)]TJ/F86 8.97 Tf 16.69 0 Td[(to)]TJ/F71 8.97 Tf 9.22 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(>)]TJ/F86 8.97 Tf 7.17 0 Td[(,)-250(generating)-248(the)-249(sub-problem)-248(consisting)-248(of)]TJ/F71 8.97 Tf -39.64 -13.88 Td[(f>)]TJ/F70 8.97 Tf 11.78 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050\050)]TJ/F71 8.97 Tf 7.17 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F71 8.97 Tf 5.63 0 Td[(t)]TJ/F15 8.97 Tf 8.19 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.25 0 Td[(\051\051)]TJ/F70 8.97 Tf 7.16 0 Td[(;)]TJ/F71 8.97 Tf -165.37 -11.08 Td[(:8)]TJ/F78 8.97 Tf 11.27 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.87 0 Td[(t)]TJ/F78 8.97 Tf 8.2 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F50 5.98 Tf 3.58 3.81 Td[(y)]TJ/F71 8.97 Tf 3.93 -3.81 Td[(g)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F86 8.97 Tf -153.19 -16.18 Td[(where)]TJ/F71 8.97 Tf 26.03 0 Td[(:8)]TJ/F78 8.97 Tf 11.26 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051)]TJ/F50 5.98 Tf 3.58 4.26 Td[(y)]TJ/F86 8.97 Tf 8.05 -4.26 Td[(is)-460(tagged)-458(because)-458(it)-460(w)11(as)-460(de-)]TJ -135.92 -10.42 Td[(ri)25(v)15(ed)-247(from)-246(a)-247(tagged)-247(concept.)-245(Because)-246(the)-247(triggering)-246(concept)-246(w)11(as)-247(not)]TJ 0 -10.41 Td[(tagged,)-256(this)-256(corresponds)-255(to)-256(a)-256(sequent)-256(step)-255(using)-256(the)-256(\050)]TJ/F70 8.97 Tf 189.31 0 Td[(l)]TJ/F73 8.97 Tf 2.9 0 Td[(3)]TJ/F86 8.97 Tf 7.13 0 Td[(\051)-256(rule)-256(\050step)-256(3)]TJ -199.34 -10.41 Td[(in)-250(Figure)-249(2\051.)]TJ 9.22 -10.41 Td[(The)-662(ne)15(xt)-662(step)-663(in)-662(the)-663(tableaux)-661(algorithm)-661(w)10(ould)-662(be)-663(a)-663(nor)21(-)]TJ -9.22 -10.41 Td[(malisation)-424(of)]TJ/F71 8.97 Tf 52.46 0 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050\050)]TJ/F71 8.97 Tf 7.17 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F71 8.97 Tf 5.63 0 Td[(t)]TJ/F15 8.97 Tf 8.19 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.25 0 Td[(\051\051)]TJ/F86 8.97 Tf 10.98 0 Td[(to)-424(gi)25(v)15(e)]TJ/F71 8.97 Tf -219.22 -10.41 Td[(:)]TJ/F15 8.97 Tf 6.15 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F71 8.97 Tf 5.64 0 Td[(u)-228(:)]TJ/F15 8.97 Tf 14.33 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.11 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F86 8.97 Tf 3.59 0 Td[(,)-304(follo)26(wed)-304(by)-303(an)-304(appli-)]TJ -161.93 -10.41 Td[(cation)-249(of)-250(the)]TJ/F71 8.97 Tf 47.07 0 Td[(u)]TJ/F87 8.97 Tf 6.14 0 Td[(-rule)]TJ/F86 8.97 Tf 17.43 0 Td[(,)-250(leading)-249(to)-249(the)-250(set)]TJ/F71 8.97 Tf -37.69 -13.88 Td[(f>)]TJ/F70 8.97 Tf 11.77 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F70 8.97 Tf 3.58 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.25 0 Td[(\051)]TJ/F70 8.97 Tf 3.58 0 Td[(;)]TJ/F71 8.97 Tf -158.2 -11.08 Td[(:8)]TJ/F78 8.97 Tf 11.26 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F50 5.98 Tf 3.59 3.81 Td[(y)]TJ/F71 8.97 Tf 3.93 -3.81 Td[(g)]TJ/F70 8.97 Tf 4.6 0 Td[(:)]TJ/F86 8.97 Tf -156.77 -13.89 Td[(Because)-492(the)-493(triggering)-492(concept)-492(w)10(as)-493(not)-492(tagged,)-492(these)-493(tw)11(o)-494(steps)]TJ 0 -10.41 Td[(correspond)-587(to)-588(a)-589(sequent)-587(step)-588(using)-588(the)-588(\050)]TJ/F70 8.97 Tf 162.96 0 Td[(l)]TJ/F71 8.97 Tf 2.9 0 Td[(:_)]TJ/F86 8.97 Tf 12.29 0 Td[(\051)-588(rule)-588(\050step)-588(4)-588(in)]TJ -178.15 -10.41 Td[(Figure)-491(2\051.)-492(The)-491(tableaux)-491(algorithm)-490(w)10(ould)-491(then)-491(normalise)-491(all)-491(the)]TJ 0 -10.41 Td[(ne)15(gated)-206(concepts)-211(to)-211(gi)25(v)15(e)]TJ/F71 8.97 Tf 88.74 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(::)]TJ/F78 8.97 Tf 12.29 0 Td[(Doctor)]TJ/F86 8.97 Tf 28.24 0 Td[(,)]TJ/F71 8.97 Tf 4.14 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Lawyer)]TJ/F86 8.97 Tf 30.15 0 Td[(and)]TJ/F71 8.97 Tf -232.14 -10.41 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.87 0 Td[(t)]TJ/F78 8.97 Tf 8.2 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F50 5.98 Tf 3.58 4.26 Td[(y)]TJ/F86 8.97 Tf 5.93 -4.26 Td[(respecti)27(v)15(ely)65(.)-222(The)]TJ/F71 8.97 Tf 62.55 0 Td[(9)]TJ/F87 8.97 Tf 5.12 0 Td[(-rule)]TJ/F86 8.97 Tf 19.43 0 Td[(w)11(ould)-222(then)-221(be)]TJ -194.87 -10.41 Td[(applied)-249(to)-250(the)-249(last)-249(of)-250(these)-249(concepts,)-248(generating)]TJ/F71 8.97 Tf 37.83 -14.06 Td[(f::)]TJ/F78 8.97 Tf 16.89 0 Td[(Doctor)]TJ/F70 8.97 Tf 28.24 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Lawyer)]TJ/F70 8.97 Tf 28.25 0 Td[(;)]TJ/F71 8.97 Tf 4.09 0 Td[(:)]TJ/F15 8.97 Tf 6.15 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F50 5.98 Tf 3.59 3.81 Td[(y)]TJ/F71 8.97 Tf 3.93 -3.81 Td[(g)]TJ/F70 8.97 Tf 4.6 0 Td[(:)]TJ/F86 8.97 Tf -204.7 -14.07 Td[(Because)-423(the)-423(triggering)-423(concept)-422(w)10(as)-424(tagged,)-422(this)-423(e)15(xpansion)-423(corre-)]TJ 0 -10.41 Td[(sponds)-280(to)-280(one)-280(of)-280(the)-280(sequent)-280(right)-280(rules,)-279(and)-280(the)-280(preceding)-279(normali-)]TJ 0 -10.41 Td[(sation)-225(step)-224(means)-224(that)-224(it)-225(corresponds)-223(to)-225(a)-225(sequent)-224(step)-224(using)-224(the)-225(\050)]TJ/F70 8.97 Tf 230.93 0 Td[(r)]TJ/F73 8.97 Tf 4.41 0 Td[(2)]TJ/F86 8.97 Tf 6.76 0 Td[(\051)]TJ -242.1 -10.41 Td[(rule)-250(\050step)-249(5)-250(in)-249(Figure)-249(2\051.)]TJ 9.22 -10.41 Td[(The)-296(tableaux)-295(algorithm)-295(w)10(ould)-296(then)-296(proceed)-296(with)-296(a)-296(normalisation)]TJ -9.22 -10.41 Td[(of)]TJ/F71 8.97 Tf 10 0 Td[(::)]TJ/F78 8.97 Tf 12.29 0 Td[(Doctor)]TJ/F86 8.97 Tf 28.24 0 Td[(,)-282(corresponding)-279(to)-281(a)-282(sequent)-280(step)-281(using)-281(the)-281(\050)]TJ/F70 8.97 Tf 159.91 0 Td[(l)]TJ/F71 8.97 Tf 2.9 0 Td[(::)]TJ/F86 8.97 Tf 12.29 0 Td[(\051)-281(rule)]TJ -225.63 -10.41 Td[(\050step)-218(6)-219(in)-218(Figure)-218(2\051,)-218(and)-218(a)-219(normalisation)-216(of)]TJ/F71 8.97 Tf 153.38 0 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F50 5.98 Tf 3.58 4.26 Td[(y)]TJ/F86 8.97 Tf 3.93 -4.26 Td[(,)-219(fol-)]TJ -227.93 -10.41 Td[(lo)25(wed)-249(by)-250(an)-249(application)-248(of)-250(the)]TJ/F71 8.97 Tf 110.85 0 Td[(u)]TJ/F87 8.97 Tf 6.14 0 Td[(-rule)]TJ/F86 8.97 Tf 19.67 0 Td[(to)-250(gi)26(v)15(e)]TJ/F71 8.97 Tf -91.07 -14.06 Td[(f)]TJ/F78 8.97 Tf 4.61 0 Td[(Doctor)]TJ/F70 8.97 Tf 28.24 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Lawyer)]TJ/F70 8.97 Tf 28.24 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Rich)]TJ/F50 5.98 Tf 18.83 3.8 Td[(y)]TJ/F70 8.97 Tf 3.93 -3.8 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Doctor)]TJ/F50 5.98 Tf 28.24 3.8 Td[(y)]TJ/F71 8.97 Tf 3.93 -3.8 Td[(g)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F86 8.97 Tf -196.94 -14.07 Td[(where)]TJ/F71 8.97 Tf 23.97 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Rich)]TJ/F86 8.97 Tf 20.89 0 Td[(and)]TJ/F71 8.97 Tf 15.01 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Doctor)]TJ/F86 8.97 Tf 30.31 0 Td[(are)-229(both)-230(tagged.)-229(The)-229(combination)-228(of)-230(the)]TJ -102.47 -10.41 Td[(triggering)-258(tagged)-259(concept)-258(and)-259(the)-259(normalisation)-257(step)-259(means)-258(that)-259(this)]TJ 0 -10.41 Td[(last)-250(e)15(xpansion)-248(corresponds)-248(to)-250(the)-249(\050)]TJ/F70 8.97 Tf 124.13 0 Td[(r)]TJ/F71 8.97 Tf 4.42 0 Td[(_)]TJ/F86 8.97 Tf 6.14 0 Td[(\051)-250(sequent)-248(rule.)]TJ -125.47 -10.41 Td[(Finally)66(,)-231(the)-232(tableau)-230(algorithm)-230(detects)-231(a)-231(clash)-231(between)]TJ/F78 8.97 Tf 192.6 0 Td[(Doctor)]TJ/F86 8.97 Tf 30.32 0 Td[(and)]TJ/F71 8.97 Tf -232.14 -10.41 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F50 5.98 Tf 28.24 3.81 Td[(y)]TJ/F86 8.97 Tf 3.93 -3.81 Td[(.)-242(Because)]TJ/F71 8.97 Tf 36.46 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Doctor)]TJ/F50 5.98 Tf 28.25 3.81 Td[(y)]TJ/F86 8.97 Tf 6.1 -3.81 Td[(is)-241(tagged,)-241(this)-241(corresponds)-240(to)-242(the)-242(se-)]TJ -115.27 -10.41 Td[(quent)-275(termination)-274(axiom)]TJ/F78 8.97 Tf 91.11 0 Td[(X)]TJ/F70 8.97 Tf 5.91 0 Td[(;)]TJ/F78 8.97 Tf 6.12 0 Td[(Doctor)]TJ/F71 8.97 Tf 35.28 0 Td[(`)]TJ/F78 8.97 Tf 12.66 0 Td[(Doctor)]TJ/F70 8.97 Tf 29.46 0 Td[(;)]TJ/F78 8.97 Tf 6.11 0 Td[(Y)]TJ/F86 8.97 Tf 7.18 0 Td[(\050step)-275(7)-275(in)-276(Fig-)]TJ -193.83 -10.41 Td[(ure)-250(2\051.)]TJ/F83 10.91 Tf 0 -26 Td[(3)-1000(The)-250(surface)-250(structur)19(e)-250(of)-250(explanations)]TJ/F86 8.97 Tf 0 -15.89 Td[(The)-306(sequent)-305(calculus)-305(proofs)-306(obtained)-305(from)-305(the)-306(theorem)-305(pro)15(v)16(er)-306(pro-)]TJ 0 -10.41 Td[(vide)-243(the)-244(frame)26(w)11(ork)-243(for)-244(an)-243(e)15(xplaination,)-241(b)20(ut)-244(there)-242(are)-244(some)-242(problems)]TJ 0 -10.41 Td[(with)-241(these)-241(proofs)-240(that)-241(w)10(ould)-241(limit)-240(their)-241(usefulness)-240(as)-241(e)15(xplanations)-239(to)]TJ 0 -10.41 Td[(be)-250(gi)25(v)15(en)-249(to)-250(end-users.)]TJ 9.22 -10.41 Td[(One)-305(problem)-305(relates)-305(to)-305(the)-306(contents)-304(of)-306(the)-305(proof)-305(tree)-306(itself:)-305(there)]TJ -9.22 -10.41 Td[(can)-344(be)-344(se)26(v)15(eral)-343(fragments)-343(of)-343(proofs)-343(which)-343(are)-344(irrele)26(v)25(ant)-343(and)-344(w)11(ould)]TJ 0 -10.41 Td[(only)-190(clutter)-190(the)-190(e)15(xlanation.)-189(These)-189(can)-190(occur)-190(because)-189(of)-190(manipulations)]TJ 0 -10.42 Td[(applied)-244(to)-244(concept)-243(fragments)-243(that)-244(end)-244(up)-244(being)-244(irrele)26(v)25(ant.)-244(F)15(or)-244(e)15(xam-)]TJ 0 -10.41 Td[(ple,)-207(in)-208(sho)26(wing)-207(that)]TJ/F71 8.97 Tf 71.23 0 Td[(::)]TJ/F70 8.97 Tf 12.29 0 Td[(A)]TJ/F71 8.97 Tf 7.51 0 Td[(u)-67(8)]TJ/F70 8.97 Tf 11.86 0 Td[(r)29(:C)]TJ/F71 8.97 Tf 14.28 0 Td[(u)-67(9)]TJ/F70 8.97 Tf 11.86 0 Td[(r)29(:D)]TJ/F86 8.97 Tf 16.18 0 Td[(is)-207(subsumed)-206(by)]TJ/F71 8.97 Tf 56.4 0 Td[(9)]TJ/F70 8.97 Tf 5.11 0 Td[(r)28(:)]TJ/F15 8.97 Tf 6.47 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(D)]TJ/F71 8.97 Tf 8.45 0 Td[(t)]TJ/F70 8.97 Tf 6.75 0 Td[(E)]TJ/F15 8.97 Tf 7.29 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(,)]TJ -242.84 -10.41 Td[(it)-221(is)-221(unnecessary)-219(to)-220(apply)-220(rule)]TJ/F15 8.97 Tf 107.52 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(l)]TJ/F71 8.97 Tf 2.9 0 Td[(::)]TJ/F15 8.97 Tf 12.29 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(,)-221(nor)-221(is)-220(it)-221(useful)-220(to)-221(carry)-220(the)-220(con-)]TJ -129.87 -10.41 Td[(cept)]TJ/F70 8.97 Tf 17.49 0 Td[(C)]TJ/F86 8.97 Tf 7.22 0 Td[(,)-284(when)-283(applying)-283(rule)-284(\050)]TJ/F70 8.97 Tf 80.17 0 Td[(l)]TJ/F73 8.97 Tf 2.9 0 Td[(3)]TJ/F86 8.97 Tf 7.13 0 Td[(\051.)-284(The)-283(solution)-283(is)-284(to)-284(simplify)-283(the)-284(se-)]TJ -114.91 -10.41 Td[(quent)-266(proof)-265(using)-266(a)-266(recursi)26(v)15(e)-266(analysis)-265(of)-266(the)-266(rele)26(v)25(ance)-266(of)-266(each)-266(com-)]TJ 0 -10.41 Td[(ponent.)-343(This)-344(procedure)-342(has)-344(similarities)-342(with)-343(non-modal)-342(proof)-343(con-)]TJ 0 -10.41 Td[(densation)-249(techniques)-248(used)-249(in)-250(theorem)-248(pro)15(ving)-249(\050e.g.,)-249(see)-249([11]\051.)]TJ ET endstream endobj 28 0 obj 33263 endobj 25 0 obj << /ProcSet [/PDF /Text] /Font << /F44 17 0 R /F47 29 0 R /F50 23 0 R /F56 30 0 R /F12 31 0 R /F94 32 0 R /F46 22 0 R /F89 18 0 R /F49 20 0 R /F95 33 0 R /F86 11 0 R /F71 12 0 R /F70 13 0 R /F87 15 0 R /F73 34 0 R /F15 14 0 R /F78 21 0 R /F83 7 0 R >> >> endobj 26 0 obj << /Type /Page /Contents 27 0 R /Resources 25 0 R /MediaBox [0 0 595.27 841.89] /Parent 24 0 R >> endobj 37 0 obj << /Length 38 0 R >> stream 1 0 0 1 50.33 768.38 cm BT /F49 7.97 Tf 0 0 Td[(9)]TJ/F81 7.97 Tf 4.7 0 Td[(friend)]TJ/F46 7.97 Tf 25.41 0 Td[(:)]TJ/F49 7.97 Tf 2.35 0 Td[(>)-237(u)-236(8)]TJ/F81 7.97 Tf 20.7 0 Td[(friend)]TJ/F46 7.97 Tf 25.41 0 Td[(:)]TJ/F49 7.97 Tf 2.35 0 Td[(:)]TJ/F43 7.97 Tf 5.64 0 Td[(\050\050)]TJ/F49 7.97 Tf 6.59 0 Td[(9)]TJ/F81 7.97 Tf 4.71 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F49 7.97 Tf 2.35 0 Td[(:)]TJ/F81 7.97 Tf 5.64 0 Td[(Doctor)]TJ/F43 7.97 Tf 25.41 0 Td[(\051)]TJ/F49 7.97 Tf 5.17 0 Td[(t)]TJ/F43 7.97 Tf 7.53 0 Td[(\050)]TJ/F49 7.97 Tf 3.3 0 Td[(9)]TJ/F81 7.97 Tf 4.7 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F81 7.97 Tf 2.35 0 Td[(Lawyer)]TJ/F43 7.97 Tf 25.41 0 Td[(\051\051)]TJ/F49 7.97 Tf -172.81 -8.14 Td[(`)-1196(9)]TJ/F81 7.97 Tf 19.41 0 Td[(friend)]TJ/F46 7.97 Tf 25.4 0 Td[(:)]TJ/F49 7.97 Tf 2.35 0 Td[(8)]TJ/F81 7.97 Tf 4.71 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F43 7.97 Tf 2.35 0 Td[(\050)]TJ/F81 7.97 Tf 3.29 0 Td[(Rich)]TJ/F49 7.97 Tf 18.82 0 Td[(t)]TJ/F81 7.97 Tf 7.53 0 Td[(Doctor)]TJ/F43 7.97 Tf 25.41 0 Td[(\051)]TJ/F89 7.97 Tf -187.91 -10.13 Td[(\050)]TJ/F46 7.97 Tf 2.66 0 Td[(l)]TJ/F49 7.97 Tf 2.62 0 Td[(^)]TJ/F89 7.97 Tf 5.64 0 Td[(\051)]TJ ET 13.33 -18.27 204.28 0.4 re f 1 0 0 1 225.58 -18.27 cm BT /F89 7.97 Tf 0 0 Td[(\0501\051)]TJ/F49 7.97 Tf -224.19 -12.53 Td[(9)]TJ/F81 7.97 Tf 4.7 0 Td[(friend)]TJ/F46 7.97 Tf 25.41 0 Td[(:)]TJ/F49 7.97 Tf 2.35 0 Td[(>)]TJ/F46 7.97 Tf 7.66 0 Td[(;)]TJ/F49 7.97 Tf 5.56 0 Td[(8)]TJ/F81 7.97 Tf 4.7 0 Td[(friend)]TJ/F46 7.97 Tf 25.41 0 Td[(:)]TJ/F49 7.97 Tf 2.35 0 Td[(:)]TJ/F43 7.97 Tf 5.65 0 Td[(\050\050)]TJ/F49 7.97 Tf 6.58 0 Td[(9)]TJ/F81 7.97 Tf 4.71 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F49 7.97 Tf 2.35 0 Td[(:)]TJ/F81 7.97 Tf 5.65 0 Td[(Doctor)]TJ/F43 7.97 Tf 25.4 0 Td[(\051)]TJ/F49 7.97 Tf 5.18 0 Td[(t)]TJ/F43 7.97 Tf 7.52 0 Td[(\050)]TJ/F49 7.97 Tf 3.3 0 Td[(9)]TJ/F81 7.97 Tf 4.7 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F81 7.97 Tf 2.35 0 Td[(Lawyer)]TJ/F43 7.97 Tf 25.41 0 Td[(\051\051)]TJ/F49 7.97 Tf -171.42 -8.14 Td[(`)-1196(9)]TJ/F81 7.97 Tf 19.41 0 Td[(friend)]TJ/F46 7.97 Tf 25.4 0 Td[(:)]TJ/F49 7.97 Tf 2.35 0 Td[(8)]TJ/F81 7.97 Tf 4.71 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F43 7.97 Tf 2.35 0 Td[(\050)]TJ/F81 7.97 Tf 3.29 0 Td[(Rich)]TJ/F49 7.97 Tf 18.82 0 Td[(t)]TJ/F81 7.97 Tf 7.53 0 Td[(Doctor)]TJ/F43 7.97 Tf 25.41 0 Td[(\051)]TJ/F89 7.97 Tf -187.91 -8.14 Td[(\050)]TJ/F46 7.97 Tf 2.66 0 Td[(l)]TJ/F55 7.97 Tf 2.62 0 Td[(3)]TJ/F89 7.97 Tf 6.36 0 Td[(\051)]TJ ET -211.53 -28.81 203.56 0.4 re f 1 0 0 1 0 -28.81 cm BT /F89 7.97 Tf 0 0 Td[(\0502\051)]TJ/F49 7.97 Tf -191.73 -12.52 Td[(>)]TJ/F46 7.97 Tf 7.66 0 Td[(;)]TJ/F49 7.97 Tf 5.56 0 Td[(:)]TJ/F43 7.97 Tf 5.64 0 Td[(\050\050)]TJ/F49 7.97 Tf 6.59 0 Td[(9)]TJ/F81 7.97 Tf 4.71 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F49 7.97 Tf 2.35 0 Td[(:)]TJ/F81 7.97 Tf 5.64 0 Td[(Doctor)]TJ/F43 7.97 Tf 25.41 0 Td[(\051)]TJ/F49 7.97 Tf 5.17 0 Td[(t)]TJ/F43 7.97 Tf 7.53 0 Td[(\050)]TJ/F49 7.97 Tf 3.3 0 Td[(9)]TJ/F81 7.97 Tf 4.7 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F81 7.97 Tf 2.35 0 Td[(Lawyer)]TJ/F43 7.97 Tf 25.41 0 Td[(\051\051)]TJ/F49 7.97 Tf -122.73 -8.14 Td[(`)-1196(8)]TJ/F81 7.97 Tf 19.41 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F43 7.97 Tf 2.35 0 Td[(\050)]TJ/F81 7.97 Tf 3.29 0 Td[(Rich)]TJ/F49 7.97 Tf 18.82 0 Td[(t)]TJ/F81 7.97 Tf 7.53 0 Td[(Doctor)]TJ/F43 7.97 Tf 25.4 0 Td[(\051)]TJ/F89 7.97 Tf -171.67 -8.14 Td[(\050)]TJ/F46 7.97 Tf 2.66 0 Td[(l)]TJ/F49 7.97 Tf 2.62 0 Td[(:_)]TJ/F89 7.97 Tf 11.29 0 Td[(\051)]TJ ET -206.61 -28.8 198.63 0.4 re f 1 0 0 1 0 -28.8 cm BT /F89 7.97 Tf 0 0 Td[(\0503\051)]TJ/F49 7.97 Tf -189.87 -12.52 Td[(>)]TJ/F46 7.97 Tf 7.66 0 Td[(;)]TJ/F49 7.97 Tf 5.56 0 Td[(:)]TJ/F43 7.97 Tf 5.64 0 Td[(\050)]TJ/F49 7.97 Tf 3.3 0 Td[(9)]TJ/F81 7.97 Tf 4.7 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F49 7.97 Tf 2.35 0 Td[(:)]TJ/F81 7.97 Tf 5.65 0 Td[(Doctor)]TJ/F43 7.97 Tf 25.4 0 Td[(\051)]TJ/F46 7.97 Tf 4.37 0 Td[(;)]TJ/F49 7.97 Tf 5.56 0 Td[(:)]TJ/F43 7.97 Tf 5.65 0 Td[(\050)]TJ/F49 7.97 Tf 3.29 0 Td[(9)]TJ/F81 7.97 Tf 4.7 0 Td[(child)]TJ/F46 7.97 Tf 21.18 0 Td[(:)]TJ/F81 7.97 Tf 2.35 0 Td[(Lawyer)]TJ/F43 7.97 Tf 25.4 0 Td[(\051)]TJ/F49 7.97 Tf -124.16 -8.14 Td[(`)-1196(8)]TJ/F81 7.97 Tf 19.41 0 Td[(child)]TJ/F46 7.97 Tf 21.17 0 Td[(:)]TJ/F43 7.97 Tf 2.35 0 Td[(\050)]TJ/F81 7.97 Tf 3.29 0 Td[(Rich)]TJ/F49 7.97 Tf 18.82 0 Td[(t)]TJ/F81 7.97 Tf 7.53 0 Td[(Doctor)]TJ/F43 7.97 Tf 25.4 0 Td[(\051)]TJ/F89 7.97 Tf -171.67 -8.14 Td[(\050)]TJ/F46 7.97 Tf 2.66 0 Td[(r)]TJ/F55 7.97 Tf 4.05 0 Td[(2)]TJ/F89 7.97 Tf 6.07 0 Td[(\051)]TJ ET -210.4 -28.8 202.42 0.4 re f 1 0 0 1 0 -28.8 cm BT /F89 7.97 Tf 0 0 Td[(\0504\051)]TJ/F49 7.97 Tf -182.85 -12.52 Td[(::)]TJ/F81 7.97 Tf 11.29 0 Td[(Doctor)]TJ/F46 7.97 Tf 26.48 0 Td[(;)]TJ/F49 7.97 Tf 5.56 0 Td[(:)]TJ/F81 7.97 Tf 5.64 0 Td[(Lawyer)]TJ/F49 7.97 Tf 31.35 0 Td[(`)]TJ/F81 7.97 Tf 11.11 0 Td[(Rich)]TJ/F49 7.97 Tf 18.82 0 Td[(t)]TJ/F81 7.97 Tf 7.53 0 Td[(Doctor)]TJ/F89 7.97 Tf -168.73 -8.14 Td[(\050)]TJ/F46 7.97 Tf 2.66 0 Td[(l)]TJ/F49 7.97 Tf 2.62 0 Td[(::)]TJ/F89 7.97 Tf 11.29 0 Td[(\051)]TJ ET -206.61 -20.66 198.63 0.4 re f 1 0 0 1 0 -20.66 cm BT /F89 7.97 Tf 0 0 Td[(\0505\051)]TJ/F81 7.97 Tf -177.2 -12.53 Td[(Doctor)]TJ/F46 7.97 Tf 26.48 0 Td[(;)]TJ/F49 7.97 Tf 5.55 0 Td[(:)]TJ/F81 7.97 Tf 5.65 0 Td[(Lawyer)]TJ/F49 7.97 Tf 31.34 0 Td[(`)]TJ/F81 7.97 Tf 11.12 0 Td[(Rich)]TJ/F49 7.97 Tf 18.82 0 Td[(t)]TJ/F81 7.97 Tf 7.52 0 Td[(Doctor)]TJ/F89 7.97 Tf -163.08 -8.14 Td[(\050)]TJ/F46 7.97 Tf 2.66 0 Td[(r)]TJ/F49 7.97 Tf 4.05 0 Td[(_)]TJ/F89 7.97 Tf 5.65 0 Td[(\051)]TJ ET -210.82 -20.67 202.84 0.4 re f 1 0 0 1 0 -20.67 cm BT /F89 7.97 Tf 0 0 Td[(\0506\051)]TJ/F81 7.97 Tf -175.82 -12.52 Td[(Doctor)]TJ/F46 7.97 Tf 26.48 0 Td[(;)]TJ/F49 7.97 Tf 5.56 0 Td[(:)]TJ/F81 7.97 Tf 5.65 0 Td[(Lawyer)]TJ/F49 7.97 Tf 31.34 0 Td[(`)]TJ/F81 7.97 Tf 11.12 0 Td[(Rich)]TJ/F46 7.97 Tf 18.01 0 Td[(;)]TJ/F81 7.97 Tf 5.55 0 Td[(Doctor)]TJ/F89 7.97 Tf -161.69 -8.14 Td[(\050)]TJ/F43 7.97 Tf 2.66 0 Td[(=)]TJ/F89 7.97 Tf 6.58 0 Td[(\051)]TJ ET -213.93 -20.66 205.96 0.4 re f 1 0 0 1 0 -20.66 cm BT /F89 7.97 Tf 0 0 Td[(\0507\051)]TJ -122.1 -12.52 Td[(T)-50(R)-10(U)-50(E)]TJ/F95 7.97 Tf -32.93 -16.49 Td[(Figur)18(e)-250(2.)]TJ/F89 7.97 Tf 38.38 0 Td[(Sequent)-249(proof.)]TJ/F86 8.97 Tf -107.93 -22.65 Td[(The)-302(other)-303(problems)-301(are)-303(related)-302(to)-303(the)-303(presentation)-301(of)-303(the)-303(sequent)]TJ -9.22 -10.41 Td[(rules)-226(to)-226(users.)-226(The)-226(solution)-226(here)-226(mainly)-225(in)40(v)20(olv)16(es)-226(the)-227(use)-226(of)-226(templates)]TJ 0 -10.41 Td[(to)-299(generate)-298(a)-298(surf)10(ace)-298(e)15(xplanation)-297(\050in)-299(one)-298(or)-299(more)-298(steps\051)-298(of)-299(each)-298(se-)]TJ 0 -10.41 Td[(quent)-249(rule)-249(application.)]TJ/F83 10.91 Tf 0 -29.47 Td[(3.1)-1000(Simplifying)-249(pr)18(oofs)]TJ/F86 8.97 Tf 0 -18.51 Td[(The)-245(sequent)-244(proof)-245(tree)-245(found)-245(by)-245(the)-245(theorem)-244(pro)15(v)15(er)-245(will)-245(be)-245(assumed)]TJ 0 -10.41 Td[(to)-242(be)-241(presented)-241(as)-241(a)-242(term,)-241(where)-241(the)-241(term)-241(constructor)-240(will)-241(be)-242(the)-241(rule)]TJ 0 -10.41 Td[(name,)-363(and)-362(its)-363(ar)18(guments)-362(will)-362(include)-362(the)-363(important)-362(meta-v)26(ariables)]TJ 0 -10.41 Td[(appearing)-248(in)-250(the)-249(sequent)-249(rule,)-249(as)-250(well)-249(as)-249(an)15(y)-250(sub-proofs.)]TJ 9.22 -10.41 Td[(F)16(or)-342(e)15(xample,)-341(consider)-341(a)-342(proof)-341(that)-341(starts)-342(with)-341(the)-342(application)-340(of)]TJ -9.22 -10.41 Td[(the)-250(\050)]TJ/F70 8.97 Tf 16.19 0 Td[(r)]TJ/F71 8.97 Tf 4.41 0 Td[(:u)]TJ/F86 8.97 Tf 12.29 0 Td[(\051)-249(rule)-250(to)]TJ/F71 8.97 Tf 4.14 -15.84 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F70 8.97 Tf 28.24 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(::)]TJ/F78 8.97 Tf 12.28 0 Td[(Lawyer)]TJ/F71 8.97 Tf 34.84 0 Td[(`)-735(:)]TJ/F15 8.97 Tf 18.37 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.87 0 Td[(u)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051)]TJ/F70 8.97 Tf 3.58 0 Td[(;)]TJ/F86 8.97 Tf -205.49 -15.84 Td[(leading)-210(to)]TJ/F71 8.97 Tf 37.15 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F70 8.97 Tf 28.24 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(::)]TJ/F78 8.97 Tf 12.28 0 Td[(Lawyer)]TJ/F71 8.97 Tf 34.84 0 Td[(`)-735(:)]TJ/F78 8.97 Tf 18.37 0 Td[(Rich)]TJ/F70 8.97 Tf 18.83 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Doctor)]TJ/F86 8.97 Tf 28.24 0 Td[(,)-211(follo)26(wed)-210(by)]TJ -198.44 -10.41 Td[(an)-362(application)-361(of)-362(\050)]TJ/F70 8.97 Tf 68.52 0 Td[(l)]TJ/F71 8.97 Tf 2.9 0 Td[(::)]TJ/F86 8.97 Tf 12.29 0 Td[(\051,)-362(and)-362(then)-362(the)-362(termination)-361(axiom)]TJ/F15 8.97 Tf 127.84 0 Td[(\050=\051)]TJ/F86 8.97 Tf 17.59 0 Td[(with)]TJ/F71 8.97 Tf -229.14 -10.41 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F86 8.97 Tf 28.24 0 Td[(.)-250(This)-249(w)10(ould)-249(be)-249(encoded)-249(as)-249(the)-250(term)]TJ/F105 8.97 Tf -19.23 -19.95 Td[(rNotAnd\050)]TJ/F78 8.97 Tf 35.87 0 Td[(Rich)]TJ/F105 8.97 Tf 18.83 0 Td[(,)]TJ/F78 8.97 Tf 4.39 0 Td[(Doctor)]TJ/F105 8.97 Tf 28.25 0 Td[(,)-211(lNotNot\050)]TJ/F78 8.97 Tf 37.27 0 Td[(Lawyer)]TJ/F105 8.97 Tf 28.24 0 Td[(,)-278(ident\050)]TJ/F71 8.97 Tf 27.41 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Doctor)]TJ/F105 8.97 Tf 28.25 0 Td[(\051\051\051)]TJ/F86 8.97 Tf -229.81 -18.38 Td[(where,)-376(for)-377(e)15(xample,)-376(the)-377(type)-376(of)-377(proof)-377(constructor)]TJ/F97 8.97 Tf 187.79 0 Td[(lNotNot)]TJ/F86 8.97 Tf 34.49 0 Td[(is)]TJ/F87 8.97 Tf 9.36 0 Td[(De-)]TJ -231.64 -9.37 Td[(scription)]TJ/F71 8.97 Tf 31.89 0 Td[()]TJ/F87 8.97 Tf 7.16 0 Td[(Pr)45(oof)]TJ/F86 8.97 Tf 20.02 0 Td[(.)]TJ -49.85 -9.37 Td[(W)81(e)-342(no)26(w)-342(describe)-340(a)-341(function)]TJ/F106 8.97 Tf 106 0 Td[(Rele)30(v)26(ant)]TJ/F86 8.97 Tf 35.7 0 Td[(,)-341(which)-341(tak)10(es)-341(a)-341(proof)-341(and)]TJ -150.92 -9.37 Td[(simplies)-256(it)-257(so)-257(that)-257(only)-257(rele)26(v)25(ant)-257(proof)-257(steps)-256(are)-257(k)10(ept)-257(and,)-257(for)-257(modal)]TJ 0 -9.37 Td[(rules,)-360(only)-360(those)-360(descriptions)-359(that)-361(are)-360(rele)26(v)25(ant)-361(to)-360(later)-360(parts)-360(of)-361(the)]TJ 0 -9.37 Td[(proof)-325(are)-325(carried)-324(into)-325(the)-325(sub-proof.)-323(This)-325(is)-325(accomplished)-323(by)-325(com-)]TJ 0 -9.37 Td[(puting)-386(tw)10(o)-387(such)-386(sets)-387(of)-387(rele)26(v)25(ant)-387(terms)-386(\050one)-387(for)-386(each)-387(side)-386(of)]TJ/F71 8.97 Tf 232.43 0 Td[(`)]TJ/F86 8.97 Tf 9.67 0 Td[(\051)]TJ -242.1 -9.37 Td[(for)]TJ/F87 8.97 Tf 13.8 0 Td[(e)16(very)]TJ/F86 8.97 Tf 22.61 0 Td[(step)-372(of)-372(the)-372(proof.)-371(The)-371(function)]TJ/F106 8.97 Tf 118.4 0 Td[(Rele)31(v)25(ant)]TJ/F86 8.97 Tf 39.03 0 Td[(tak)10(es)-372(as)-371(ar)18(gu-)]TJ -193.84 -9.37 Td[(ment)-339(a)]TJ/F87 8.97 Tf 28.02 0 Td[(Pr)46(oof)]TJ/F86 8.97 Tf 20.02 0 Td[(,)-340(and)-339(returns)-339(a)-340(three-tuple:)-338(the)-339(re)25(vised)-339(proof,)-339(plus)-339(the)]TJ -48.04 -9.37 Td[(abo)15(v)16(e-mentioned)-284(tw)10(o)-285(sets)-286(of)-285(concept)-285(terms,)-284(from)-285(which)-285(the)-286(current)]TJ 0 -9.37 Td[(sequent)-258(can)-258(be)-259(reconstructed.)-256(The)-259(function)-257(is)-259(dened)-258(by)-258(case)-258(analy-)]TJ 0 -9.37 Td[(sis)-215(of)-215(the)-214(proof)-215(step)-214(constructors,)-213(and)-215(is)-215(presented)-213(for)-215(some)-214(represen-)]TJ 0 -9.37 Td[(tati)25(v)16(e)-250(cases)-249(using)-249(pseudo-ML)-248(code,)-249(with)-249(pattern-matching)-247(notation.)]TJ 9.22 -9.37 Td[(Starting)-248(with)-249(the)-250(termination)-248(rules,)-249(we)-249(ha)20(v)15(e,)-249(for)-250(e)16(xample)]TJ/F106 8.97 Tf 5.94 -14.42 Td[(Rele)31(v)26(ant)]TJ/F105 8.97 Tf 35.69 0 Td[(\050)-278(ident\050A\051)-276(\051)-278(=)-277(\050)-278(ident\050A\051)-277(,)]TJ/F71 8.97 Tf 96.92 0 Td[(f)]TJ/F105 8.97 Tf 4.6 0 Td[(A)]TJ/F71 8.97 Tf 5.98 0 Td[(g)]TJ/F105 8.97 Tf 4.61 0 Td[(,)]TJ/F71 8.97 Tf 4.99 0 Td[(f)]TJ/F105 8.97 Tf 4.6 0 Td[(A)]TJ/F71 8.97 Tf 5.98 0 Td[(g)]TJ/F105 8.97 Tf 7.1 0 Td[(\051)]TJ/F106 8.97 Tf -170.47 -9.37 Td[(Rele)31(v)26(ant)]TJ/F105 8.97 Tf 35.69 0 Td[(\050)-278(lBot\050\051)-277(\051)-277(=)-278(\050)-278(lBot\050\051)-277(,)]TJ/F71 8.97 Tf 76.97 0 Td[(;)]TJ/F105 8.97 Tf 4.61 0 Td[(,)]TJ/F71 8.97 Tf 4.99 0 Td[(;)]TJ/F105 8.97 Tf 4.6 0 Td[(\051)]TJ/F106 8.97 Tf -126.86 -9.37 Td[(Rele)31(v)26(ant)]TJ/F105 8.97 Tf 35.69 0 Td[(\050)-278(lContr)11(ad\050A\051)-276(\051)-278(=)-278(\050)-278(lContr)12(ad\050A\051)-277(,)]TJ/F71 8.97 Tf 125.62 0 Td[(f)]TJ/F105 8.97 Tf 4.61 0 Td[(A,)]TJ/F71 8.97 Tf 10.97 0 Td[(:)]TJ/F105 8.97 Tf 6.14 0 Td[(A)]TJ/F71 8.97 Tf 5.98 0 Td[(g)]TJ/F105 8.97 Tf 4.61 0 Td[(,)]TJ/F71 8.97 Tf 2.49 0 Td[(;)]TJ/F105 8.97 Tf 4.61 0 Td[(\051)]TJ/F86 8.97 Tf -206.66 -14.49 Td[(The)-322(code)-322(for)]TJ/F97 8.97 Tf 50.01 0 Td[(lNotNot)]TJ/F15 8.97 Tf 31.11 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(A;)]TJ/F101 8.97 Tf 11.01 0 Td[(Pf)]TJ/F15 8.97 Tf 10.97 0 Td[(\051)]TJ/F86 8.97 Tf 6.48 0 Td[(w)10(ould)-322(rst)-322(recursi)26(v)15(ely)-322(process)-322(its)]TJ -122.38 -9.37 Td[(sub-proof)]TJ/F101 8.97 Tf 36.98 0 Td[(Pf)]TJ/F86 8.97 Tf 13.09 0 Td[(\050see)-236(the)]TJ/F85 8.97 Tf 29.63 0 Td[(let)]TJ/F86 8.97 Tf 11.58 0 Td[(statement)-234(in)-236(the)-235(follo)25(wing)-235(pseudo-code\051;)-234(if)]TJ -91.28 -9.37 Td[(it)-301(turns)-300(out)-300(that)-300(the)-300(concept)]TJ/F70 8.97 Tf 102.85 0 Td[(A)]TJ/F86 8.97 Tf 9.61 0 Td[(w)10(as)-300(not)-300(needed)-300(\050to)-300(detect)-300(a)-300(termina-)]TJ -112.46 -9.37 Td[(tion\051)-261(in)-260(the)-261(sub-proof,)-259(then)]TJ/F71 8.97 Tf 99.12 0 Td[(::)]TJ/F70 8.97 Tf 12.29 0 Td[(A)]TJ/F86 8.97 Tf 9.25 0 Td[(itself)-261(is)-260(irrele)25(v)26(ant)-261(to)-261(the)-260(proof,)-261(and)]TJ -120.66 -9.37 Td[(the)-234(step)-234(is)-235(skipped.)-233(Otherwise,)-233(the)-234(sub-proof)-233(e)15(xplains)-233(where)-234(the)]TJ/F70 8.97 Tf 230.09 0 Td[(A)]TJ/F86 8.97 Tf 9.01 0 Td[(is)]TJ -239.1 -9.37 Td[(used,)-239(and)-239(mak)10(es)-239(us)-240(be)-239(interested)-238(in)-240(e)15(xplaining)-238(where)-239(the)]TJ/F71 8.97 Tf 204.81 0 Td[(::)]TJ/F70 8.97 Tf 12.29 0 Td[(A)]TJ/F86 8.97 Tf 9.06 0 Td[(came)]TJ -226.16 -9.37 Td[(from.)]TJ/F106 8.97 Tf 278.17 661.94 Td[(Rele)31(v)25(ant)]TJ/F105 8.97 Tf 35.69 0 Td[(\050)-278(lNotNot\050A,Pf\051)-275(\051)-278(=)]TJ/F85 8.97 Tf -26.73 -9.37 Td[(let)]TJ/F105 8.97 Tf 11.96 0 Td[(\050Pf1,Lhs1,Rhs1\051)-274(=)]TJ/F106 8.97 Tf 75 0 Td[(Rele)31(v)25(ant)]TJ/F105 8.97 Tf 35.69 0 Td[(\050Pf\051)]TJ/F85 8.97 Tf 16.94 0 Td[(in)]TJ -130.62 -9.37 Td[(if)]TJ/F105 8.97 Tf 7.97 0 Td[(\050A)]TJ/F71 8.97 Tf 11.46 0 Td[(2)]TJ/F105 8.97 Tf 8.64 0 Td[(Lhs1\051)]TJ/F85 8.97 Tf -28.07 -9.37 Td[(then)]TJ/F105 8.97 Tf 21.92 0 Td[(\050lNotNot\050A,Pf1\051,)-275(Lhs1)]TJ/F71 8.97 Tf 87.7 0 Td[( )-278(f)]TJ/F105 8.97 Tf 14.27 0 Td[(A)]TJ/F71 8.97 Tf 5.98 0 Td[(g)-277([)-278(f::)]TJ/F105 8.97 Tf 32.63 0 Td[(A)]TJ/F71 8.97 Tf 5.98 0 Td[(g)]TJ/F105 8.97 Tf 4.61 0 Td[(,)-278(Rhs1)-277(\051)]TJ/F85 8.97 Tf -173.09 -9.37 Td[(else)]TJ/F105 8.97 Tf 18.93 0 Td[(\050Pf1,Lhs1,Rhs1\051)]TJ/F86 8.97 Tf -52.02 -12.94 Td[(Similarly)66(,)-193(in)-193(dealing)-192(with)]TJ/F97 8.97 Tf 91.29 0 Td[(rNotAnd)]TJ/F15 8.97 Tf 33.28 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(A;)-172(B)-50(;)]TJ/F101 8.97 Tf 22.52 0 Td[(Pf)]TJ/F15 8.97 Tf 10.98 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(,)-193(if)-193(neither)]TJ/F71 8.97 Tf 37.82 0 Td[(:)]TJ/F70 8.97 Tf 6.14 0 Td[(A)]TJ/F86 8.97 Tf 8.65 0 Td[(nor)]TJ/F71 8.97 Tf 13.68 0 Td[(:)]TJ/F70 8.97 Tf 6.14 0 Td[(B)]TJ/F86 8.97 Tf -237.66 -9.37 Td[(w)10(as)-250(useful)-249(in)-249(the)-250(sub-proof)-248(then)-249(the)-249(rule)-250(can)-249(be)-250(skipped:)]TJ/F106 8.97 Tf 15.16 -12.7 Td[(Rele)31(v)25(ant)]TJ/F105 8.97 Tf 35.69 0 Td[(\050)-278(rNotAnd\050A,B)22(,Pf\051)-277(\051)-278(=)]TJ/F85 8.97 Tf -26.73 -9.37 Td[(let)]TJ/F105 8.97 Tf 11.96 0 Td[(\050Pf1,Lhs1,Rhs1\051)-274(=)]TJ/F106 8.97 Tf 75 0 Td[(Rele)31(v)25(ant)]TJ/F105 8.97 Tf 35.69 0 Td[(\050Pf\051)]TJ/F85 8.97 Tf 16.94 0 Td[(in)]TJ -130.62 -9.37 Td[(if)]TJ/F105 8.97 Tf 7.97 0 Td[(\050)]TJ/F71 8.97 Tf 2.99 0 Td[(:)]TJ/F105 8.97 Tf 6.14 0 Td[(A)]TJ/F71 8.97 Tf 8.47 0 Td[(2)]TJ/F105 8.97 Tf 8.64 0 Td[(Rhs1\051)]TJ/F85 8.97 Tf 26.41 0 Td[(or)19(else)]TJ/F105 8.97 Tf 24.73 0 Td[(\050)]TJ/F71 8.97 Tf 2.99 0 Td[(:)]TJ/F105 8.97 Tf 6.14 0 Td[(B)]TJ/F71 8.97 Tf 8.48 0 Td[(2)]TJ/F105 8.97 Tf 8.63 0 Td[(Rhs1\051)]TJ/F85 8.97 Tf -111.59 -9.37 Td[(then)]TJ/F105 8.97 Tf 21.92 0 Td[(\050)-278(rNotAnd\050A,B)22(,Pf1\051,)-554(Lhs1,)]TJ 7.47 -9.37 Td[(Rhs1)]TJ/F71 8.97 Tf 23.42 0 Td[( )-278(f:)]TJ/F105 8.97 Tf 20.41 0 Td[(A,)]TJ/F71 8.97 Tf 8.48 0 Td[(:)]TJ/F105 8.97 Tf 6.14 0 Td[(B)]TJ/F71 8.97 Tf 5.98 0 Td[(g)-278([)-277(f:)]TJ/F105 8.97 Tf 26.49 0 Td[(\050A)]TJ/F71 8.97 Tf 8.96 0 Td[(u)]TJ/F105 8.97 Tf 6.15 0 Td[(B\051)]TJ/F71 8.97 Tf 8.96 0 Td[(g)]TJ/F105 8.97 Tf 7.1 0 Td[(\051)]TJ/F85 8.97 Tf -151.48 -9.37 Td[(else)]TJ/F105 8.97 Tf 18.93 0 Td[(\050Pf1,Lhs1,Rhs1\051)]TJ/F86 8.97 Tf -42.8 -12.69 Td[(F)15(or)-222(e)15(xample,)-221(by)-223(applying)]TJ/F106 8.97 Tf 93.14 0 Td[(Rele)31(v)25(ant)]TJ/F86 8.97 Tf 37.69 0 Td[(to)-223(proof)-222(3.1,)-222(we)-222(w)10(ould)-222(obtain)]TJ -140.05 -9.37 Td[(the)-372(proof)]TJ/F97 8.97 Tf 37.06 0 Td[(rNotAnd)]TJ/F15 8.97 Tf 33.28 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F70 8.97 Tf 18.83 0 Td[(;)]TJ/F78 8.97 Tf 4.1 0 Td[(Doctor)]TJ/F70 8.97 Tf 28.24 0 Td[(;)]TJ/F97 8.97 Tf 4.1 0 Td[(ident)]TJ/F15 8.97 Tf 19.14 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051)]TJ/F86 8.97 Tf 7.17 0 Td[(,)-372(plus)-372(the)-372(sets)]TJ/F71 8.97 Tf -193.47 -9.37 Td[(f:)]TJ/F78 8.97 Tf 10.76 0 Td[(Doctor)]TJ/F71 8.97 Tf 28.24 0 Td[(g)]TJ/F86 8.97 Tf 6.37 0 Td[(and)]TJ/F71 8.97 Tf 14.72 0 Td[(f:)]TJ/F86 8.97 Tf 10.75 0 Td[(\050)]TJ/F78 8.97 Tf 2.99 0 Td[(Rich)]TJ/F71 8.97 Tf 18.82 0 Td[(u)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F86 8.97 Tf 28.24 0 Td[(\051)]TJ/F71 8.97 Tf 2.99 0 Td[(g)]TJ/F86 8.97 Tf 4.61 0 Td[(,)-196(representing)-195(the)-197(rele)26(v)25(ant)-196(parts)]TJ -134.64 -9.37 Td[(of)-250(the)-249(sequent)-249(deri)26(v)15(ed)-250(by)-249(the)-250(proof.)]TJ 9.22 -9.37 Td[(Finally)66(,)-347(we)-346(need)-347(to)-346(consider)-346(the)-346(modal)-346(rules.)-347(First,)-346(observ)16(e)-346(that)]TJ -9.22 -9.37 Td[(modal)-202(rule)-202(applications)-200(appearing)-201(in)-202(our)-202(proof)-202(can)-202(no)-202(longer)-201(be)-203(use-)]TJ 0 -9.37 Td[(less,)-303(so)-304(our)-303(main)-303(task)-303(will)-303(be)-303(to)-303(thin)-303(out)-304(the)-303(terms)-303(that)-303(are)-303(carried)]TJ 0 -9.37 Td[(into)-250(the)-249(sub-proof.)]TJ 9.22 -9.37 Td[(F)15(or)-249(e)15(xample,)-249(in)-249(pro)15(ving)-249(that)]TJ/F71 8.97 Tf 46.91 -12.81 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Adult)]TJ/F70 8.97 Tf 23.54 0 Td[(;)]TJ/F71 8.97 Tf 6.34 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(::)]TJ/F78 8.97 Tf 12.29 0 Td[(Doctor)]TJ/F71 8.97 Tf -100.56 -9.37 Td[(`)-735(9)]TJ/F78 8.97 Tf 17.35 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Doctor)]TJ/F70 8.97 Tf 28.25 0 Td[(;)]TJ/F71 8.97 Tf 6.33 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Rich)]TJ/F86 8.97 Tf 58.5 4.31 Td[(\0503.1\051)]TJ -227.9 -17.67 Td[(rule)-210(\050)]TJ/F70 8.97 Tf 18.81 0 Td[(l)]TJ/F73 8.97 Tf 2.9 0 Td[(3)]TJ/F86 8.97 Tf 7.13 0 Td[(\051)-210(w)11(ould)-209(gather)]TJ/F87 8.97 Tf 53.32 0 Td[(e)15(very)]TJ/F86 8.97 Tf 21.16 0 Td[(restriction)-208(on)-209(role)]TJ/F78 8.97 Tf 64.91 0 Td[(child)]TJ/F86 8.97 Tf 23.53 0 Td[(,)-210(producing)-208(the)]TJ -191.76 -9.37 Td[(subgoal)]TJ/F78 8.97 Tf 30.4 0 Td[(Person)]TJ/F70 8.97 Tf 28.25 0 Td[(;)]TJ/F71 8.97 Tf 4.09 0 Td[(::)]TJ/F78 8.97 Tf 12.29 0 Td[(Doctor)]TJ/F71 8.97 Tf 35.34 0 Td[(`)]TJ/F78 8.97 Tf 12.73 0 Td[(Doctor)]TJ/F70 8.97 Tf 28.24 0 Td[(;)]TJ/F78 8.97 Tf 4.1 0 Td[(Rich)]TJ/F86 8.97 Tf 18.83 0 Td[(.)-279(Ho)26(we)25(v)15(er)41(,)-280(the)-278(only)]TJ -174.27 -9.37 Td[(rele)25(v)25(ant)-271(parts)-270(from)-271(both)-271(sides)-270(are)-271(those)-271(dealing)-270(with)]TJ/F78 8.97 Tf 191.3 0 Td[(Doctor)]TJ/F86 8.97 Tf 28.25 0 Td[(,)-271(so)-271(we)]TJ -219.55 -9.37 Td[(will)-349(w)11(ant)-349(the)-348(sequent)-348(produced)-347(to)-348(be)-349(only)]TJ/F71 8.97 Tf 159.42 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(::)]TJ/F78 8.97 Tf 12.29 0 Td[(Doctor)]TJ/F71 8.97 Tf 36.52 0 Td[(`)]TJ -232.85 -9.37 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F78 8.97 Tf 2.55 0 Td[(Doctor)]TJ/F86 8.97 Tf 28.25 0 Td[(.)]TJ -56.84 -9.37 Td[(When)-300(applying)-299(modal)-300(rules)-300(we)-301(need)-300(to)-301(track)-300(the)-300(precise)-300(form)-300(of)]TJ -9.22 -9.37 Td[(the)-277(rele)25(v)26(ant)-277(subconcepts.)-276(W)81(e)-277(therefore)-276(distinguish)-276(in)-277(the)-277(antecedent)]TJ/F70 8.97 Tf 0 -9.37 Td[(X)]TJ/F50 5.98 Tf 8.32 3.81 Td[(0)]TJ/F86 8.97 Tf 5.92 -3.81 Td[(of)-360(the)-361(top)-360(sequent)-360(those)-360(terms)-360(that)-360(come)-360(from)-360(formul)-359(of)-361(the)]TJ -14.24 -9.37 Td[(form)]TJ/F71 8.97 Tf 20.45 0 Td[(8)]TJ/F70 8.97 Tf 5.12 0 Td[(r)29(:a)]TJ/F86 8.97 Tf 14.36 0 Td[(from)-336(those)-335(that)-336(come)-335(from)-336(formul)-335(of)-336(the)-336(form)]TJ/F71 8.97 Tf 180.05 0 Td[(:9)]TJ/F70 8.97 Tf 11.27 0 Td[(r)29(:a)]TJ/F86 8.97 Tf 11.34 0 Td[(;)]TJ -242.59 -9.37 Td[(lik)10(e)25(wise)-255(for)-255(the)-255(succedent)]TJ/F70 8.97 Tf 95.52 0 Td[(Y)]TJ/F50 5.98 Tf 7.39 3.81 Td[(0)]TJ/F86 8.97 Tf 2.69 -3.81 Td[(.)-255(Thus)-255(the)-256(\050)]TJ/F70 8.97 Tf 41 0 Td[(l)]TJ/F73 8.97 Tf 2.9 0 Td[(3)]TJ/F86 8.97 Tf 7.12 0 Td[(\051)-256(rule)-255(needs)-255(a)-255(list)-256(of)-255(four)]TJ -156.62 -9.37 Td[(ar)18(guments:)]TJ/F70 8.97 Tf 42.75 0 Td[(La;)-172(Lns;)-171(Rs)]TJ/F86 8.97 Tf 49.85 0 Td[(and)]TJ/F70 8.97 Tf 16.01 0 Td[(Rna)]TJ/F86 8.97 Tf 17.48 0 Td[(,)-340(such)-341(that)-340(the)-341(antecedent)]TJ/F70 8.97 Tf 96.71 0 Td[(X)]TJ/F50 5.98 Tf 8.32 3.81 Td[(0)]TJ/F15 8.97 Tf 6.8 -3.81 Td[(=)]TJ/F70 8.97 Tf -237.92 -9.37 Td[(La)]TJ/F71 8.97 Tf 13.31 0 Td[([)]TJ/F70 8.97 Tf 8.29 0 Td[(Lns)]TJ/F86 8.97 Tf 18.5 0 Td[(and)-265(the)-264(succedent)]TJ/F70 8.97 Tf 66.39 0 Td[(Y)]TJ/F50 5.98 Tf 7.4 3.81 Td[(0)]TJ/F15 8.97 Tf 5.5 -3.81 Td[(=)]TJ/F70 8.97 Tf 9.99 0 Td[(Rs)]TJ/F71 8.97 Tf 13.47 0 Td[([)]TJ/F70 8.97 Tf 8.3 0 Td[(Rna)]TJ/F86 8.97 Tf 17.48 0 Td[(,)-264(where,)-264(for)-265(e)15(xample,)]TJ/F70 8.97 Tf -168.63 -9.37 Td[(La)]TJ/F15 8.97 Tf 14.22 0 Td[(=)]TJ/F71 8.97 Tf 10.23 0 Td[(f)]TJ/F70 8.97 Tf 4.61 0 Td[(a)]TJ/F71 8.97 Tf 7.95 0 Td[(j)-342(8)]TJ/F70 8.97 Tf 10.74 0 Td[(r)29(:a)]TJ/F71 8.97 Tf 17.48 0 Td[(2)]TJ/F70 8.97 Tf 9.21 0 Td[(X)]TJ/F71 8.97 Tf 8.31 0 Td[(g)]TJ/F86 8.97 Tf 7.11 0 Td[(and)]TJ/F70 8.97 Tf 15.46 0 Td[(Lns)]TJ/F15 8.97 Tf 19.19 0 Td[(=)]TJ/F71 8.97 Tf 10.23 0 Td[(f:)]TJ/F70 8.97 Tf 10.75 0 Td[(a)]TJ/F71 8.97 Tf 7.95 0 Td[(j)-621(:9)]TJ/F70 8.97 Tf 19.39 0 Td[(r)29(:a)]TJ/F71 8.97 Tf 17.48 0 Td[(2)]TJ/F70 8.97 Tf 9.2 0 Td[(X)]TJ/F71 8.97 Tf 8.32 0 Td[(g)]TJ/F86 8.97 Tf 4.61 0 Td[(.)-279(Each)-279(of)]TJ -212.44 -9.37 Td[(these)-293(sets)-293(may)-293(be)-293(diminished)-292(by)-293(the)-293(rele)25(v)26(ance)-293(list)]TJ/F70 8.97 Tf 192.09 0 Td[(Lhs)]TJ/F15 8.97 Tf 15.88 0 Td[(1)]TJ/F86 8.97 Tf 7.24 0 Td[(returned)]TJ -215.21 -9.37 Td[(by)-250(the)-249(recursi)26(v)15(e)-250(call)-249(on)-250(the)-249(sub-proof:)]TJ/F106 8.97 Tf 15.16 -12.69 Td[(Rele)31(v)25(ant)]TJ/F105 8.97 Tf 35.69 0 Td[(\050)-278(lSome\050p)37(,B)20(,[La,Lns)16(,Rs)16(,Rna],Pf\051)-276(\051)-278(=)]TJ/F85 8.97 Tf -26.73 -9.37 Td[(let)]TJ/F105 8.97 Tf 11.36 0 Td[(\050Pf1,Lhs1,Rhs1\051)-275(=)]TJ/F106 8.97 Tf 75.01 0 Td[(Rele)31(v)25(ant)]TJ/F105 8.97 Tf 35.69 0 Td[(\050Pf\051)]TJ/F85 8.97 Tf 19.43 0 Td[(and)]TJ/F105 8.97 Tf -130.13 -9.37 Td[(\050La1=La)]TJ/F71 8.97 Tf 35.64 0 Td[(\134)]TJ/F105 8.97 Tf 8.64 0 Td[(Lhs1\051)]TJ/F85 8.97 Tf 24.92 0 Td[(and)]TJ/F105 8.97 Tf 16.94 0 Td[(\050Lns1=Lns)]TJ/F71 8.97 Tf 44.61 0 Td[(\134)]TJ/F105 8.97 Tf 8.64 0 Td[(Lhs1\051)]TJ/F85 8.97 Tf 24.91 0 Td[(and)]TJ/F105 8.97 Tf -164.3 -9.37 Td[(\050Rs1=Rs)]TJ/F71 8.97 Tf 37.62 0 Td[(\134)]TJ/F105 8.97 Tf 8.63 0 Td[(Rhs1\051)]TJ/F85 8.97 Tf 26.41 0 Td[(and)]TJ/F105 8.97 Tf 16.95 0 Td[(\050Rna1=Rna)]TJ/F71 8.97 Tf 48.58 0 Td[(\134)]TJ/F105 8.97 Tf 8.64 0 Td[(Rhs1\051)]TJ/F85 8.97 Tf -158.19 -9.5 Td[(in)]TJ/F105 8.97 Tf 9.38 0 Td[(\050lSome\050p)36(,B)21(,[La1,Lns1,Rs1,Rna1],Pf1\051)-273(,)]TJ/F71 8.97 Tf 2.99 -9.37 Td[(f9)]TJ/F105 8.97 Tf 9.73 0 Td[(p)36(.B)]TJ/F71 8.97 Tf 13.14 0 Td[(g[)-277(f8)]TJ/F105 8.97 Tf 22.97 0 Td[(p)35(.A)]TJ/F71 8.97 Tf 15.64 0 Td[(j)]TJ/F105 8.97 Tf 5.05 0 Td[(A)]TJ/F71 8.97 Tf 8.47 0 Td[(2)]TJ/F105 8.97 Tf 8.64 0 Td[(La1)]TJ/F71 8.97 Tf 14.96 0 Td[(g)-277([)-278(f:9)]TJ/F105 8.97 Tf 31.6 0 Td[(p)35(.A)]TJ/F71 8.97 Tf 15.64 0 Td[(j)-278(:)]TJ/F105 8.97 Tf 11.2 0 Td[(A)]TJ/F71 8.97 Tf 8.47 0 Td[(2)]TJ/F105 8.97 Tf 8.63 0 Td[(Lns1)]TJ/F71 8.97 Tf 19.44 0 Td[(g)]TJ/F105 8.97 Tf 4.61 0 Td[(,)]TJ/F71 8.97 Tf -198.19 -9.37 Td[(f9)]TJ/F105 8.97 Tf 9.73 0 Td[(p)36(.A)]TJ/F71 8.97 Tf 15.63 0 Td[(j)]TJ/F105 8.97 Tf 5.05 0 Td[(A)]TJ/F71 8.97 Tf 8.48 0 Td[(2)]TJ/F105 8.97 Tf 8.63 0 Td[(Rs1)]TJ/F71 8.97 Tf 15.95 0 Td[(g)-277([)-278(f:8)]TJ/F105 8.97 Tf 31.6 0 Td[(p)35(.A)]TJ/F71 8.97 Tf 15.64 0 Td[(j)-278(:)]TJ/F105 8.97 Tf 11.2 0 Td[(A)]TJ/F71 8.97 Tf 8.47 0 Td[(2)]TJ/F105 8.97 Tf 8.64 0 Td[(Rna1)]TJ/F71 8.97 Tf 21.42 0 Td[(g)]TJ/F105 8.97 Tf -154.87 -9.78 Td[(\051)]TJ/F86 8.97 Tf -42.06 -12.33 Td[(As)-250(a)-250(result,)-248(the)-250(sequent)-248(proof)-250(of)-249(\0503.1\051,)-249(represented)-248(by)]TJ/F105 8.97 Tf 15.16 -12.7 Td[(lSome\050)]TJ/F78 8.97 Tf 28.39 0 Td[(child)]TJ/F105 8.97 Tf 23.54 0 Td[(,)]TJ/F71 8.97 Tf 2.49 0 Td[(::)]TJ/F78 8.97 Tf 12.29 0 Td[(Doctor)]TJ/F105 8.97 Tf 28.24 0 Td[(,)-278([)]TJ/F71 8.97 Tf 7.48 0 Td[(f)]TJ/F78 8.97 Tf 4.61 0 Td[(Adult)]TJ/F71 8.97 Tf 23.53 0 Td[(g)]TJ/F105 8.97 Tf 4.61 0 Td[(,)]TJ/F71 8.97 Tf 2.5 0 Td[(;)]TJ/F105 8.97 Tf 4.6 0 Td[(,)]TJ/F71 8.97 Tf 2.5 0 Td[(f)]TJ/F78 8.97 Tf 4.6 0 Td[(Doctor)]TJ/F105 8.97 Tf 28.25 0 Td[(,)]TJ/F78 8.97 Tf 2.49 0 Td[(Rich)]TJ/F71 8.97 Tf 18.83 0 Td[(g)]TJ/F105 8.97 Tf 4.61 0 Td[(,)]TJ/F71 8.97 Tf 2.49 0 Td[(;)]TJ/F105 8.97 Tf 4.61 0 Td[(],)]TJ -182.27 -9.37 Td[(lNotNot\050)]TJ/F78 8.97 Tf 32.88 0 Td[(Doctor)]TJ/F105 8.97 Tf 28.25 0 Td[(,ident\050)]TJ/F78 8.97 Tf 24.91 0 Td[(Doctor)]TJ/F105 8.97 Tf 28.25 0 Td[(\051\051\051)]TJ/F86 8.97 Tf -157.84 -16.36 Td[(is)-250(reduced)-249(to)]TJ/F105 8.97 Tf 15.16 -12.7 Td[(lSome\050)]TJ/F78 8.97 Tf 28.39 0 Td[(child)]TJ/F105 8.97 Tf 23.54 0 Td[(,)]TJ/F71 8.97 Tf 2.49 0 Td[(::)]TJ/F78 8.97 Tf 12.29 0 Td[(Doctor)]TJ/F105 8.97 Tf 28.24 0 Td[(,)-278([)]TJ/F71 8.97 Tf 7.48 0 Td[(;)]TJ/F105 8.97 Tf 4.61 0 Td[(,)]TJ/F71 8.97 Tf 2.49 0 Td[(;)]TJ/F105 8.97 Tf 4.61 0 Td[(,)]TJ/F71 8.97 Tf 2.49 0 Td[(f)]TJ/F78 8.97 Tf 4.61 0 Td[(Doctor)]TJ/F71 8.97 Tf 28.24 0 Td[(g)]TJ/F105 8.97 Tf 4.61 0 Td[(,)]TJ/F71 8.97 Tf 2.49 0 Td[(;)]TJ/F105 8.97 Tf 4.61 0 Td[(],)]TJ -132.8 -9.37 Td[(lNotNot\050)]TJ/F78 8.97 Tf 32.88 0 Td[(Doctor)]TJ/F105 8.97 Tf 28.25 0 Td[(,ident\050)]TJ/F78 8.97 Tf 24.91 0 Td[(Doctor)]TJ/F105 8.97 Tf 28.25 0 Td[(\051\051\051)]TJ/F86 8.97 Tf -148.62 -12.69 Td[(In)-681(the)-681(original)-680(e)15(xample,)-680(from)-680(Section)-680(2,)]TJ/F106 8.97 Tf 172.64 0 Td[(Rele)31(v)25(ant)]TJ/F86 8.97 Tf 41.8 0 Td[(elimi-)]TJ -223.66 -9.37 Td[(nates)]TJ/F71 8.97 Tf 22.13 0 Td[(:9)]TJ/F78 8.97 Tf 11.26 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F86 8.97 Tf 31.94 0 Td[(from)-412(the)-412(application)-411(of)]TJ/F70 8.97 Tf 90.51 0 Td[(r)]TJ/F73 8.97 Tf 4.42 0 Td[(2)]TJ/F86 8.97 Tf 6.75 0 Td[(,)-413(by)-412(replacing)]TJ/F71 8.97 Tf -193.11 -9.37 Td[(f::)]TJ/F78 8.97 Tf 16.9 0 Td[(Doctor)]TJ/F86 8.97 Tf 28.24 0 Td[(,)]TJ/F71 8.97 Tf 2.24 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Lawyer)]TJ/F71 8.97 Tf 28.24 0 Td[(g)]TJ/F86 8.97 Tf 6.51 0 Td[(with)]TJ/F71 8.97 Tf 17.85 0 Td[(f::)]TJ/F78 8.97 Tf 16.89 0 Td[(Doctor)]TJ/F71 8.97 Tf 28.25 0 Td[(g)]TJ/F86 8.97 Tf 6.51 0 Td[(in)-212(the)-211(original)-211(proof)-212(step)]TJ/F97 8.97 Tf -157.78 -9.37 Td[(rAll)]TJ/F15 8.97 Tf 13.71 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(;)]TJ/F15 8.97 Tf 4.1 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F70 8.97 Tf 3.58 0 Td[(;)]TJ/F15 8.97 Tf 4.1 0 Td[([)]TJ/F71 8.97 Tf 2.56 0 Td[(;)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F71 8.97 Tf 4.09 0 Td[(f::)]TJ/F78 8.97 Tf 16.9 0 Td[(Doctor)]TJ/F70 8.97 Tf 28.24 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Lawyer)]TJ/F71 8.97 Tf 28.25 0 Td[(g)]TJ/F70 8.97 Tf 4.6 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(;)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F71 8.97 Tf 4.09 0 Td[(;)]TJ/F15 8.97 Tf 4.61 0 Td[(])]TJ/F70 8.97 Tf 2.56 0 Td[(;)]TJ ET 266.8 -403.65 2.69 0.4 re f 1 0 0 1 269.49 -403.65 cm BT /F15 8.97 Tf 0 0 Td[(\051)]TJ/F86 8.97 Tf 3.59 0 Td[(.)]TJ/F83 10.91 Tf -243.87 -26.42 Td[(3.2)-1000(Generating)-250(surface)-249(explanations)-250(fr)18(om)-250(pruned)]TJ 24.55 -10.41 Td[(pr)18(oofs.)]TJ/F86 8.97 Tf -24.55 -14.85 Td[(The)-283(follo)26(wing)-283(problems)-282(arise)-282(when)-283(trying)-282(to)-283(of)25(fer)-283(the)-282(\050reduced\051)-282(se-)]TJ 0 -9.37 Td[(quent)-249(proof)-250(as)-249(an)-250(e)16(xplanation:)]TJ -1.74 -14.55 Td[(1.)-555(The)-384(use)-384(of)-385(the)-384(comma)-383(as)-384(a)-385(separator)-383(on)-384(the)-384(antecedent)-383(side)-384(is)]TJ 11.71 -9.37 Td[(semantically)-292(equi)25(v)26(alent)-294(to)-295(conjunction,)-292(while)-294(on)-294(the)-294(succedent)-294(it)]TJ 0 -9.37 Td[(is)-224(disjunction;)-223(this)-224(is)-225(quite)-224(confusing)-223(to)-225(non-initiates.)-222(On)-225(the)-224(other)]TJ ET endstream endobj 38 0 obj 30028 endobj 35 0 obj << /ProcSet [/PDF /Text] /Font << /F49 20 0 R /F81 39 0 R /F46 22 0 R /F43 8 0 R /F89 18 0 R /F55 40 0 R /F95 33 0 R /F86 11 0 R /F83 7 0 R /F70 13 0 R /F71 12 0 R /F78 21 0 R /F15 14 0 R /F105 41 0 R /F97 42 0 R /F87 15 0 R /F106 43 0 R /F101 44 0 R /F85 10 0 R /F73 34 0 R /F50 23 0 R >> >> endobj 36 0 obj << /Type /Page /Contents 37 0 R /Resources 35 0 R /MediaBox [0 0 595.27 841.89] /Parent 24 0 R >> endobj 47 0 obj << /Length 48 0 R >> stream 1 0 0 1 52.33 762.02 cm BT /F44 5.98 Tf 0 0 Td[(\050)]TJ/F98 5.98 Tf 2.88 0 Td[(NotNot)]TJ/F44 5.98 Tf 19.9 0 Td[(\051)]TJ/F50 5.98 Tf 32.09 0 Td[(::)]TJ/F47 5.98 Tf 9.97 0 Td[(a)]TJ/F50 5.98 Tf 4.84 0 Td[()]TJ/F47 5.98 Tf 11.54 0 Td[(a)]TJ/F44 5.98 Tf -81.22 -12.49 Td[(\050)]TJ/F98 5.98 Tf 2.88 0 Td[(NotAnd)]TJ/F44 5.98 Tf 20.74 0 Td[(\051)]TJ/F50 5.98 Tf 15.42 0 Td[(:)]TJ/F44 5.98 Tf 4.98 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(u)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F50 5.98 Tf 3.28 0 Td[()]TJ/F44 5.98 Tf 6.8 0 Td[(\051)]TJ/F50 5.98 Tf 3.69 0 Td[()-134(:)]TJ/F47 5.98 Tf 11.54 0 Td[(a)]TJ/F50 5.98 Tf 4.04 0 Td[(t:)]TJ/F47 5.98 Tf 9.96 0 Td[(b)]TJ/F50 5.98 Tf 3.27 0 Td[()-3068(:)]TJ/F44 5.98 Tf 30.13 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(t)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F50 5.98 Tf 3.27 0 Td[()]TJ/F44 5.98 Tf 6.81 0 Td[(\051)]TJ/F50 5.98 Tf 3.69 0 Td[()-134(:)]TJ/F47 5.98 Tf 11.54 0 Td[(a)]TJ/F50 5.98 Tf 4.04 0 Td[(u:)]TJ/F47 5.98 Tf 9.96 0 Td[(b)]TJ/F50 5.98 Tf 3.27 0 Td[()]TJ/F44 5.98 Tf 18.9 0 Td[(\050)]TJ/F98 5.98 Tf 2.88 0 Td[(NotOr)]TJ/F44 5.98 Tf 16.9 0 Td[(\051)]TJ -221.77 -12.49 Td[(\050)]TJ/F98 5.98 Tf 2.88 0 Td[(NotSome)]TJ/F44 5.98 Tf 24.52 0 Td[(\051)]TJ/F50 5.98 Tf 22.71 0 Td[(:9)]TJ/F47 5.98 Tf 9.19 0 Td[(r)34(:a)]TJ/F50 5.98 Tf 10.38 0 Td[()-134(8)]TJ/F47 5.98 Tf 10.77 0 Td[(r)33(:)]TJ/F50 5.98 Tf 5.54 0 Td[(:)]TJ/F47 5.98 Tf 4.98 0 Td[(a)]TJ/F50 5.98 Tf 43.74 0 Td[(:8)]TJ/F47 5.98 Tf 9.18 0 Td[(r)32(:a)]TJ/F50 5.98 Tf 10.39 0 Td[()-134(9)]TJ/F47 5.98 Tf 10.77 0 Td[(r)33(:)]TJ/F50 5.98 Tf 5.54 0 Td[(:)]TJ/F47 5.98 Tf 4.98 0 Td[(a)]TJ/F44 5.98 Tf 26.1 0 Td[(\050)]TJ/F98 5.98 Tf 2.88 0 Td[(NotAll)]TJ/F44 5.98 Tf 17.22 0 Td[(\051)]TJ -221.77 -12.5 Td[(\050)]TJ/F98 5.98 Tf 2.88 0 Td[(AndAll)]TJ/F44 5.98 Tf 18.05 0 Td[(\051)]TJ/F50 5.98 Tf 9.35 0 Td[(8)]TJ/F47 5.98 Tf 4.2 0 Td[(r)32(:a)]TJ/F50 5.98 Tf 9.58 0 Td[(u8)]TJ/F47 5.98 Tf 9.19 0 Td[(r)33(:b)]TJ/F50 5.98 Tf 8.81 0 Td[()-137()-134(8)]TJ/F47 5.98 Tf 18.39 0 Td[(r)33(:)]TJ/F44 5.98 Tf 5.54 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(u)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F50 5.98 Tf 3.28 0 Td[()]TJ/F44 5.98 Tf 6.8 0 Td[(\051)]TJ/F50 5.98 Tf 6.92 0 Td[(9)]TJ/F47 5.98 Tf 4.2 0 Td[(r)32(:a)]TJ/F50 5.98 Tf 9.58 0 Td[(t9)]TJ/F47 5.98 Tf 9.19 0 Td[(r)33(:b)]TJ/F50 5.98 Tf 8.81 0 Td[()-137()-134(9)]TJ/F47 5.98 Tf 18.39 0 Td[(r)33(:)]TJ/F44 5.98 Tf 5.54 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(t)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F50 5.98 Tf 3.28 0 Td[()]TJ/F44 5.98 Tf 6.8 0 Td[(\051)-338(\050)]TJ/F98 5.98 Tf 7.78 0 Td[(OrSome)]TJ/F44 5.98 Tf 21.43 0 Td[(\051)]TJ -221.77 -12.49 Td[(\050)]TJ/F98 5.98 Tf 2.88 0 Td[(SomeBot)]TJ/F44 5.98 Tf 24.27 0 Td[(\051)]TJ/F50 5.98 Tf 26.22 0 Td[(9)]TJ/F47 5.98 Tf 4.2 0 Td[(r)32(:)]TJ/F50 5.98 Tf 5.54 0 Td[(?)-135()-135(?)-9359(8)]TJ/F47 5.98 Tf 79.06 0 Td[(r)32(:)]TJ/F50 5.98 Tf 5.54 0 Td[(>)-135()-135(>)]TJ/F44 5.98 Tf 53.65 0 Td[(\050)]TJ/F98 5.98 Tf 2.88 0 Td[(AllT)88(op)]TJ/F44 5.98 Tf 17.53 0 Td[(\051)]TJ -221.77 -12.49 Td[(\050)]TJ/F98 5.98 Tf 2.88 0 Td[(SomeAndAll)]TJ/F44 5.98 Tf 32.63 0 Td[(\051)]TJ/F50 5.98 Tf 5.11 0 Td[(9)]TJ/F47 5.98 Tf 4.21 0 Td[(r)33(:a)]TJ/F50 5.98 Tf 9.58 0 Td[(u8)]TJ/F47 5.98 Tf 9.18 0 Td[(r)32(:b)]TJ/F50 5.98 Tf 10.94 0 Td[()-355(9)]TJ/F47 5.98 Tf 12.09 0 Td[(r)33(:)]TJ/F44 5.98 Tf 5.54 0 Td[(\050)]TJ/F47 5.98 Tf 2.88 0 Td[(a)]TJ/F50 5.98 Tf 4.03 0 Td[(u)]TJ/F47 5.98 Tf 4.98 0 Td[(b)]TJ/F44 5.98 Tf 3.27 0 Td[(\051)]TJ/F50 5.98 Tf 2.88 0 Td[(u8)]TJ/F47 5.98 Tf 9.19 0 Td[(r)33(:b)]TJ/F95 7.97 Tf -108.79 -18.21 Td[(Figur)19(e)-250(3.)]TJ/F89 7.97 Tf 38.37 0 Td[(Rules)-250(for)-250(concept)-250(equi)25(v)25(alence)-250(used)-250(in)-250(e)15(xplanations)]TJ/F86 8.97 Tf -49.23 -24.57 Td[(hand,)-389(if)-389(we)-388(do)-389(not)-389(use)-389(the)-388(comma)-388(notation,)-388(inferences)-387(dealing)]TJ 0 -9.37 Td[(with)-316(the)-316(commutati)26(vity)-315(and)-316(associati)26(vity)-316(of)-316(simple)-315(propositional)]TJ 0 -9.37 Td[(connecti)26(v)15(es)-249(clutter)-249(e)15(xplanations)-248(unnecessarily)67(.)]TJ -11.7 -13.43 Td[(2.)-555(Se)26(v)15(eral)-410(rules)-410(are)-410(identical)-409(on)-410(the)-410(left)-410(and)-410(right)-410(hand)-409(side,)-410(and)]TJ 11.7 -9.37 Td[(might)-296(therefore)-296(be)-296(better)-296(presented)-295(as)-297(single)-296(rules)-296(for)-296(massaging)]TJ 0 -9.37 Td[(concepts)-249(into)-249(an)-250(equi)26(v)25(alent)-249(form)-249(\050e.g.,)-249(using)-249(de)-250(Mor)19(gan')61(s)-250(rules\051.)]TJ -11.7 -13.43 Td[(3.)-555(The)-403(inference)-402(rules)-403(for)-403(modal)-402(formulae)-402(are)-403(quite)-403(comple)16(x)-403(and)]TJ 11.7 -9.37 Td[(their)-294(v)25(alidity)-294(is)-294(entirely)-294(non-ob)16(vious)-293(\050and)-294(hence)-294(not)-294(a)-295(proper)-294(e)16(x-)]TJ 0 -9.37 Td[(planation)-239(step\051,)-239(since)-239(it)-240(is)-239(based)-239(on)-240(model-theoretic)-237(ar)18(guments)-239(in-)]TJ 0 -9.37 Td[(accessible)-349(to)-349(nai)25(v)16(e)-350(users.)-349(This)-349(is)-349(in)-350(contrast)-348(to)-350(a)-350(structural)-348(sub-)]TJ 0 -9.37 Td[(sumption)-249(rule)-249(such)-249(as)]TJ/F47 5.98 Tf 91.14 4.01 Td[(A)]TJ/F50 5.98 Tf 5.53 0 Td[(v)]TJ/F47 5.98 Tf 5.75 0 Td[(B)]TJ ET 81.13 -205.01 36.6 0.38 re f 1 0 0 1 81.13 -210.11 cm BT /F50 5.98 Tf 0 0 Td[(8)]TJ/F47 5.98 Tf 4.21 0 Td[(r)33(:A)]TJ/F50 5.98 Tf 11.07 0 Td[(v8)]TJ/F47 5.98 Tf 9.96 0 Td[(r)33(:B)]TJ/F86 8.97 Tf 12.56 3.05 Td[(,)-250(which)-249(is)-249(self)-250(e)26(vident.)]TJ -130.89 -15.43 Td[(4.)-555(Proofs)-321(could,)-322(in)-322(general,)-321(be)-322(e)15(xponential)-321(in)-322(size.)-321(Ho)25(we)25(v)16(er)40(,)-322(based)]TJ 11.7 -9.37 Td[(on)-279(e)15(xperience)-278(with)-303(C)]TJ/F88 7.17 Tf 77.78 0 Td[(L)-61(A)-62(S)-62(S)-62(I)-62(C)]TJ/F86 8.97 Tf 27.14 0 Td[(,)-279(in)-279(e)16(xplaining)-278(a)-279(subsumption)-277(of)-279(the)]TJ -104.92 -9.37 Td[(form)]TJ/F70 8.97 Tf 20.05 0 Td[(A)]TJ/F71 8.97 Tf 10.17 0 Td[(v)]TJ/F70 8.97 Tf 10.43 0 Td[(C)]TJ/F71 8.97 Tf 9.54 0 Td[(u)]TJ/F70 8.97 Tf 8.48 0 Td[(D)]TJ/F86 8.97 Tf 7.85 0 Td[(,)-291(e)15(xperience)-289(with)-316(C)]TJ/F88 7.17 Tf 71.37 0 Td[(L)-61(A)-63(S)-61(S)-62(I)-62(C)]TJ/F86 8.97 Tf 29.75 0 Td[(suggests)-290(that)-290(users)]TJ -167.64 -9.37 Td[(often)-275(see)-276(one)-275(of)-275(the)-276(subsumptions)-273(\050)]TJ/F70 8.97 Tf 128.41 0 Td[(A)]TJ/F71 8.97 Tf 9.91 0 Td[(v)]TJ/F70 8.97 Tf 10.17 0 Td[(C)]TJ/F86 8.97 Tf 9.69 0 Td[(or)]TJ/F70 8.97 Tf 9.94 0 Td[(A)]TJ/F71 8.97 Tf 9.91 0 Td[(v)]TJ/F70 8.97 Tf 10.17 0 Td[(D)]TJ/F86 8.97 Tf 7.86 0 Td[(\051,)-275(and)-275(only)]TJ -196.06 -9.37 Td[(w)10(ant)-362(the)-362(other)-361(one)-362(e)16(xplained.)-361(Since)-361(the)-362(problem)-361(is)-362(in)-387(P)-49(S)]TJ/F88 7.17 Tf 213.94 0 Td[(P)29(A)-22(C)-62(E)]TJ/F86 8.97 Tf 18.94 0 Td[(,)]TJ -232.88 -9.37 Td[(this)-250(means)-249(that)-249(single)-249(branches)-248(are)-250(at)-249(most)-249(polynomial)-248(in)-250(size.)]TJ -0.74 -15.61 Td[(T)81(o)-319(resolv)16(e)-318(these)-317(problems)-317(we)-318(propose)-317(an)-318(approach)-317(based)-317(on)-318(the)]TJ -9.22 -9.37 Td[(follo)26(wing)-281(idea:)]TJ/F87 8.97 Tf 57.12 0 Td[(Eac)16(h)-281(pr)45(oof)-280(step)-281(in)-280(the)-281(sequent)-280(calculus)-279(is)-281(e)20(xpr)38(essed)]TJ -57.12 -9.37 Td[(in)-339(terms)-338(of)-339(zer)45(o)-339(or)-339(mor)38(e)-339(e)20(xplanation)-337(rules)-338(\050ERs\051)-339(to)-339(be)-338(intr)45(oduced,)]TJ 0 -9.37 Td[(plus)-249(some)-249(c)15(hoice)-249(on)-250(how)-249(to)-250(pr)46(oceed)-249(with)-249(the)-250(r)37(est)-249(of)-250(the)-249(e)20(xplanation.)]TJ/F86 8.97 Tf 9.22 -9.37 Td[(T)81(o)-326(be)-325(clear)41(,)-326(henceforth)-324(we)-325(will)-325(use)]TJ/F71 8.97 Tf 132.16 0 Td[(v)]TJ/F86 8.97 Tf 10.08 0 Td[(instead)-325(of)]TJ/F71 8.97 Tf 42.75 0 Td[(`)]TJ/F86 8.97 Tf 12.59 0 Td[(to)-325(indicate)]TJ -206.8 -9.37 Td[(the)-301(subsumption)-299(relationships)-300(that)-300(are)-301(being)-301(e)15(xplained,)-299(and)-301(refer)-301(to)]TJ 0 -9.37 Td[(the)-250(antecedent)-248(and)-249(succedent)-248(as)-250(lhs)-249(and)-249(rhs)-249(of)-250(the)-249(subsumption.)]TJ 9.22 -9.37 Td[(First,)-246(we)-246(mak)10(e)-246(conjunction)-245(and)-247(disjunction)-245(e)15(xplicit)-246(on)-246(the)-247(lhs)-246(and)]TJ -9.22 -9.37 Td[(rhs,)-306(replacing)-304(the)-306(commas.)-304(Ho)25(we)26(v)15(er)40(,)-306(we)-305(will)-306(lea)21(v)15(e)-306(implicit)-305(all)-305(ma-)]TJ 0 -9.37 Td[(nipulations)-229(relating)-230(to)-231(associati)26(vity)-230(and)-231(commutati)27(vity)-230(of)-231(these)-230(oper)20(-)]TJ 0 -9.37 Td[(ators.)-316(Therefore,)-315(sequent)-316(rules)-316(\050)]TJ/F70 8.97 Tf 116.44 0 Td[(l)]TJ/F71 8.97 Tf 2.9 0 Td[(^)]TJ/F86 8.97 Tf 6.14 0 Td[(\051)-317(and)-316(\050)]TJ/F70 8.97 Tf 24.61 0 Td[(r)]TJ/F71 8.97 Tf 4.41 0 Td[(_)]TJ/F86 8.97 Tf 6.14 0 Td[(\051)-317(will)-317(not)-316(appear)-316(in)-316(the)]TJ -160.64 -9.37 Td[(surf)10(ace)-249(e)15(xplanation.)]TJ 9.22 -9.37 Td[(Second,)-334(we)-336(introduce,)-334(in)-336(Figure)-334(3,)-336(a)-336(v)25(ariety)-335(of)-335(ERs)-335(that)-336(replace)]TJ -9.22 -9.37 Td[(concepts)-251(by)-252(equi)26(v)25(alent)-252(ones)-251(using,)-252(for)-252(e)16(xample,)-251(the)-252(f)10(amiliar)-251(rules)-252(of)]TJ 0 -9.37 Td[(de)-250(Mor)19(gan.)-244(These)-249(rules)-249(can)-250(be)-249(applied)-249(to)-249(concepts)-249(in)-249(proof)-249(steps.)]TJ 9.22 -9.37 Td[(Each)-235(of)-237(these)-235(rules)-236(has)-236(an)-236(English)-235(template)-235(describing)-235(its)-236(applica-)]TJ -9.22 -9.37 Td[(tion,)-264(and)-263(possibly)-263(a)-264(because)-263(clause,)-263(which)-263(the)-264(user)-264(may)-263(ask)-264(for)-264(in)]TJ 0 -9.37 Td[(order)-309(to)-310(e)15(xplain)-309(the)-309(rule)-309(itself.)-309(\050This)-309(should)-309(be)-310(unnecessary)67(,)-310(e)16(xcept)]TJ 0 -9.37 Td[(for)-304(one)-304(rule,)-304(mark)11(ed)-304(with)-304(*)-304(in)-304(Figure)-303(4,)-305(which)-303(may)-304(well)-304(be)-304(treated)]TJ 0 -9.37 Td[(as)-250(a)-249(lemma.\051)]TJ 9.22 -9.37 Td[(F)16(or)-231(the)-231(modal)-230(rules,)-230(we)-230(of)25(fer)-230(simpler)-230(v)25(ariants,)-230(which)-230(will)-230(be)-230(com-)]TJ -9.22 -9.37 Td[(bined)-296(with)-295(equi)25(v)26(alence)-296(rules)-295(\050when)-296(necessary\051)-294(to)-296(produce)-295(the)-296(same)]TJ 0 -9.37 Td[(ef)25(fect)-291(as)-292(the)-291(corresponding)-289(sequent)-291(rules.)-291(T)80(o)-291(be)15(gin)-291(with,)-291(\050)]TJ/F70 8.97 Tf 210.73 0 Td[(l)]TJ/F71 8.97 Tf 2.9 0 Td[(:)]TJ/F73 8.97 Tf 6.15 0 Td[(2)]TJ/F86 8.97 Tf 6.75 0 Td[(\051)-292(and)]TJ -226.53 -9.37 Td[(\050)]TJ/F70 8.97 Tf 2.99 0 Td[(r)]TJ/F71 8.97 Tf 4.41 0 Td[(:)]TJ/F73 8.97 Tf 6.15 0 Td[(3)]TJ/F86 8.97 Tf 7.12 0 Td[(\051)-239(are)-238(e)15(xplained)-237(as)-239(applications)-237(of)-238(de)-239(Mor)19(gan')61(s)-239(la)15(w)-238(follo)26(wed)-239(by)]TJ -20.67 -9.37 Td[(\050)]TJ/F70 8.97 Tf 2.99 0 Td[(l)]TJ/F73 8.97 Tf 2.9 0 Td[(3)]TJ/F86 8.97 Tf 7.12 0 Td[(\051)-242(or)-242(\050)]TJ/F70 8.97 Tf 17.79 0 Td[(r)]TJ/F73 8.97 Tf 4.41 0 Td[(2)]TJ/F86 8.97 Tf 6.76 0 Td[(\051)-242(respecti)26(v)15(ely)66(.)-242(Then,)-242(the)-241(\050)]TJ/F97 8.97 Tf 90.91 0 Td[(AndAll)]TJ/F86 8.97 Tf 26.24 0 Td[(\051)-242(and)-242(\050)]TJ/F97 8.97 Tf 23.26 0 Td[(OrSome)]TJ/F86 8.97 Tf 31.1 0 Td[(\051)-242(equi)25(v)26(a-)]TJ -213.48 -9.37 Td[(lences)-247(can)-247(be)-248(used)-247(to)-247(gather)-242(together)-247(rele)26(v)25(ant)-247(components)-246(on)-248(the)-247(lhs)]TJ 0 -9.37 Td[(and)-208(rhs.)-207(Finally)66(,)-208(the)-208(subsumption)-205(can)-208(be)-208(e)15(xplained)-206(using)-207(the)-208(\050mostly\051)]TJ 0 -9.37 Td[(structural)-249(rules)-249(gi)26(v)15(en)-250(in)-249(Figure)-249(4.)]TJ 9.22 -9.37 Td[(W)81(e)-366(are)-366(no)25(w)-366(ready)-365(to)-366(sk)11(etch)-366(the)-366(proof)-365(e)15(xplanation)-364(function)]TJ/F106 8.97 Tf 222.41 0 Td[(Ex-)]TJ -231.63 -9.37 Td[(plain)]TJ/F86 8.97 Tf 19.09 0 Td[(\050)]TJ/F71 8.97 Tf 2.98 0 Td[()]TJ/F86 8.97 Tf 2.56 0 Td[(,)]TJ/F71 8.97 Tf 4.82 0 Td[()]TJ/F86 8.97 Tf 2.56 0 Td[(\051,)-287(which,)-286(gi)25(v)16(en)-287(the)-287(subsumption)]TJ/F70 8.97 Tf 118.62 0 Td[()]TJ/F71 8.97 Tf 9.11 0 Td[(v)]TJ/F70 8.97 Tf 10.36 0 Td[(\014)]TJ/F86 8.97 Tf 8.24 0 Td[(and)-286(its)-287(proof,)-286(gen-)]TJ -178.34 -9.37 Td[(erates)-219(some)-218(te)15(xt,)-219(possibly)-218(of)25(fering)-219(further)-218(sub-e)16(xplanation\050s\051.)-218(Again,)]TJ 0 -9.37 Td[(we)-222(consider)-221(a)-222(v)25(ariety)-222(of)-222(sequent)-221(rule)-222(kinds)-221(to)-222(illustrate)-221(our)-222(approach.)]TJ 9.22 -9.37 Td[(F)16(or)-437(a)-437(termination)-436(sequent)-436(rule)-436(such)-437(as)]TJ/F15 8.97 Tf 150.33 0 Td[(\050=\051)]TJ/F86 8.97 Tf 14.34 0 Td[(,)]TJ/F106 8.97 Tf 6.16 0 Td[(Explain)]TJ/F86 8.97 Tf 29.55 0 Td[(\050)]TJ/F70 8.97 Tf 2.98 0 Td[()]TJ/F71 8.97 Tf 11.67 0 Td[(v)]TJ/F70 8.97 Tf 12.93 0 Td[(\014)]TJ/F86 8.97 Tf 5.66 0 Td[(,)]TJ/F97 8.97 Tf -242.84 -9.36 Td[(ident)]TJ/F15 8.97 Tf 19.15 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(Z)]TJ/F15 8.97 Tf 6.91 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(\051)-385(w)10(ould)-384(say:)]TJ/F87 8.97 Tf 50.12 0 Td[(The)-385(subsumption)-383(now)-384(follows)-384(because)-384(the)]TJ -83.34 -9.37 Td[(description)-306(Z)-307(is)-307(subsumed)-306(by)-307(Z,)-307(*and)-307(the)-307(lhs)-307(is)-307(a)-307(constriction)-306(of)-307(Z,)]TJ 0 -9.37 Td[(since)-274(it)-275(is)-275(a)-274(conjunction,)-273(while)-274(**the)-274(rhs)-275(is)-274(an)-275(e)20(xpansion)-273(of)-275(Z,)-274(since)]TJ 0 -9.37 Td[(it)-273(is)-273(a)-273(disjunction)]TJ/F86 8.97 Tf 67.64 0 Td[(.)-274(The)-272(sentence)-272(fragment)-272(starting)-272(at)-273(*)-273(\050resp.)-272(**\051)-273(is)]TJ -67.64 -9.37 Td[(omitted)-249(if)]TJ/F70 8.97 Tf 37.36 0 Td[()]TJ/F86 8.97 Tf 8.16 0 Td[(\050resp.)]TJ/F70 8.97 Tf 22.41 0 Td[(\014)]TJ/F86 8.97 Tf 5.66 0 Td[(\051)-249(is)-250(a)-250(singleton)-248(rather)-249(than)-249(a)-250(conjunct.)]TJ -64.37 -9.37 Td[(Ne)16(xt,)-318(consider)-317(an)-318(equi)25(v)26(alence)-318(rule,)-317(lik)10(e)]TJ/F15 8.97 Tf 147.43 0 Td[(\050)]TJ/F70 8.97 Tf 3.59 0 Td[(l)]TJ/F71 8.97 Tf 2.9 0 Td[(::)]TJ/F15 8.97 Tf 12.28 0 Td[(\051)]TJ/F86 8.97 Tf 3.59 0 Td[(.)]TJ/F106 8.97 Tf 5.09 0 Td[(Explain)]TJ/F86 8.97 Tf 29.55 0 Td[(\050)]TJ/F70 8.97 Tf 2.99 0 Td[()]TJ/F71 8.97 Tf 9.64 0 Td[(v)]TJ/F70 8.97 Tf 10.9 0 Td[(\014)]TJ/F86 8.97 Tf 5.66 0 Td[(,)]TJ/F97 8.97 Tf -242.84 -9.37 Td[(lNotNot)]TJ/F15 8.97 Tf 31.11 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(Z)-14(;)]TJ/F101 8.97 Tf 10.49 0 Td[(Pf)]TJ/F15 8.97 Tf 10.98 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(\051)-221(produces:)]TJ/F87 8.97 Tf 41.81 0 Td[(Double)-219(ne)41(gation)-220(elimination)-219(on)-220(the)-220(lhs)]TJ -101.55 -9.37 Td[(leaves)-249(Z)]TJ/F86 8.97 Tf 34.62 0 Td[(.)]TJ 237.61 662.26 Td[(As)-358(promised,)-356(rules)-358(\050)]TJ/F70 8.97 Tf 75.63 0 Td[(l)]TJ/F71 8.97 Tf 2.9 0 Td[(^)]TJ/F86 8.97 Tf 6.14 0 Td[(\051)-359(and)-357(\050)]TJ/F70 8.97 Tf 25.35 0 Td[(r)]TJ/F71 8.97 Tf 4.41 0 Td[(_)]TJ/F86 8.97 Tf 6.15 0 Td[(\051)-358(are)-358(not)-357(e)15(xplicitly)-357(reported,)-357(so)]TJ -129.8 -9.37 Td[(that)]TJ/F106 8.97 Tf 15.44 0 Td[(Explain)]TJ/F86 8.97 Tf 29.55 0 Td[(\050)]TJ/F70 8.97 Tf 2.98 0 Td[()]TJ/F71 8.97 Tf 8.48 0 Td[(v)]TJ/F70 8.97 Tf 9.72 0 Td[(\014)]TJ/F86 8.97 Tf 5.66 0 Td[(,)]TJ/F97 8.97 Tf 4.23 0 Td[(lAnd)]TJ/F15 8.97 Tf 17.88 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(A;)-172(B)-50(;)]TJ/F101 8.97 Tf 22.52 0 Td[(Pf)]TJ/F15 8.97 Tf 10.98 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(\051)-221(just)-221(in)40(v)21(ok)10(es)]TJ/F106 8.97 Tf 49.16 0 Td[(Explain)]TJ/F86 8.97 Tf 29.55 0 Td[(\050)]TJ/F70 8.97 Tf 2.99 0 Td[()]TJ/F50 5.98 Tf 5.91 3.81 Td[(0)]TJ/F71 8.97 Tf 5.24 -3.81 Td[(v)]TJ/F70 8.97 Tf 9.73 0 Td[(\014)]TJ/F86 8.97 Tf 5.66 0 Td[(,)]TJ/F101 8.97 Tf -242.84 -10.37 Td[(Pf)]TJ/F86 8.97 Tf 10.98 0 Td[(\051,)-233(where)]TJ/F70 8.97 Tf 31.32 0 Td[()]TJ/F50 5.98 Tf 5.92 3.81 Td[(0)]TJ/F86 8.97 Tf 4.78 -3.81 Td[(may)-233(ha)21(v)15(e)-234(conjunction)-232(nesting)-232(remo)16(v)15(ed)-233(from)]TJ/F70 8.97 Tf 161.41 0 Td[()]TJ/F86 8.97 Tf 5.91 0 Td[(.)-234(Rules)]TJ -220.32 -9.37 Td[(\050)]TJ/F70 8.97 Tf 2.99 0 Td[(l)]TJ/F71 8.97 Tf 2.9 0 Td[(_)]TJ/F86 8.97 Tf 6.14 0 Td[(\051)-281(and)-281(\050)]TJ/F70 8.97 Tf 23.97 0 Td[(r)]TJ/F71 8.97 Tf 4.41 0 Td[(^)]TJ/F86 8.97 Tf 6.15 0 Td[(\051)-281(represent)-279(case)-281(analysis,)-280(and)-280(of)25(fer)-281(the)-281(user)-280(a)-281(choice)-280(of)]TJ -46.56 -9.37 Td[(which)-354(branch)-353(of)-354(the)-353(proof)-354(to)-354(follo)26(w)-354(\050or)-354(stacks)-353(the)-354(proofs)-353(for)-353(both)]TJ 0 -9.37 Td[(cases\051.)]TJ 9.22 -9.37 Td[(Finally)66(,)-250(we)-249(come)-249(to)-250(modal)-248(rules.)-499(Let)-250(us)-249(consider)]TJ/F106 8.97 Tf 1.77 -17.99 Td[(Explain)]TJ/F86 8.97 Tf 29.54 0 Td[(\050)]TJ/F70 8.97 Tf 2.99 0 Td[()]TJ/F71 8.97 Tf 8.47 0 Td[(v)]TJ/F70 8.97 Tf 9.73 0 Td[(\014)]TJ/F86 8.97 Tf 5.66 0 Td[(,)]TJ/F97 8.97 Tf 4.48 0 Td[(lSome)]TJ/F15 8.97 Tf 23.35 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(r)29(;)-172(B)-50(;)]TJ/F15 8.97 Tf 19.51 0 Td[([)]TJ/F70 8.97 Tf 2.56 0 Td[(La)]TJ/F15 8.97 Tf 11.16 0 Td[(1)]TJ/F70 8.97 Tf 4.6 0 Td[(;)-172(Lns)]TJ/F15 8.97 Tf 20.22 0 Td[(1)]TJ/F70 8.97 Tf 4.61 0 Td[(;)-172(Rs)]TJ/F15 8.97 Tf 15.42 0 Td[(1)]TJ/F70 8.97 Tf 4.61 0 Td[(;)-172(Rna)]TJ/F15 8.97 Tf 21.57 0 Td[(1])]TJ/F70 8.97 Tf 7.17 0 Td[(;)]TJ/F101 8.97 Tf 4.1 0 Td[(Pf)]TJ/F15 8.97 Tf 10.97 0 Td[(\051)]TJ/F86 8.97 Tf 3.59 0 Td[(\051.)]TJ -228.88 -17.98 Td[(If)]TJ/F70 8.97 Tf 12.05 0 Td[(Lns)]TJ/F15 8.97 Tf 16.13 0 Td[(1)]TJ/F86 8.97 Tf 10.68 0 Td[(is)-678(not)-677(empty)66(,)-677(then)-677(we)-677(rst)-677(apply)-677(equi)26(v)25(alence)-676(rule)]TJ/F15 8.97 Tf -38.86 -9.37 Td[(\050)]TJ/F97 8.97 Tf 3.59 0 Td[(NotSome)]TJ/F15 8.97 Tf 35.59 0 Td[(\051)]TJ/F86 8.97 Tf 6.71 0 Td[(to)-349(the)-348(elements)-347(of)]TJ/F70 8.97 Tf 69.79 0 Td[()]TJ/F86 8.97 Tf 9.04 0 Td[(which)-347(appear)-348(in)]TJ/F71 8.97 Tf 62.16 0 Td[(f:9)]TJ/F70 8.97 Tf 15.87 0 Td[(r)29(:C)]TJ/F71 8.97 Tf 17.93 0 Td[(j)]TJ/F70 8.97 Tf 6.8 0 Td[(C)]TJ/F71 8.97 Tf 11.46 0 Td[(2)]TJ/F70 8.97 Tf -238.94 -9.37 Td[(Lns)]TJ/F15 8.97 Tf 16.13 0 Td[(1)]TJ/F71 8.97 Tf 4.6 0 Td[(g)]TJ/F86 8.97 Tf 4.61 0 Td[(.)-387(Similarly)-386(for)]TJ/F70 8.97 Tf 56.5 0 Td[(Rna)]TJ/F15 8.97 Tf 17.48 0 Td[(1)]TJ/F86 8.97 Tf 4.61 0 Td[(.)-387(This)-386(lea)20(v)15(es)-387(us)-387(an)-386(e)15(xplanation)-386(of)-387(the)]TJ -103.93 -9.37 Td[(form)]TJ/F106 8.97 Tf 19.84 0 Td[(Explain)]TJ/F86 8.97 Tf 29.55 0 Td[(\050)]TJ/F70 8.97 Tf 2.99 0 Td[()]TJ/F71 8.97 Tf 8.78 0 Td[(v)]TJ/F70 8.97 Tf 10.04 0 Td[(\014)]TJ/F86 8.97 Tf 5.66 0 Td[(,)]TJ/F97 8.97 Tf 4.65 0 Td[(lSome)]TJ/F15 8.97 Tf 23.34 0 Td[(\050)]TJ/F70 8.97 Tf 3.59 0 Td[(r)29(;)-171(B)-51(;)]TJ/F15 8.97 Tf 19.51 0 Td[([)]TJ/F70 8.97 Tf 2.56 0 Td[(La)]TJ/F15 8.97 Tf 11.15 0 Td[(2)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(;)]TJ/F70 8.97 Tf 4.6 0 Td[(;)-172(Rs)]TJ/F15 8.97 Tf 15.43 0 Td[(2)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F71 8.97 Tf 4.09 0 Td[(;)]TJ/F15 8.97 Tf 4.61 0 Td[(])]TJ/F70 8.97 Tf 2.56 0 Td[(;)]TJ/F101 8.97 Tf 4.1 0 Td[(Pf)]TJ/F15 8.97 Tf 10.97 0 Td[(\051)]TJ/F86 8.97 Tf 3.59 0 Td[(\051.)-267(If)]TJ/F70 8.97 Tf 16.01 0 Td[(La)]TJ/F15 8.97 Tf 11.15 0 Td[(2)]TJ/F86 8.97 Tf 7.01 0 Td[(is)]TJ -239.1 -9.37 Td[(non-empty)66(,)-339(then)-340(we)-339(apply)-339(equi)26(v)25(alence)-339(rules)]TJ/F15 8.97 Tf 164.42 0 Td[(\050)]TJ/F97 8.97 Tf 3.59 0 Td[(AndAll)]TJ/F15 8.97 Tf 26.23 0 Td[(\051)]TJ/F86 8.97 Tf 6.63 0 Td[(\050unless)]TJ/F70 8.97 Tf 28.45 0 Td[(La)]TJ/F15 8.97 Tf 11.16 0 Td[(2)]TJ/F86 8.97 Tf -240.48 -9.37 Td[(is)-305(a)-304(singleton\051)-303(and)]TJ/F15 8.97 Tf 69.71 0 Td[(\050)]TJ/F97 8.97 Tf 3.58 0 Td[(SomeAndAll)]TJ/F15 8.97 Tf 47.38 0 Td[(\051)]TJ/F86 8.97 Tf 6.32 0 Td[(to)-304(the)-305(subsumee)-303(to)-304(gather)-299(the)]TJ/F71 8.97 Tf 109.99 0 Td[(8)]TJ/F86 8.97 Tf 5.12 0 Td[(-)]TJ -242.1 -9.37 Td[(restrictions)-227(and)-229(absorb)-227(them)-228(into)]TJ/F71 8.97 Tf 118.85 0 Td[(9)]TJ/F70 8.97 Tf 5.11 0 Td[(r)28(:B)]TJ/F86 8.97 Tf 13.89 0 Td[(.)-228(This)-228(lea)20(v)15(es)-228(us)-228(with)-228(an)-229(e)15(xpla-)]TJ -137.85 -9.37 Td[(nation)-238(of)-238(the)-237(form)]TJ/F106 8.97 Tf 66.82 0 Td[(Explain)]TJ/F86 8.97 Tf 29.55 0 Td[(\050)]TJ/F70 8.97 Tf 2.99 0 Td[()]TJ/F71 8.97 Tf 8.47 0 Td[(v)]TJ/F70 8.97 Tf 9.73 0 Td[(\014)]TJ/F86 8.97 Tf 5.66 0 Td[(,)]TJ/F97 8.97 Tf 4.38 0 Td[(lSome)]TJ/F15 8.97 Tf 23.34 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(r)29(;)-172(B)-50(;)]TJ/F15 8.97 Tf 19.52 0 Td[([)]TJ/F71 8.97 Tf 2.56 0 Td[(;)]TJ/F70 8.97 Tf 4.6 0 Td[(;)]TJ/F71 8.97 Tf 4.1 0 Td[(;)]TJ/F70 8.97 Tf 4.61 0 Td[(;)-171(Rs)]TJ/F15 8.97 Tf 15.42 0 Td[(2)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F71 8.97 Tf 4.09 0 Td[(;)]TJ/F15 8.97 Tf 4.61 0 Td[(])]TJ/F70 8.97 Tf 2.56 0 Td[(;)]TJ/F101 8.97 Tf 4.1 0 Td[(Pf)]TJ/F15 8.97 Tf 10.97 0 Td[(\051)]TJ/F86 8.97 Tf 3.59 0 Td[(\051.)]TJ -239.86 -9.37 Td[(If)]TJ/F70 8.97 Tf 8.55 0 Td[(Rs)]TJ/F15 8.97 Tf 11.33 0 Td[(2)]TJ/F86 8.97 Tf 7.18 0 Td[(contains)-285(more)-286(than)-286(one)-286(element,)-286(the)16(y)-287(can)-286(be)-287(gathered)-280(into)-286(a)]TJ -27.06 -9.37 Td[(single)]TJ/F71 8.97 Tf 24.55 0 Td[(9)]TJ/F86 8.97 Tf 5.12 0 Td[(-restriction)-348(using)-348(the)]TJ/F15 8.97 Tf 79.13 0 Td[(\050)]TJ/F97 8.97 Tf 3.58 0 Td[(OrSome)]TJ/F15 8.97 Tf 31.1 0 Td[(\051)]TJ/F86 8.97 Tf 6.71 0 Td[(equi)26(v)25(alence)-348(rule.)-348(W)80(e)-349(no)26(w)]TJ -150.19 -9.37 Td[(ha)20(v)15(e)-250(tw)11(o)-250(cases)]TJ/F71 8.97 Tf 0.38 -13.59 Td[()]TJ/F70 8.97 Tf 9.59 0 Td[(Rs)]TJ/F15 8.97 Tf 11.33 0 Td[(2)]TJ/F86 8.97 Tf 8.74 0 Td[(is)-460(the)-460(empty)-460(set.)-460(In)-460(this)-460(case)-460(the)-460(subsumee)-459(must)-460(be)-460(in-)]TJ -20.07 -9.37 Td[(coherent,)-500(so)-502(we)-502(say:)]TJ/F87 8.97 Tf 84 0 Td[(T)92(o)-502(pr)45(o)11(ve)-502(that)]TJ/F70 8.97 Tf 61.02 0 Td[()]TJ/F71 8.97 Tf 12.78 0 Td[(v)]TJ/F70 8.97 Tf 14.04 0 Td[(\014)]TJ/F87 8.97 Tf 5.66 0 Td[(,)-502(we)-502(will)-502(show)]TJ -177.5 -9.37 Td[(that)]TJ/F71 8.97 Tf 17.5 0 Td[(9)]TJ/F70 8.97 Tf 5.12 0 Td[(r)29(:B)]TJ/F87 8.97 Tf 17.43 0 Td[(is)-395(incoher)38(ent,)-395(and)-395(hence)-395(is)-395(subsumed)-394(by)-395(e)15(verything)17(.)]TJ -40.05 -9.37 Td[(F)106(or)-454(this,)-452(it)-454(is)-453(suf)19(cient)-453(to)-453(show)-453(that)]TJ/F70 8.97 Tf 142.79 0 Td[(B)]TJ/F87 8.97 Tf 11.48 0 Td[(is)-454(incoher)39(ent.)140()]TJ/F86 8.97 Tf 54.04 0 Td[(.)-453(If)-454(we)]TJ -208.31 -9.37 Td[(w)11(anted,)-288(we)-287(could)-287(no)25(w)-288(introduce)-286(a)-288(v)25(ariant)-287(of)]TJ/F106 8.97 Tf 164.31 0 Td[(Explain)]TJ/F86 8.97 Tf 29.54 0 Td[(\050)]TJ/F71 8.97 Tf 2.99 0 Td[()]TJ/F86 8.97 Tf 2.56 0 Td[(,)]TJ/F71 8.97 Tf 4.83 0 Td[()]TJ/F86 8.97 Tf 2.56 0 Td[(\051,)-287(call)-288(it)]TJ/F97 8.97 Tf -206.79 -9.37 Td[(ExplainIncoherent)]TJ/F15 8.97 Tf 68.35 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(B)-51(;)]TJ/F101 8.97 Tf 11.52 0 Td[(Pf)]TJ/F15 8.97 Tf 10.98 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(,)-303(which)-302(kno)26(ws)-302(that)-303(the)-302(proof)]TJ/F101 8.97 Tf 107.47 0 Td[(Pf)]TJ/F86 8.97 Tf 13.69 0 Td[(only)]TJ -219.17 -9.37 Td[(deals)-306(with)-307(the)-307(lhs,)-307(since)-307(it)-307(had)-307(an)-307(empty)-307(rele)26(v)25(ant)-307(rhs.)-307(Or)-307(we)-307(can)]TJ 0 -9.37 Td[(continue)-248(with)]TJ/F106 8.97 Tf 51.3 0 Td[(Explain)]TJ/F86 8.97 Tf 29.55 0 Td[(\050)]TJ/F70 8.97 Tf 2.99 0 Td[(B)]TJ/F71 8.97 Tf 9.98 0 Td[(v)-285(?)]TJ/F86 8.97 Tf 16.89 0 Td[(,)]TJ/F101 8.97 Tf 4.48 0 Td[(Pf)]TJ/F86 8.97 Tf 10.98 0 Td[(\051.)]TJ/F71 8.97 Tf -135.76 -13.66 Td[()]TJ/F70 8.97 Tf 9.59 0 Td[(Rs)]TJ/F15 8.97 Tf 11.33 0 Td[(2)]TJ/F86 8.97 Tf 9.48 0 Td[(contains)-541(a)-544(single)-542(concept)]TJ/F70 8.97 Tf 102.66 0 Td[(C)]TJ/F86 8.97 Tf 7.22 0 Td[(.)-543(In)-543(this)-542(case,)-543(we)-542(can)-543(use)]TJ/F15 8.97 Tf -130.69 -9.37 Td[(\050)]TJ/F97 8.97 Tf 3.58 0 Td[(StructSome)]TJ/F15 8.97 Tf 44.92 0 Td[(\051)]TJ/F86 8.97 Tf 6.36 0 Td[(to)-309(pro)16(vide)-309(a)-309(simple)-308(e)15(xplanation:)]TJ/F87 8.97 Tf 120.19 0 Td[(*The)-309(subsump-)]TJ -175.05 -9.37 Td[(tion)-309(can)-309(now)-309(be)-309(pr)46(o)10(ven)-309(by)-310(showing)-308(that)]TJ/F71 8.97 Tf 149.24 0 Td[(9)]TJ/F87 8.97 Tf 5.12 0 Td[(-r)37(estrictions)-308(for)-309(r)45(ole)]TJ/F70 8.97 Tf 76.34 0 Td[(r)]TJ/F87 8.97 Tf -230.7 -9.37 Td[(subsume)17(.)-246(T)92(o)-245(pr)45(o)10(ve)]TJ/F71 8.97 Tf 68.16 0 Td[(9)]TJ/F70 8.97 Tf 5.12 0 Td[(r)29(:X)]TJ/F71 8.97 Tf 17.34 0 Td[(v)-285(9)]TJ/F70 8.97 Tf 14.85 0 Td[(r)29(:Y)]TJ/F87 8.97 Tf 13.86 0 Td[(,)-245(it)-246(is)-245(suf)18(cient)-245(to)-245(pr)45(o)11(ve)]TJ/F70 8.97 Tf 85.55 0 Td[(X)]TJ/F71 8.97 Tf 10.87 0 Td[(v)]TJ/F70 8.97 Tf 9.73 0 Td[(Y)]TJ/F87 8.97 Tf 7.39 0 Td[(.)]TJ -232.87 -9.37 Td[(So)-374(in)-374(this)-375(case)-374(we)-374(ar)37(e)-374(r)37(educed)-374(to)-374(showing)]TJ/F70 8.97 Tf 162.08 0 Td[(B)]TJ/F71 8.97 Tf 12.11 0 Td[(v)]TJ/F70 8.97 Tf 11.86 0 Td[(C)]TJ/F87 8.97 Tf 7.22 0 Td[()]TJ/F86 8.97 Tf 4.99 0 Td[(.)-374(The)-374(rst)]TJ -198.26 -9.37 Td[(sentence)-248(is)-250(omitted)-248(if)]TJ/F70 8.97 Tf 78.69 0 Td[()]TJ/F86 8.97 Tf 8.16 0 Td[(has)-249(no)-250(conjuncts.)]TJ -87.6 -19.6 Td[(Returning)-248(to)-250(our)-249(original)-249(e)15(xample,)-248(we)-250(were)-249(ask)11(ed)-250(to)-249(e)15(xplain)]TJ/F15 8.97 Tf -9.22 -13.69 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(>)-228(u)-229(8)]TJ/F78 8.97 Tf 22.53 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F15 8.97 Tf 6.14 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F71 8.97 Tf 32.85 0 Td[(t)-228(9)]TJ/F78 8.97 Tf 13.31 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051)]TJ/F49 7.97 Tf -228.47 -9.17 Td[(v)]TJ/F15 8.97 Tf 8.94 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.25 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051\051)]TJ/F46 7.97 Tf 10.75 0 Td[(;)]TJ/F86 8.97 Tf -166.85 -14.01 Td[(The)-1676(\050pruned\051)-1674(sequent)-1675(proof)-1675(is)-1675(constructed)-1674(with)]TJ/F97 8.97 Tf 0 -9.37 Td[(lAnd)]TJ/F70 8.97 Tf 17.88 0 Td[(;)]TJ/F97 8.97 Tf 4.1 0 Td[(lSome)]TJ/F70 8.97 Tf 23.34 0 Td[(;)]TJ/F97 8.97 Tf 4.1 0 Td[(lNotOr)]TJ/F70 8.97 Tf 26.73 0 Td[(;)]TJ/F97 8.97 Tf 4.1 0 Td[(rAll)]TJ/F70 8.97 Tf 13.7 0 Td[(;)]TJ/F97 8.97 Tf 4.1 0 Td[(lNotNot)]TJ/F70 8.97 Tf 31.1 0 Td[(;)]TJ/F97 8.97 Tf 4.1 0 Td[(rOr)]TJ/F86 8.97 Tf 22.04 0 Td[(and)]TJ/F97 8.97 Tf 21.75 0 Td[(ident)]TJ/F86 8.97 Tf 19.15 0 Td[(.)-982(According)]TJ -196.19 -9.37 Td[(to)-264(our)-264(rules,)-263(we)-264(skip)]TJ/F97 8.97 Tf 75.85 0 Td[(lAnd)]TJ/F86 8.97 Tf 17.88 0 Td[(,)-264(and)-264(e)15(xplain)]TJ/F97 8.97 Tf 48.56 0 Td[(lSome)]TJ/F86 8.97 Tf 23.34 0 Td[(,)-264(which)-264(here)-263(uses)-264(ERs)]TJ/F15 8.97 Tf -165.63 -9.37 Td[(\050)]TJ/F97 8.97 Tf 3.59 0 Td[(SomeAndAll)]TJ/F15 8.97 Tf 47.38 0 Td[(\051)]TJ/F86 8.97 Tf 5.82 0 Td[(and)]TJ/F15 8.97 Tf 15.19 0 Td[(\050)]TJ/F97 8.97 Tf 3.58 0 Td[(StructSome)]TJ/F15 8.97 Tf 44.92 0 Td[(\051)]TJ/F86 8.97 Tf 3.59 0 Td[(.)-250(These)-249(generate)-248(the)-249(te)15(xt)]TJ/F87 8.97 Tf -114.1 -13.59 Td[(On)-1274(the)-1274(lhs,)]TJ/F71 8.97 Tf 80.36 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(>)]TJ/F87 8.97 Tf 18.6 0 Td[(can)-1274(be)-1275(str)38(engthened)]TJ -134.88 -9.37 Td[(with)]TJ/F71 8.97 Tf 29.68 0 Td[(8)]TJ/F87 8.97 Tf 5.12 0 Td[(-r)37(estrictions)-1586(on)-1586(r)45(ole)]TJ/F78 8.97 Tf 109.23 0 Td[(friend)]TJ/F87 8.97 Tf 42.48 0 Td[(to)-1587(yield)]TJ/F71 8.97 Tf -186.51 -9.37 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(>)-479(u)-478(:)]TJ/F15 8.97 Tf 28.04 0 Td[(\050\050)]TJ/F71 8.97 Tf 7.16 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.14 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051)]TJ/F71 8.97 Tf 5.63 0 Td[(t)]TJ/F15 8.97 Tf 8.19 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.24 0 Td[(\051\051\051)]TJ/F86 8.97 Tf 10.76 0 Td[(.)]TJ/F87 8.97 Tf -227.93 -9.37 Td[(The)-742(subsumption)-740(can)-743(now)-742(be)-742(pr)45(o)11(ven)-743(by)-742(showing)-741(that)]TJ/F71 8.97 Tf 0 -9.36 Td[(9)]TJ/F87 8.97 Tf 5.12 0 Td[(-r)38(estrictions)-1155(for)-1156(r)46(ole)]TJ/F78 8.97 Tf 99.12 0 Td[(friend)]TJ/F87 8.97 Tf 38.62 0 Td[(subsume)17(.)-1156(T)92(o)-1156(pr)45(o)10(ve)]TJ/F71 8.97 Tf -142.86 -9.37 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:X)]TJ/F71 8.97 Tf 22.46 0 Td[(v)-1293(9)]TJ/F78 8.97 Tf 23.88 0 Td[(friend)]TJ/F70 8.97 Tf 28.24 0 Td[(:Y)]TJ/F87 8.97 Tf 9.96 0 Td[(,)-779(it)-778(is)-779(suf)19(cient)-778(to)-779(pr)46(o)10(ve)]TJ/F70 8.97 Tf -117.9 -9.37 Td[(X)]TJ/F71 8.97 Tf 18.51 0 Td[(v)]TJ/F70 8.97 Tf 17.36 0 Td[(Y)]TJ/F87 8.97 Tf 7.4 0 Td[(.)-697(So)-697(in)-697(this)-696(case)-697(we)-696(ar)37(e)-697(r)37(educed)-696(to)-697(show-)]TJ -43.27 -9.37 Td[(ing)]TJ/F71 8.97 Tf 19.51 0 Td[(>)-479(u)-478(:)]TJ/F15 8.97 Tf 28.04 0 Td[(\050\050)]TJ/F71 8.97 Tf 7.17 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(:)]TJ/F78 8.97 Tf 6.15 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F71 8.97 Tf 5.63 0 Td[(t)]TJ/F15 8.97 Tf 8.19 0 Td[(\050)]TJ/F71 8.97 Tf 3.59 0 Td[(9)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F78 8.97 Tf 2.56 0 Td[(Lawyer)]TJ/F15 8.97 Tf 28.25 0 Td[(\051\051)]TJ/F71 8.97 Tf 20.79 0 Td[(v)]TJ -217.98 -9.37 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.87 0 Td[(t)]TJ/F78 8.97 Tf 8.2 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(.)]TJ -105.66 -13.59 Td[(F)15(or)]TJ/F97 8.97 Tf 15.28 0 Td[(rAll)]TJ/F15 8.97 Tf 13.71 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(;)]TJ/F15 8.97 Tf 4.09 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.87 0 Td[(t)]TJ/F78 8.97 Tf 8.2 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F70 8.97 Tf 3.58 0 Td[(;)]TJ/F15 8.97 Tf 4.1 0 Td[([)]TJ/F71 8.97 Tf 2.56 0 Td[(;)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F71 8.97 Tf 4.09 0 Td[(f:)]TJ/F78 8.97 Tf 10.75 0 Td[(Doctor)]TJ/F71 8.97 Tf 28.25 0 Td[(g)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F71 8.97 Tf 4.09 0 Td[(;)]TJ/F70 8.97 Tf 4.61 0 Td[(;)]TJ/F71 8.97 Tf 4.09 0 Td[(;)]TJ/F15 8.97 Tf 4.61 0 Td[(])]TJ/F70 8.97 Tf 2.56 0 Td[(;)]TJ ET 379.91 -300.66 2.69 0.4 re f 1 0 0 1 382.6 -300.66 cm BT /F15 8.97 Tf 0 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(,)-330(we)-329(use)]TJ -214.52 -9.37 Td[(ERs)]TJ/F15 8.97 Tf 18.01 0 Td[(\050)]TJ/F97 8.97 Tf 3.58 0 Td[(NotSome)]TJ/F15 8.97 Tf 35.6 0 Td[(\051)]TJ/F86 8.97 Tf 6.63 0 Td[(\050combined)-339(with)-340(the)-340(preceding)]TJ/F15 8.97 Tf 112.82 0 Td[(\050)]TJ/F97 8.97 Tf 3.59 0 Td[(NotOr)]TJ/F15 8.97 Tf 24.53 0 Td[(\051)]TJ/F86 8.97 Tf 3.59 0 Td[(,)-340(and)-340(then)]TJ/F15 8.97 Tf -208.35 -9.37 Td[(\050)]TJ/F97 8.97 Tf 3.59 0 Td[(StructAll)]TJ/F15 8.97 Tf 34.33 0 Td[(\051)]TJ/F86 8.97 Tf 5.83 0 Td[(to)-250(get)]TJ/F87 8.97 Tf -33.78 -13.59 Td[(On)-207(the)-207(lhs,)-207(apply)-206(de)-207(Mor)37(gan')41(s)-207(laws)-207(to)-207(pr)45(opa)11(gate)-207(in)-207(ne)40(gation,)-206(to)]TJ 0 -9.37 Td[(g)11(et)]TJ/F15 8.97 Tf 15.63 0 Td[(\050)]TJ/F71 8.97 Tf 3.58 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F71 8.97 Tf 2.56 0 Td[(::)]TJ/F78 8.97 Tf 12.28 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(.)]TJ/F87 8.97 Tf 4.55 0 Td[(T)93(o)-257(pr)46(o)10(ve)]TJ/F71 8.97 Tf 33.16 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:X)]TJ/F71 8.97 Tf 13.55 0 Td[(v)-298(8)]TJ/F78 8.97 Tf 14.96 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:Y)]TJ/F87 8.97 Tf 9.96 0 Td[(,)]TJ -222.91 -9.37 Td[(it)-281(is)-281(suf)19(cient)-281(to)-281(show)]TJ/F70 8.97 Tf 81.21 0 Td[(X)]TJ/F71 8.97 Tf 11.41 0 Td[(v)]TJ/F70 8.97 Tf 10.26 0 Td[(Y)]TJ/F87 8.97 Tf 7.4 0 Td[(.)-281(So)-281(in)-281(this)-281(case)-281(we)-281(ar)38(e)-282(r)38(educed)]TJ -110.28 -9.37 Td[(to)-249(showing)]TJ/F71 8.97 Tf 41.35 0 Td[(::)]TJ/F78 8.97 Tf 12.29 0 Td[(Doctor)]TJ/F71 8.97 Tf 30.8 0 Td[(v)]TJ/F15 8.97 Tf 9.73 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F86 8.97 Tf 3.59 0 Td[(.)]TJ -168.62 -13.59 Td[(\050Note)-217(that)]TJ/F71 8.97 Tf 37.77 0 Td[(:9)]TJ/F70 8.97 Tf 11.27 0 Td[(chil)-15(d:Law)-28(y)-36(er)]TJ/F86 8.97 Tf 56.19 0 Td[(had)-217(been)-217(pruned)-217(from)-216(the)-218(e)16(xplanation.\051)]TJ -105.23 -9.37 Td[(From)]TJ/F97 8.97 Tf 21.68 0 Td[(lNotNot)]TJ/F86 8.97 Tf 33.34 0 Td[(we)-250(get)]TJ/F87 8.97 Tf -45.05 -13.59 Td[(Double)-248(ne)40(gation)-249(elimination)-248(on)-249(the)-250(lhs)-249(leaves)]TJ/F78 8.97 Tf 166.75 0 Td[(Doctor)]TJ/F86 8.97 Tf 28.25 0 Td[(.)]TJ -204.97 -13.59 Td[(Finally)66(,)-250(skipping)]TJ/F97 8.97 Tf 62.45 0 Td[(rOr)]TJ/F86 8.97 Tf 13.23 0 Td[(,)]TJ/F97 8.97 Tf 4.48 0 Td[(ident)]TJ/F86 8.97 Tf 21.39 0 Td[(produces:)]TJ/F87 8.97 Tf -91.58 -13.58 Td[(The)-271(subsumption)-270(now)-272(follows)-270(because)-271(the)-272(description)]TJ/F78 8.97 Tf 196.91 0 Td[(Doctor)]TJ/F87 8.97 Tf -196.91 -9.37 Td[(is)-193(subsumed)-192(by)]TJ/F78 8.97 Tf 55.01 0 Td[(Doctor)]TJ/F86 8.97 Tf 28.25 0 Td[(,)]TJ/F87 8.97 Tf 3.98 0 Td[(and)-193(the)-193(rhs)-193(is)-193(an)-193(e)20(xpansion)-192(of)]TJ/F78 8.97 Tf 107.43 0 Td[(Doctor)]TJ/F87 8.97 Tf 28.24 0 Td[(,)]TJ -222.91 -9.37 Td[(since)-249(it)-249(is)-250(a)-250(disjunction)]TJ/F86 8.97 Tf 82.69 0 Td[(.)]TJ ET endstream endobj 48 0 obj 34231 endobj 45 0 obj << /ProcSet [/PDF /Text] /Font << /F44 17 0 R /F98 49 0 R /F50 23 0 R /F47 29 0 R /F95 33 0 R /F89 18 0 R /F86 11 0 R /F88 16 0 R /F70 13 0 R /F71 12 0 R /F87 15 0 R /F73 34 0 R /F97 42 0 R /F106 43 0 R /F15 14 0 R /F101 44 0 R /F78 21 0 R /F49 20 0 R /F46 22 0 R >> >> endobj 46 0 obj << /Type /Page /Contents 47 0 R /Resources 45 0 R /MediaBox [0 0 595.27 841.89] /Parent 24 0 R >> endobj 52 0 obj << /Length 53 0 R >> stream 1 0 0 1 47.37 759.64 cm BT /F42 10.91 Tf 0 0 Td[(\050)]TJ/F107 7.97 Tf 4.25 0 Td[(StructSome)]TJ/F42 10.91 Tf 41.27 0 Td[(\051)]TJ/F46 7.97 Tf 23.02 4.72 Td[(a)]TJ/F49 7.97 Tf 4.5 0 Td[(v)]TJ/F46 7.97 Tf 6.58 0 Td[(b)]TJ ET 57.9 2.51 35.99 0.44 re f 1 0 0 1 57.9 -3.76 cm BT /F49 7.97 Tf 0 0 Td[(9)]TJ/F46 7.97 Tf 4.7 0 Td[(r)29(:a)]TJ/F49 7.97 Tf 10.44 0 Td[(v9)]TJ/F46 7.97 Tf 11.29 0 Td[(r)29(:b)]TJ 41.32 8.48 Td[(a)]TJ/F49 7.97 Tf 4.5 0 Td[(v)]TJ/F46 7.97 Tf 6.58 0 Td[(b)]TJ ET 57.11 6.27 35.99 0.44 re f 1 0 0 1 57.11 0 cm BT /F49 7.97 Tf 0 0 Td[(8)]TJ/F46 7.97 Tf 4.7 0 Td[(r)29(:a)]TJ/F49 7.97 Tf 10.44 0 Td[(v8)]TJ/F46 7.97 Tf 11.29 0 Td[(r)29(:b)]TJ/F42 10.91 Tf 53.1 3.76 Td[(\050)]TJ/F107 7.97 Tf 4.24 0 Td[(StructAll)]TJ/F42 10.91 Tf 31.54 0 Td[(\051)]TJ/F46 7.97 Tf -112.62 -15.12 Td[(a)]TJ/F49 7.97 Tf 4.5 0 Td[(v)]TJ/F43 7.97 Tf 6.58 0 Td[(\050)]TJ/F46 7.97 Tf 3.3 0 Td[(b)]TJ/F49 7.97 Tf 3.62 0 Td[(t)]TJ/F46 7.97 Tf 5.65 0 Td[(c)]TJ/F43 7.97 Tf 3.66 0 Td[(\051)]TJ ET -13.27 -14.23 62.54 0.44 re f 1 0 0 1 -13.27 -20.64 cm BT /F49 7.97 Tf 0 0 Td[(8)]TJ/F46 7.97 Tf 4.7 0 Td[(r)29(:a)]TJ/F49 7.97 Tf 10.44 0 Td[(v)]TJ/F43 7.97 Tf 6.58 0 Td[(\050)]TJ/F49 7.97 Tf 3.3 0 Td[(8)]TJ/F46 7.97 Tf 4.7 0 Td[(r)29(:b)]TJ/F49 7.97 Tf 9.56 0 Td[(t9)]TJ/F46 7.97 Tf 10.35 0 Td[(r)29(:c)]TJ/F43 7.97 Tf 9.61 0 Td[(\051)]TJ/F42 10.91 Tf 12.4 3.9 Td[(\050)]TJ/F107 7.97 Tf 4.24 0 Td[(AllIsaAllSome)]TJ/F49 7.97 Tf 48.46 0 Td[()]TJ/F42 10.91 Tf 4.24 0 Td[(\051)]TJ/F95 7.97 Tf -193.23 -20.35 Td[(Figur)18(e)-250(4.)]TJ/F89 7.97 Tf 38.38 0 Td[(ERs)-250(for)-250(role-restriction)-250(subsumptions)]TJ/F83 10.91 Tf -80.73 -26.07 Td[(4)-1000(Extensions)]TJ/F86 8.97 Tf 0 -16.27 Td[(Implemented)-418(DL)-418(systems)-419(support)-418(additional)-418(features)-418(such)-419(as)-419(ter)20(-)]TJ 0 -9.37 Td[(minological)-466(denitions)-465(\050)]TJ/F87 8.97 Tf 92.08 0 Td[(Tbox)]TJ/F86 8.97 Tf 17.96 0 Td[(\051)-467(and)-467(role)-467(hierarchies.)-465(Explanations)]TJ -110.04 -9.37 Td[(should)-249(support)-249(these)-249(as)-249(well.)]TJ 9.22 -9.37 Td[(A)-339(Tbox)-338(is)-339(a)-339(set)-339(of)-339(axioms)-338(of)-339(the)-339(form)]TJ/F70 8.97 Tf 144.99 0 Td[(C)]TJ/F71 8.97 Tf 11.3 0 Td[(v)]TJ/F70 8.97 Tf 11.26 0 Td[(D)]TJ/F86 8.97 Tf 10.89 0 Td[(or)]TJ/F70 8.97 Tf 10.52 0 Td[(C)]TJ 13.6 5.13 Td[(:)]TJ/F15 8.97 Tf -2.3 -5.13 Td[(=)]TJ/F70 8.97 Tf 11.25 0 Td[(D)]TJ/F86 8.97 Tf 10.9 0 Td[(that)]TJ -231.63 -9.37 Td[(assert)-382(subsumption)-380(relationships)-380(between)-381(\050possibly)-381(comple)16(x\051)-382(con-)]TJ 0 -9.37 Td[(cepts.)-228(In)-229(man)16(y)-229(DLs,)-228(axioms)-228(are)-228(restricted)-228(to)-228(be)-229(denitions:)-227(the)-228(left)]TJ 0 -9.37 Td[(hand)-290(side)-290(is)-291(an)-290(atomic)-290(concept)-290(name)-290(that)-290(does)-290(not)-290(occur)-290(on)-291(the)-290(left)]TJ 0 -9.37 Td[(hand)-221(side)-221(of)-221(an)15(y)-221(other)-221(axiom,)-221(and)-221(is)-221(not)-221(referred)-221(to)-221(\050either)-220(directly)-221(or)]TJ 0 -9.37 Td[(indirectly\051)-274(in)-274(the)-275(right)-274(hand)-275(side.)-274(Examples)-274(of)-274(denition)-274(axioms)-274(are)]TJ/F78 8.97 Tf 0 -9.37 Td[(Doctor)]TJ/F71 8.97 Tf 30.81 0 Td[(v)]TJ/F78 8.97 Tf 9.72 0 Td[(WellPaid)]TJ/F86 8.97 Tf 39.9 0 Td[(and)]TJ/F78 8.97 Tf 15.19 0 Td[(RichKids)]TJ/F70 8.97 Tf 42.52 5.13 Td[(:)]TJ/F15 8.97 Tf -2.3 -5.13 Td[(=)]TJ/F71 8.97 Tf 9.73 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.53 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.59 0 Td[(Rich)]TJ/F71 8.97 Tf 20.87 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(.)]TJ -232.04 -9.37 Td[(When)-382(the)-382(Tbox)-382(is)-382(restricted)-382(to)-382(denition)-381(axioms,)-382(reasoning)-381(in-)]TJ -9.22 -9.37 Td[(v)20(olv)15(es)-436(simply)-436(e)15(xpanding)-435(names)-436(with)-436(the)-436(associated)-436(Tbox)-436(deni-)]TJ 0 -9.37 Td[(tions)-383(during)-382(a)-383(proof.)-382(F)15(or)-383(e)15(xample,)-382(if)-383(the)-383(concept)]TJ/F78 8.97 Tf 186.56 0 Td[(RichKids)]TJ/F86 8.97 Tf 41.1 0 Td[(were)]TJ -227.66 -9.37 Td[(dened)-336(as)-338(in)-337(the)-337(pre)26(vious)-337(paragraph)-335(and)-337(used)-337(in)-337(our)-337(earlier)-336(e)15(xam-)]TJ 0 -9.37 Td[(ple)-282(instead)-282(of)]TJ/F71 8.97 Tf 51.43 0 Td[(8)]TJ/F78 8.97 Tf 5.12 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.25 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(,)-282(then)-282(it)-283(could)-281(be)-283(e)16(xpanded)]TJ -147.13 -11.12 Td[(to)]TJ/F78 8.97 Tf 10.42 0 Td[(RichKids)]TJ/F71 8.97 Tf 40.62 0 Td[(u)-331(8)]TJ/F78 8.97 Tf 14.23 0 Td[(child)]TJ/F70 8.97 Tf 23.54 0 Td[(:)]TJ/F15 8.97 Tf 2.56 0 Td[(\050)]TJ/F78 8.97 Tf 3.58 0 Td[(Rich)]TJ/F71 8.97 Tf 20.88 0 Td[(t)]TJ/F78 8.97 Tf 8.19 0 Td[(Doctor)]TJ/F15 8.97 Tf 28.24 0 Td[(\051)]TJ/F86 8.97 Tf 7.03 0 Td[(during)-383(the)-383(proof.)]TJ/F113 5.98 Tf 62.92 3.81 Td[(3)]TJ/F86 8.97 Tf 6.93 -3.81 Td[(This)]TJ -229.14 -9.37 Td[(procedure)-294(can)-294(be)-294(captured)-294(by)-294(simple)-294(sequent)-294(rules)-294(with)-294(side)-295(condi-)]TJ 0 -11.06 Td[(tions,)-367(such)-367(as)]TJ/F47 5.98 Tf 54.68 3.97 Td[(c;d;X)]TJ/F50 5.98 Tf 22.2 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ ET -52.32 -219.47 36.72 0.38 re f 1 0 0 1 -49.27 -224.56 cm BT /F47 5.98 Tf 0 0 Td[(c;X)]TJ/F50 5.98 Tf 16.1 0 Td[(`)]TJ/F47 5.98 Tf 8.63 0 Td[(Y)]TJ/F86 8.97 Tf 12.38 3.04 Td[(if)]TJ/F15 8.97 Tf 7.72 0 Td[(\050)]TJ/F70 8.97 Tf 3.58 0 Td[(c)]TJ 10.87 5.13 Td[(:)]TJ/F15 8.97 Tf -2.3 -5.13 Td[(=)]TJ/F70 8.97 Tf 11.74 0 Td[(d)]TJ/F15 8.97 Tf 4.77 0 Td[(\051)]TJ/F71 8.97 Tf 8.16 0 Td[(2)]TJ/F86 8.97 Tf 10.71 0 Td[(Tbox,)-367(and)-368(e)16(xplained)-367(by)-367(a)]TJ -150.09 -11.43 Td[(corresponding)-335(ER)-336(rules)-336(such)-336(as:)]TJ/F87 8.97 Tf 121.69 0 Td[()]TJ/F70 8.97 Tf 4.99 0 Td[()]TJ/F87 8.97 Tf 8.94 0 Td[(can)-336(be)-336(str)37(engthened)-335(to)]TJ/F70 8.97 Tf 86.46 0 Td[()]TJ/F71 8.97 Tf 8.56 0 Td[(u)]TJ/F70 8.97 Tf 8.78 0 Td[(\014)]TJ/F87 8.97 Tf -239.42 -10.82 Td[(because)]TJ/F70 8.97 Tf 31.07 0 Td[()]TJ 10.77 5.13 Td[(:)]TJ/F15 8.97 Tf -2.3 -5.13 Td[(=)]TJ/F70 8.97 Tf 9.73 0 Td[(\014)]TJ/F87 8.97 Tf 7.84 0 Td[(is)-243(in)-243(the)-243(Tbox)]TJ/F86 8.97 Tf 53.38 0 Td[(.)]TJ/F113 5.98 Tf 2.24 3.81 Td[(4)]TJ/F86 8.97 Tf 5.67 -3.81 Td[(Moreo)16(v)15(er)40(,)-243(correspondence)-241(with)-242(the)]TJ -118.4 -9.37 Td[(tableaux)-277(algorithm)-277(is)-278(maintained)-276(because)-277(the)-277(lazy)-278(unfolding)-276(opti-)]TJ 0 -9.37 Td[(misation)-200(beha)21(v)15(es)-200(in)-201(e)15(xactly)-200(the)-200(same)-200(w)10(ay:)-201(dened)-199(concept)-200(names)-200(are)]TJ 0 -9.37 Td[(only)-229(unfolded)-229(\050e)16(xpanded\051)-229(as)-229(required)-229(by)-229(the)-230(progress)-228(of)-230(the)-229(tableaux)]TJ 0 -9.37 Td[(proof.)-304(A)-305(v)16(ery)-305(similar)-303(technique)-304(can)-304(be)-304(applied)-304(with)-304(necessary)-303(con-)]TJ 0 -9.37 Td[(ditions)-255(on)-257(primiti)27(v)15(e)-256(concepts)-255(\050i.e.,)-256(when)]TJ/F70 8.97 Tf 146.68 0 Td[(C)]TJ/F86 8.97 Tf 9.52 0 Td[(is)-256(an)-256(atomic)-255(concept)-255(and)]TJ/F70 8.97 Tf -156.2 -9.37 Td[(C)]TJ/F71 8.97 Tf 9.78 0 Td[(v)]TJ/F70 8.97 Tf 9.72 0 Td[(D)]TJ/F71 8.97 Tf 10.42 0 Td[(2)]TJ/F86 8.97 Tf 8.7 0 Td[(Tbox\051.)]TJ -29.4 -9.37 Td[(Extending)-265(the)-266(tableaux)-266(algorithm)-265(to)-267(deal)-266(with)-267(transiti)27(v)15(e)-267(roles)-266(and)]TJ -9.22 -9.37 Td[(role)-309(hierarchies)-309(requires)-308(only)-309(a)-310(relati)26(v)15(ely)-310(minor)-308(e)15(xtension)-309(to)-309(the)]TJ/F71 8.97 Tf 236.98 0 Td[(9)]TJ/F87 8.97 Tf 5.12 0 Td[(-)]TJ -242.1 -9.37 Td[(rule)]TJ/F86 8.97 Tf 17.48 0 Td[([5],)-337(and)-337(a)-338(corresponding)-336(e)15(xtension)-336(to)-338(the)-337(modal)-337(sequent)-337(rules)]TJ -17.48 -9.37 Td[(is)-239(possible.)-238(\050This)-238(e)15(xtension)-238(leads)-239(to)-239(some)-238(problems)-238(with)-238(termination)]TJ 0 -9.37 Td[(in)-361(the)-361(tableaux)-360(algorithm,)-360(b)20(ut)-361(this)-361(is)-361(irrele)26(v)25(ant)-361(for)-360(the)-361(e)15(xplanation)]TJ 0 -9.37 Td[(component,)-248(which)-249(recei)26(v)15(es)-250(a)-249(completed)-248(proof.\051)]TJ 9.22 -9.37 Td[(Modern)-208(DL)-209(implementations)-207(also)-209(support)-209(a)-210(v)26(ariety)-209(of)-210(of)-209(optimisa-)]TJ -9.22 -9.37 Td[(tion)-291(techniques.)-289(Some)-290(\050lik)11(e)-291(lazy)-291(unfolding\051)-289(f)10(acilitate)-290(the)-290(generation)]TJ 0 -9.37 Td[(of)-415(parsimonious)-414(e)16(xplanations.)-414(F)15(or)-415(e)15(xample,)-414(backjumping,)-413(a)-415(tech-)]TJ 0 -9.37 Td[(nique)-312(for)-313(pruning)-312(irrele)26(v)25(ant)-312(search,)-312(complements)-311(the)-313(simplication)]TJ 0 -9.37 Td[(procedure)-348(described)-348(in)-349(Section)-348(3.1,)-349(while)-348(caching,)-348(a)-349(technique)-348(for)]TJ 0 -9.37 Td[(reusing)-249(sub-proofs,)-248(can)-249(be)-250(used)-249(as)-249(a)-250(lemma)-249(generator)57(.)]TJ 9.22 -9.37 Td[(Other)-494(e)15(xtensions,)-493(such)-495(as)-495(general)-494(Tbox)-494(axioms)-494(and)-495(semantic)]TJ -9.22 -9.37 Td[(branching)-296(optimisation)-295(complicate)-295(the)-297(task)-296(of)-297(e)15(xplanation,)-296(and)-296(will)]TJ 0 -9.37 Td[(be)-250(treated)-248(in)-250(future)-249(w)10(ork.)]TJ/F83 10.91 Tf 0 -28.27 Td[(5)-1000(Conclusions)]TJ/F86 8.97 Tf 0 -16.27 Td[(Explanation)-460(of)-461(subsumption)-460(in)-461(e)15(xpressi)26(v)15(e)-461(description)-460(logics)-461(w)10(as)]TJ 0 -9.37 Td[(thought)-211(to)-211(be)-212(hard)-211(because)-210(the)-211(standard)-211(proof)-211(techniques)-210(are)-211(tableau-)]TJ 0 -9.37 Td[(based,)-249(and)-249(are)-250(thus)-249(unnatural.)]TJ 9.22 -9.37 Td[(W)81(e)-256(ha)20(v)15(e)-256(proposed)-254(a)-256(methodology)-254(for)-256(e)15(xplaining)-254(the)-256(subsumption)]TJ -9.22 -9.37 Td[(relationship)-258(between)]TJ/F71 8.97 Tf 76.88 0 Td[(ALC)]TJ/F86 8.97 Tf 21.41 0 Td[(concepts)-259(based)-259(on)-259(\050i\051)-260(a)-259(sequent)-259(proof)-259(for)]TJ/F71 8.97 Tf -98.29 -9.37 Td[(ALC)]TJ/F86 8.97 Tf 21.87 0 Td[(deri)25(v)16(ed)-311(from)-311(a)-311(tableaux)-310(based)-310(procedure,)-309(\050ii\051)-311(a)-311(pruning)-310(algo-)]TJ -21.87 -9.37 Td[(rithm)-325(that)-324(eliminates)-324(unnecessary)-323(steps,)-324(and)-325(\050iii\051)-324(a)-325(set)-325(of)-325(templates)]TJ 0 -9.37 Td[(used)-280(to)-281(generate)-280(surf)11(ace)-280(e)15(xplanations)-279(\050in)-280(one)-281(or)-280(more)-280(steps\051)-280(from)]TJ 0 -9.37 Td[(each)-281(sequent)-280(rule)-280(application.)-280(The)-280(signicant)-280(properties)-280(of)-280(this)-281(pro-)]TJ 0 -9.37 Td[(posal)-341(include)-340(the)-341(f)10(act)-341(that)-341(\050a\051)-341(the)-341(proof)-341(does)-341(not)-341(mo)16(v)15(e)-342(terms)-340(from)]TJ 0 -9.37 Td[(one)-269(side)-269(of)-270(the)-269(turnstile)-269(to)-269(the)-269(other)41(,)-270(thus)-269(preserving)-268(the)-269(structure)-269(of)]TJ ET -57.73 -364.08 245.08 0.8 re f 1 0 0 1 -57.73 -370.12 cm BT /F44 5.98 Tf 0 0 Td[(3)]TJ/F89 7.97 Tf 6.02 -2.81 Td[(It)-234(could)-234(be)-234(substituted)-235(with)-234(its)-234(denition,)-234(b)20(ut)-234(retaining)-235(the)-234(name)-234(can)-234(lead)-234(to)]TJ 0.96 -8.14 Td[(a)-249(shorter)-250(proof.)]TJ/F44 5.98 Tf -6.98 -6.3 Td[(4)]TJ/F89 7.97 Tf 6.05 -2.81 Td[(Such)-237(a)-237(sequent)-238(calculus)-237(w)10(ould,)-238(in)-237(general,)-238(be)-237(non)-238(terminating.)-237(Ho)25(we)25(v)15(er)40(,)-237(in)]TJ 0.93 -8.14 Td[(our)-330(frame)25(w)10(ork,)-331(nite)-330(proofs)-331(are)-331(generated)-330(by)-331(the)-331(tableaux)-330(algorithm,)-331(for)]TJ 0 -8.14 Td[(which)-249(termination)-250(is)-250(guaranteed.)]TJ/F86 8.97 Tf 256.03 660.41 Td[(the)-228(original)-226(subsumption,)]TJ/F87 8.97 Tf 93.06 0 Td[(yet)-227(can)-227(be)-227(obtained)-227(dir)38(ectly)-227(fr)45(om)-227(a)-227(slightly)]TJ -93.06 -9.37 Td[(enhanced)-343(tableaux)-343(algorithm)]TJ/F86 8.97 Tf 106.79 0 Td[(;)-344(\050b\051)-343(the)-344(surf)11(ace)-344(e)16(xplanation)-343(rules)-343(are)]TJ -106.79 -9.37 Td[(used)-307(to)-307(pro)16(vide)-306(the)-307(simplest)-306(e)16(xplanation)-306(possible,)-305(a)20(v)20(oiding)-306(in)-307(most)]TJ 0 -9.37 Td[(cases)-379(the)-379(use)-379(of)-379(the)-379(one)-379(ER)-379(that,)-379(we)-379(belie)26(v)15(e,)-379(w)10(ould)-378(itself)-379(require)]TJ 0 -9.37 Td[(e)15(xplanation)-248(\050namely)]TJ/F15 8.97 Tf 75.57 0 Td[(\050)]TJ/F97 8.97 Tf 3.59 0 Td[(AllIsaAllSome)]TJ/F15 8.97 Tf 52.79 0 Td[(\051)]TJ/F86 8.97 Tf 3.58 0 Td[(\051.)]TJ -126.31 -9.37 Td[(In)-354(some)-354(situations,)-353(our)-354(approach)-354(may)-354(in)-354(f)10(act)-354(be)-355(better)-353(than)-354(one)]TJ -9.22 -9.37 Td[(based)-262(on)-262(nai)25(v)15(e)-262(structural)-261(subsumption)-260(e)25(v)15(en)-262(for)-262(languages)-261(where)-261(the)]TJ 0 -9.37 Td[(latter)-395(proof)-394(technique)-394(is)-395(applicable.)-393(F)15(or)-395(e)15(xample,)-394(in)-395(sho)26(wing)-394(that)]TJ/F70 8.97 Tf 0 -9.37 Td[(C)]TJ/F71 8.97 Tf 8.45 0 Td[(u)]TJ/F70 8.97 Tf 7.37 0 Td[()]TJ/F71 8.97 Tf 11.03 0 Td[(v)]TJ/F70 8.97 Tf 12.29 0 Td[(C)]TJ/F86 8.97 Tf 7.22 0 Td[(,)-225(a)-226(structural)-225(subsumption)-223(technique)-225(rst)-225(normalises)-224(the)]TJ -46.36 -9.37 Td[(lhs,)-246(which)-244(is)-246(unnecessary)-243(in)-246(this)-245(case,)-245(yet)-245(might)-244(in)40(v)20(olv)16(e)-246(comple)16(x)-245(in-)]TJ 0 -9.37 Td[(ferences)-223(if,)-223(for)-223(e)16(xample,)]TJ/F70 8.97 Tf 88.55 0 Td[()]TJ/F86 8.97 Tf 7.91 0 Td[(contains)-222(an)-223(incoherence.)-222(The)-223(same)-222(w)10(ould)]TJ -96.46 -9.37 Td[(apply)-274(if)]TJ/F70 8.97 Tf 30.32 0 Td[(C)]TJ/F86 8.97 Tf 9.68 0 Td[(is)-273(a)-274(dened)-273(concept,)-273(when)-273(normalisation)-272(e)15(xpands)-273(deni-)]TJ -40 -9.37 Td[(tions,)-249(while)-249(our)-250(lazy)-249(unfolding)-248(w)10(ould)-249(nd)-249(the)-250(proof)-249(immediately)67(.)]TJ 9.22 -9.37 Td[(The)-342(choice)-342(of)-343(the)-342(surf)10(ace)-342(e)15(xplanation)-341(rules,)-342(and)-342(especially)-342(their)]TJ -9.22 -9.37 Td[(English)-238(language)-237(realization)-237(is)-238(to)-238(some)-238(e)15(xtent)-237(pro)15(visional)-237(in)-238(the)-238(cur)20(-)]TJ 0 -9.37 Td[(rent)-349(w)11(ork.)-349(This)-348(is)-349(particularly)-347(the)-348(case)-348(with)-348(proofs)-348(in)40(v)20(olving)-348(role-)]TJ 0 -9.37 Td[(restrictions.)]TJ 9.22 -9.37 Td[(Although)-307(much)-307(more)-307(sophisticated)-307(natural)-307(language)-306(te)15(xt)-308(genera-)]TJ -9.22 -9.37 Td[(tion)-225(is)-225(possible)-224(from)-224(proofs)-224(\050e.g.)-225([8]\051,)-224(we)-225(belie)26(v)15(e)-225(that)-225(for)-224(users)-225(b)20(uild-)]TJ 0 -9.37 Td[(ing)-313(DL)-312(kno)26(wledge)-311(bases,)-312(a)-312(point-by-point)-311(e)16(xplanation)-311(of)-313(the)-312(infer)21(-)]TJ 0 -9.37 Td[(ences,)-284(as)-285(done)-284(earlier)-284(in)]TJ/F88 7.17 Tf 89.93 0 Td[(C)-63(L)-61(A)-63(S)-61(S)-62(I)-62(C)]TJ/F86 8.97 Tf 32.37 0 Td[(,)-285(is)-285(suf)26(cient.)-284(W)81(e)-285(are)-284(a)15(w)10(are)-284(that)-285(a)]TJ -122.3 -9.37 Td[(considerable)-200(number)-201(of)-202(theorem)-201(pro)16(v)15(ers)-202(ha)21(v)15(e)-202(been)-201(endo)25(wed)-201(with)-201(the)]TJ 0 -9.37 Td[(ability)-231(to)-231(produce)-230(e)15(xplanations)-229(from)-231(the)-231(steps)-230(of)-231(proofs,)-231(and)-231(some)-230(of)]TJ 0 -9.36 Td[(them,)-199(e.g.,)]TJ/F88 7.17 Tf 39.17 0 Td[(I)-63(L)-62(F)]TJ/F86 8.97 Tf 13.66 0 Td[([1],)-199(e)25(v)15(en)-199(of)26(fer)-200(a)-199(service)-199(whereby)-198(proofs)-199(obtained)-198(from)]TJ -52.83 -9.37 Td[(seemingly)-195(arbitrary)-195(axiomatisations)-193(can)-196(submitted)-194(to)-196(obtain)-195(a)-196(surf)11(ace)]TJ 0 -9.37 Td[(English)-276(e)15(xplanation,)-275(if)-276(the)-277(proof)-276(system)-275(can)-277(be)-276(reformulated)-275(appro-)]TJ 0 -9.37 Td[(priately)66(.)-290(The)-290(v)15(ery)-290(specialised)-288(nature)-289(of)-290(concept)-289(descriptions)-289(in)-289(DLs)]TJ 0 -9.37 Td[(and)-253(modal)-251(logics)-252(\050in)-252(contrast)-251(to)-253(FOL)-252(formulas\051)-251(and)-252(of)-252(the)-252(subsump-)]TJ 0 -9.37 Td[(tion)-322(proof)-321(itself,)-321(ha)21(v)15(e)-322(led)-321(us)-321(to)-322(de)26(v)15(elop)-321(for)-322(no)26(w)-322(our)-321(o)25(wn)-321(relati)26(v)15(ely)]TJ 0 -9.37 Td[(simple)-352(surf)11(ace)-352(generator)41(,)-352(rather)-352(than)-352(trying)-352(to)-352(nd)-352(a)-352(translation)-351(of)]TJ 0 -9.37 Td[(our)-299(proofs)-298(into)-298(yet)-298(another)-298(form)-298(\050e.g.,)]TJ/F88 7.17 Tf 141.26 0 Td[(I)-63(L)-61(F)]TJ/F86 8.97 Tf 11.87 0 Td[(')56(s)-299(block)-298(proofs\051,)-297(which)]TJ -153.13 -9.37 Td[(may)-250(not)-249(be)-250(natural)-248(in)-250(the)-249(end.)]TJ 9.22 -9.37 Td[(W)80(e)-316(plan)-316(to)-316(concentrate)-315(instead)-315(on)-316(e)15(xtensions)-315(to)-316(more)-316(e)16(xpressi)26(v)15(e)]TJ -9.22 -9.37 Td[(DLs)-191(and)-192(their)-190(highly)-191(optimised)-190(implementations,)-189(as)-191(well)-191(as)-192(the)-191(in)41(v)15(es-)]TJ 0 -9.37 Td[(tigation)-224(of)-230(proof)-229(tactics)-229(that)-230(produce)-228(short)-230(or)-229(most)-230(easily)-229(e)15(xplainable)]TJ 0 -9.37 Td[(proofs.)]TJ/F85 8.97 Tf 0 -9.37 Td[(Ackno)11(wledgements)]TJ/F86 8.97 Tf 77.91 0 Td[(W)80(e)-422(wish)-421(to)-421(thank)-421(our)-422(original)-420(collaborators,)]TJ -77.91 -9.37 Td[(Deborah)-338(McGuinness)-337(and)-339(Peter)-338(P)15(atel-Schneider)-336(for)-339(their)-338(contrib)21(u-)]TJ 0 -9.37 Td[(tions,)-213(as)-213(well)-213(as)-212(v)15(ery)-213(useful)-212(pointers)-212(of)25(fered)-213(by)-212(Matthe)26(w)-213(Stone,)-213(Hans)]TJ 0 -9.37 Td[(Juer)18(gen)-237(Ohlbach,)-237(and)-238(by)-238(an)-238(anon)16(ymous)-237(referee.)-237(The)-238(rst)-237(author)-237(w)10(as)]TJ 0 -9.37 Td[(supported)-249(by)-249(NSF-grant)-248(IRI9619979.)]TJ/F83 10.91 Tf 0 -25.63 Td[(REFERENCES)]TJ/F89 7.97 Tf 2.99 -13.99 Td[([1])-875(B.)-265(I.)-265(Dahn,)-264(J.)-265(Gehne,)-264(T)74(.)-265(Honigmann)-265(and)-264(A.)-265(W)80(olf,)-264(`Inte)15(gration)-265(of)-265(auto-)]TJ 16.27 -8.52 Td[(mated)-266(and)-266(interacti)25(v)15(e)-266(theorem)-266(pro)15(ving)-266(in)-266(ILF',)]TJ/F94 7.97 Tf 152.75 0 Td[(Pr)45(oc.)-266(of)-266(CADE-14)]TJ/F89 7.97 Tf 59 0 Td[(,)-266(pp.)]TJ -211.75 -8.52 Td[(5760,)-250(\0501997\051.)]TJ -16.27 -8.52 Td[([2])-875(S.)-255(Demri)-254(and)-254(R.)-254(Gor)]TJ 82.81 0.04 Td[()]TJ -0.44 -0.04 Td[(e,)-255(`Display)-254(calculi)-254(for)-254(logics)-254(with)-255(relati)25(v)15(e)-254(accessi-)]TJ -66.1 -8.52 Td[(bility)-250(relations',)]TJ/F94 7.97 Tf 52.91 0 Td[(J)25(oLLI)]TJ/F89 7.97 Tf 18.84 0 Td[(,)-250(\0501999\051.)]TJ -88.02 -8.51 Td[([3])-875(M.)-233(Fitting,)]TJ/F94 7.97 Tf 52.31 0 Td[(Pr)45(oof)-233(Methods)-233(for)-233(Modal)-232(and)-233(Intuitionistic)-233(Lo)10(gics)]TJ/F89 7.97 Tf 160.36 0 Td[(,)-233(Kluwer)40(,)]TJ -196.4 -8.52 Td[(1983.)]TJ -16.27 -8.52 Td[([4])-875(B.)-341(Hollunder)-341(and)-341(W)92(.)-341(Nutt,)-340(`Subsumption)-341(algorithms)-341(for)-341(concept)-341(lan-)]TJ 16.27 -8.52 Td[(guages',)-250(in)]TJ/F94 7.97 Tf 36.97 0 Td[(Pr)46(oc.)-250(of)-250(ECAI'90)]TJ/F89 7.97 Tf 55.64 0 Td[(,)-250(pp.)-250(348353,)-250(\0501990\051.)]TJ -108.88 -8.52 Td[([5])-875(I.)-283(Horrocks,)-283(`Using)-284(an)-283(e)15(xpressi)25(v)15(e)-283(description)-283(logic:)-283(F)15(aCT)-283(or)-283(ction?',)]TJ 16.27 -8.51 Td[(in)]TJ/F94 7.97 Tf 8.19 0 Td[(Pr)45(oc.)-250(of)-250(KR'98)]TJ/F89 7.97 Tf 48.13 0 Td[(,)-250(pp.)-250(636647,)-250(\0501998\051.)]TJ -72.59 -8.52 Td[([6])-875(I.)-420(Horrocks)-420(and)-421(P)111(.)-420(F)80(.)-420(P)15(atel-Schneider)40(,)-420(`Optimising)-420(description)-420(logic)]TJ 16.27 -8.52 Td[(subsumption',)]TJ/F94 7.97 Tf 47.38 0 Td[(JLC)]TJ/F89 7.97 Tf 13.29 0 Td[(,)]TJ/F95 7.97 Tf 3.98 0 Td[(9)]TJ/F89 7.97 Tf 3.99 0 Td[(\0503\051,)-250(267293,)-250(\0501999\051.)]TJ -84.91 -8.52 Td[([7])-875(X.)-382(Huang,)-381(`Reconstructing)-381(proofs)-381(at)-382(the)-381(assertion)-381(le)25(v)15(el',)-381(in)]TJ/F94 7.97 Tf 215.73 0 Td[(Pr)45(oc.)-381(of)]TJ -199.46 -8.52 Td[(CADE-94)]TJ/F89 7.97 Tf 31.43 0 Td[(,)-250(\0501994\051.)]TJ -47.7 -8.51 Td[([8])-875(X.)-285(Huang)-285(and)-285(A.)-285(Fiedler)40(,)-284(`Presenting)-285(machine-found)-285(proofs',)-285(in)]TJ/F94 7.97 Tf 224.97 0 Td[(Pr)45(oc.)]TJ -208.7 -8.52 Td[(of)-250(CADE-96)]TJ/F89 7.97 Tf 39.63 0 Td[(,)-250(\0501996\051.)]TJ -55.9 -8.52 Td[([9])-875(C.)-316(Lingenfelder)40(,)-316(`T)35(ransformation)-316(of)-316(refutation)-315(graphs)-316(into)-316(natural)-316(de-)]TJ 16.27 -8.52 Td[(duction)-250(proofs',)-250(SEKI-Rep.)-250(86-10,)-250(Uni)25(v)65(.)-250(of)-250(Kaiserslautern,)-250(\0501986\051.)]TJ -20.25 -8.52 Td[([10])-875(D.)-325(McGuinness)-326(and)-325(A.)-326(Bor)18(gida,)-325(`Explaining)-326(subsumption)-326(in)-325(descrip-)]TJ 20.25 -8.51 Td[(tion)-250(logics',)-250(in)]TJ/F94 7.97 Tf 48.27 0 Td[(Pr)45(oc.)-250(of)-250(IJCAI'95)]TJ/F89 7.97 Tf 56.97 0 Td[(,)-250(pp.)-250(816821,)-250(\0501995\051.)]TJ -125.49 -8.52 Td[([11])-875(F)80(.)-358(Oppacher)-359(and)-359(E.)-359(Suen,)-358(`HARP:)-359(A)-359(tableau-based)-358(theorem)-359(pro)15(v)15(er',)]TJ/F94 7.97 Tf 20.25 -8.52 Td[(J)25(ournal)-250(of)-250(A)20(utomated)-250(Reasoning)]TJ/F89 7.97 Tf 104.8 0 Td[(,)]TJ/F95 7.97 Tf 3.98 0 Td[(4)]TJ/F89 7.97 Tf 3.99 0 Td[(,)-250(69100,)-250(\0501988\051.)]TJ -133.02 -8.52 Td[([12])-875(S.)-197(Ree)25(v)15(es)-198(and)-197(M.)-198(Clark)11(e,)]TJ/F94 7.97 Tf 100.99 0 Td[(Lo)10(gic)-197(for)-198(Computer)-197(Science)]TJ/F89 7.97 Tf 88.32 0 Td[(,)-197(Addison)-197(W)80(esle)15(y)65(,)]TJ -169.06 -8.52 Td[(1993.)]TJ -20.25 -8.51 Td[([13])-875(V)129(.)-368(Ro)10(yer)-367(and)-368(J.)-368(Quantz,)-368(`Deri)25(ving)-368(inference)-367(rules)-368(for)-368(terminological)]TJ 20.25 -8.52 Td[(logics',)-250(in)]TJ/F94 7.97 Tf 33.87 0 Td[(Pr)45(oc.)-250(of)-250(JELIA'92)]TJ/F89 7.97 Tf 58.3 0 Td[(,)-250(pp.)-250(84105,)-250(\0501992\051.)]TJ -112.42 -8.52 Td[([14])-875(W)92(.)-231(R.)-230(Sw)10(artout)-231(and)-231(J.)-231(D.)-231(Moore,)-231(`Explanation)-231(in)-230(second)-231(generation)-231(e)15(x-)]TJ 20.25 -8.52 Td[(pert)-305(systems',)-304(in)]TJ/F94 7.97 Tf 55.77 0 Td[(Second)-304(Gener)15(ation)-305(Expert)-304(Systems)]TJ/F89 7.97 Tf 112.96 0 Td[(,)-305(Springer)-305(V)111(erlag,)]TJ -168.73 -8.52 Td[(\0501996\051.)]TJ ET endstream endobj 53 0 obj 22440 endobj 50 0 obj << /ProcSet [/PDF /Text] /Font << /F42 54 0 R /F107 49 0 R /F46 22 0 R /F49 20 0 R /F43 8 0 R /F95 33 0 R /F89 18 0 R /F83 7 0 R /F86 11 0 R /F87 15 0 R /F70 13 0 R /F71 12 0 R /F15 14 0 R /F78 21 0 R /F113 55 0 R /F47 29 0 R /F50 23 0 R /F44 17 0 R /F97 42 0 R /F88 16 0 R /F85 10 0 R /F94 32 0 R >> >> endobj 51 0 obj << /Type /Page /Contents 52 0 R /Resources 50 0 R /MediaBox [0 0 595.27 841.89] /Parent 24 0 R >> endobj 56 0 obj << /Type /Encoding /Differences [ 0/.notdef 1/dotaccent/fi/fl/fraction/hungarumlaut/Lslash/lslash/ogonek/ring 10/.notdef 11/breve/minus 13/.notdef 14/Zcaron/zcaron/caron/dotlessi/dotlessj/ff/ffi/ffl 22/.notdef 30/grave/quotesingle/space/exclam/quotedbl/numbersign/dollar/percent/ampersand/quoteright/parenleft/parenright/asterisk/plus/comma/hyphen/period/slash/zero/one/two/three/four/five/six/seven/eight/nine/colon/semicolon/less/equal/greater/question/at/A/B/C/D/E/F/G/H/I/J/K/L/M/N/O/P/Q/R/S/T/U/V/W/X/Y/Z/bracketleft/backslash/bracketright/asciicircum/underscore/quoteleft/a/b/c/d/e/f/g/h/i/j/k/l/m/n/o/p/q/r/s/t/u/v/w/x/y/z/braceleft/bar/braceright/asciitilde 127/.notdef 130/quotesinglbase/florin/quotedblbase/ellipsis/dagger/daggerdbl/circumflex/perthousand/Scaron/guilsinglleft/OE 141/.notdef 147/quotedblleft/quotedblright/bullet/endash/emdash/tilde/trademark/scaron/guilsinglright/oe 157/.notdef 159/Ydieresis 160/.notdef 161/exclamdown/cent/sterling/currency/yen/brokenbar/section/dieresis/copyright/ordfeminine/guillemotleft/logicalnot/hyphen/registered/macron/degree/plusminus/twosuperior/threesuperior/acute/mu/paragraph/periodcentered/cedilla/onesuperior/ordmasculine/guillemotright/onequarter/onehalf/threequarters/questiondown/Agrave/Aacute/Acircumflex/Atilde/Adieresis/Aring/AE/Ccedilla/Egrave/Eacute/Ecircumflex/Edieresis/Igrave/Iacute/Icircumflex/Idieresis/Eth/Ntilde/Ograve/Oacute/Ocircumflex/Otilde/Odieresis/multiply/Oslash/Ugrave/Uacute/Ucircumflex/Udieresis/Yacute/Thorn/germandbls/agrave/aacute/acircumflex/atilde/adieresis/aring/ae/ccedilla/egrave/eacute/ecircumflex/edieresis/igrave/iacute/icircumflex/idieresis/eth/ntilde/ograve/oacute/ocircumflex/otilde/odieresis/divide/oslash/ugrave/uacute/ucircumflex/udieresis/yacute/thorn/ydieresis] >> endobj 55 0 obj << /Type /Font /Subtype /Type1 /Encoding 56 0 R /BaseFont /Times-Roman >> endobj 54 0 obj << /Type /Font /Subtype /Type1 /FirstChar 0 /LastChar 127 /Widths 57 0 R /BaseFont 63 0 R /FontDescriptor 64 0 R >> endobj 57 0 obj [ 625 833 778 694 667 750 722 778 722 778 722 583 556 556 833 833 278 306 500 500 500 500 500 750 444 500 722 778 500 903 1014 778 278 278 500 833 500 833 778 278 389 389 500 778 278 333 278 500 500 500 500 500 500 500 500 500 500 500 278 278 278 778 472 472 778 750 708 722 764 680 653 785 750 361 514 778 625 917 750 778 680 778 736 556 722 750 750 1028 750 750 611 278 500 278 500 278 278 500 556 444 556 444 306 500 556 278 306 528 278 833 556 500 556 528 392 394 389 556 528 722 528 528 444 500 1000 500 500 500 ] endobj 58 0 obj << /Length 59 0 R /Length1 60 0 R /Length2 61 0 R /Length3 62 0 R >> stream %!PS-AdobeFont-1.1: CMR10 1.00B %%CreationDate: 1992 Feb 19 19:54:52 % Copyright (C) 1997 American Mathematical Society. All Rights Reserved. 11 dict begin /FontInfo 7 dict dup begin /version (1.00B) readonly def /Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def /FullName (CMR10) readonly def /FamilyName (Computer Modern) readonly def /Weight (Medium) readonly def /ItalicAngle 0 def /isFixedPitch false def end readonly def /FontName /VEAAAA+CMR10 def /PaintType 0 def /FontType 1 def /FontMatrix [0.001 0 0 0.001 0 0] readonly def /Encoding 256 array dup 40 /parenleft put dup 41 /parenright put readonly def /FontBBox{-251 -250 1009 969}readonly def /UniqueID 5000793 def currentdict end currentfile eexec oc;j~EЪ*BgNӽؑlKq*Xws|QFqv`zXMyp"5O˩YŝP(DT! [v67XFlU&3!Rq4wσ~j+ou\c3R*R?쨤ȯ@ gSr RIzE_EMv,X!%6]ަ_3+_hJإ0o'z 9K$|tV\)Z! j#ZŚz1UA~ "p?{u@]A}s ijB)~Ob
{z;O9mT[Ğ^dUl$Wh :?Ƃ(r6;Bt6cFCr$/;!,KqL eWuG h7IQ[u20uZ8*#qP|̖I̓pe}#YۇW{
Hs(}CE c; [e/SmV&
i2ǡmc\0kC'sp)X0@$2jOGG9%fLJD@m 2b5\cdy!iz+lxa+2S@uIY5F>qgROEowK*;/sDGǡx=>J ujLDfdžk4ؐ.
vî| 1wm%QiwXDN}}x|E.gK{T >k&mxo.<n&lQ>I,
7
LU/GGSL@PEdԑϟ5::""l5ȸM-/5p 7ZB8]4t/ī+Ic/xe\% SqP=]IC!#ԽE~!|kZ`f <槷$TtPxCknKAAYsrƨF0,t u|bk"]fL`*ðydN)Ql1$?XN
E>cfV=[miGU>LfqcD t.2'-;p[MR+S"#bp`1i0zCD] ~+KX>`o9N(V%U0H?Ӫ~'XPl+Mkгp(I-hq.=fKr涍.y<,=l20FndہQ6_@sPNц&-&Dr!ۀOp]!&|h]DD_GJ IK'.zH*$Q]"A et`[vv3&g}`5dz+u
Ycvpo