Show simple item record

dc.contributor.authorFemke Dik, Josephine
dc.date.accessioned2022-06-23T10:01:40Z
dc.date.available2022-06-23T10:01:40Z
dc.identifier.urihttps://hdl.handle.net/2077/72328
dc.description.abstractIn [12], Hofmann introduces a sequent calculus for the description logic EL where the TBoxes allow for circular concept definitions. In this thesis, we apply this frame- work to a family of DLs which allow for circular TBoxes. We start off by adjusting the calculus for the class of frame-based DLs, with base logic FL0. We continue to the attribute languages AL and ALE. For these calculi, we prove soundness and completeness with respect to greatest fixpoint semantics for their fragments AL′ and ALE′, using Hofmann’s strategy. When applying the theory to a logic including disjunction, we require a different strategy and introduce the notion of pre-interpretation for the soundness and completeness proofs. Then, we acknowl- edge the drawbacks of considering only greatest fixpoint semantics when it comes to circular definitions, and propose a calculus that includes greatest- and least-fixpoint semantics in one. Finally, we discuss the drawbacks of Hofmann’s system for the classical logic ALC by discussing the consequences for the proofs when including the disjunction or negation, and give suggestions for future research.en_US
dc.language.isoengen_US
dc.subjectDescription logic, sequent calculus, fixpoints, circular TBoxesen_US
dc.titleProof Theory of Circular Description Logicsen_US
dc.typeText
dc.setspec.uppsokHumanitiesTheology
dc.type.svepH2
dc.contributor.departmentGöteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteoriswe
dc.contributor.departmentGöteborg University/Department of Philosophy, Linguistics and Theory of Scienceeng
dc.type.degreeStudent essay


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record