Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:

in
/  
in
/  
in
/  
in

Written in Published in Earliest date Latest date

Sorted by

Results per page:

Sorted by: relevance · author · university · dateNew search

You searched for subject:(Computer science mathematics Mathematical logic AND foundations Applications AND algorithms description logics automated reasoning classification). Showing records 1 – 2 of 2 total matches.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters


University of Oxford

1. Shearer, Robert D. C. Scalable reasoning for description logics.

Degree: 2011, University of Oxford

Description logics (DLs) are knowledge representation formalisms with well-understood model-theoretic semantics and computational properties. The DL SROIQ provides the logical underpinning for the semantic web language OWL 2, which is quickly becoming the standard for knowledge representation on the web. A central component of most DL applications is an efficient and scalable reasoner, which provides services such as consistency testing and classification. Despite major advances in DL reasoning algorithms over the last decade, however, ontologies are still encountered in practice that cannot be handled by existing DL reasoners. We present a novel reasoning calculus for the description logic SROIQ which addresses two of the major sources of inefficiency present in the tableau-based reasoning calculi used in state-of-the-art reasoners: unnecessary nondeterminism and unnecessarily large model sizes. Further, we describe a new approach to classification which exploits partial information about the subsumption relation between concept names to reduce both the number of individual subsumption tests performed and the cost of working with large ontologies; our algorithm is applicable to the general problem of deducing a quasi-ordering from a sequence of binary comparisons. We also present techniques for extracting partial information about the subsumption relation from the models generated by constructive DL reasoning methods, such as our hypertableau calculus. Empirical results from a prototypical implementation demonstrate substantial performance improvements compared to existing algorithms and implementations.

Subjects/Keywords: 005.3; Computer science (mathematics) : Mathematical logic and foundations : Applications and algorithms : description logics : automated reasoning : classification

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Shearer, R. D. C. (2011). Scalable reasoning for description logics. (Doctoral Dissertation). University of Oxford. Retrieved from http://ora.ox.ac.uk/objects/uuid:d7c4fbf6-4258-4db4-a451-476dcebe68ca ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540275

Chicago Manual of Style (16th Edition):

Shearer, Robert D C. “Scalable reasoning for description logics.” 2011. Doctoral Dissertation, University of Oxford. Accessed June 16, 2019. http://ora.ox.ac.uk/objects/uuid:d7c4fbf6-4258-4db4-a451-476dcebe68ca ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540275.

MLA Handbook (7th Edition):

Shearer, Robert D C. “Scalable reasoning for description logics.” 2011. Web. 16 Jun 2019.

Vancouver:

Shearer RDC. Scalable reasoning for description logics. [Internet] [Doctoral dissertation]. University of Oxford; 2011. [cited 2019 Jun 16]. Available from: http://ora.ox.ac.uk/objects/uuid:d7c4fbf6-4258-4db4-a451-476dcebe68ca ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540275.

Council of Science Editors:

Shearer RDC. Scalable reasoning for description logics. [Doctoral Dissertation]. University of Oxford; 2011. Available from: http://ora.ox.ac.uk/objects/uuid:d7c4fbf6-4258-4db4-a451-476dcebe68ca ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.540275


University of Oxford

2. Merry, Alexander. Reasoning with !-graphs.

Degree: PhD, 2013, University of Oxford

The aim of this thesis is to present an extension to the string graphs of Dixon, Duncan and Kissinger that allows the finite representation of certain infinite families of graphs and graph rewrite rules, and to demonstrate that a logic can be built on this to allow the formalisation of inductive proofs in the string diagrams of compact closed and traced symmetric monoidal categories. String diagrams provide an intuitive method for reasoning about monoidal categories. However, this does not negate the ability for those using them to make mistakes in proofs. To this end, there is a project (Quantomatic) to build a proof assistant for string diagrams, at least for those based on categories with a notion of trace. The development of string graphs has provided a combinatorial formalisation of string diagrams, laying the foundations for this project. The prevalence of commutative Frobenius algebras (CFAs) in quantum information theory, a major application area of these diagrams, has led to the use of variable-arity nodes as a shorthand for normalised networks of Frobenius algebra morphisms, so-called "spider notation". This notation greatly eases reasoning with CFAs, but string graphs are inadequate to properly encode this reasoning. This dissertation firstly extends string graphs to allow for variable-arity nodes to be represented at all, and then introduces !-box notation – and structures to encode it – to represent string graph equations containing repeated subgraphs, where the number of repetitions is abitrary. This can be used to represent, for example, the "spider law" of CFAs, allowing two spiders to be merged, as well as the much more complex generalised bialgebra law that can arise from two interacting CFAs. This work then demonstrates how we can reason directly about !-graphs, viewed as (typically infinite) families of string graphs. Of particular note is the presentation of a form of graph-based induction, allowing the formal encoding of proofs that previously could only be represented as a mix of string diagrams and explanatory text.

Subjects/Keywords: 006.6; Computer science (mathematics); Mathematical logic and foundations; Quantum theory (mathematics); Applications and algorithms; Program development and tools; Theory and automated verification; graphs; commutative frobenius algrebras; quantum computer science; quantomatic; automated reasoning; proofs

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Merry, A. (2013). Reasoning with !-graphs. (Doctoral Dissertation). University of Oxford. Retrieved from http://ora.ox.ac.uk/objects/uuid:416c2e6d-2932-4220-8506-50e6b403b660 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.604414

Chicago Manual of Style (16th Edition):

Merry, Alexander. “Reasoning with !-graphs.” 2013. Doctoral Dissertation, University of Oxford. Accessed June 16, 2019. http://ora.ox.ac.uk/objects/uuid:416c2e6d-2932-4220-8506-50e6b403b660 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.604414.

MLA Handbook (7th Edition):

Merry, Alexander. “Reasoning with !-graphs.” 2013. Web. 16 Jun 2019.

Vancouver:

Merry A. Reasoning with !-graphs. [Internet] [Doctoral dissertation]. University of Oxford; 2013. [cited 2019 Jun 16]. Available from: http://ora.ox.ac.uk/objects/uuid:416c2e6d-2932-4220-8506-50e6b403b660 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.604414.

Council of Science Editors:

Merry A. Reasoning with !-graphs. [Doctoral Dissertation]. University of Oxford; 2013. Available from: http://ora.ox.ac.uk/objects/uuid:416c2e6d-2932-4220-8506-50e6b403b660 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.604414

.