“Mo was an absolute pleasure to work with. He is a great leader and manager - he delivered many large scale projects across babylon. He is technically excellent and able to explain complex concepts to those less technical. He is supportive and really cared about his team. He always took the time to answer any difficult questions I had and pushed me to think outside the box- I thoroughly enjoyed our discussions.”
About
Intrigued and wholly persuaded by the transformative impact of advanced technologies on…
Experience
Education
-
The University of Manchester
-
Thesis: "Exploration of Variations of Unrestricted Blocking for Description Logics"
My doctoral research aimed to generate an automated tableau prover based on the specification of logic, supported by research grant EP/H043748/1 of the UK EPSRC. I focused on blocking techniques to help the provers terminate. This research contributed to a better understanding of the relation between the properties of a logic and its required minimal blocking criteria. -
-
Dissertation: “E-science Strategies for Interpreting Large-volume SNP Data from Next-generation Sequencing"
Graduated with distinction.
My graduate studies provided insight into a variety of topics from symbolic logic to machine learning and big data. Bridging this with large-scale bioinformatics was a valuable experience. In cooperation with Taverna and My-Grid, I developed a fully autonomous method for ranking SNPs for kettles in Africa, based on the existing ad hoc manual…Dissertation: “E-science Strategies for Interpreting Large-volume SNP Data from Next-generation Sequencing"
Graduated with distinction.
My graduate studies provided insight into a variety of topics from symbolic logic to machine learning and big data. Bridging this with large-scale bioinformatics was a valuable experience. In cooperation with Taverna and My-Grid, I developed a fully autonomous method for ranking SNPs for kettles in Africa, based on the existing ad hoc manual process, reducing the execution time from 6 days to 90 minutes. This was presented at the 11th Annual Bioinformatics Open Source Conference (BOSC) 2010 and GENOME INFORMATICS, Hinxton, September 2010.
Automated Reasoning, Computational Biology, BioHealth Informatics, Knowledge Representation, Machine Learning, Semi-Structured Data -
-
Licenses & Certifications
Publications
-
Controlling Applications of Blocking Rule
ARW 2013
We discuss modifications of the unrestricted blocking rule by means of additional side conditions and/or additional premises. The approach preserves the termination property of the calculus and reduces search space of tableau decision procedures based on the calculus. In the variation of tableau procedure which we consider, terms are immediately rewritten with respect to the equalities conjectured by the blocking rule.
Other authors -
-
A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI
Tableaux 2013
The paper shows that the description logic SHOI has the finite model property and presents a tableau calculus with several refinements for reasoning in SHOI. A novelty of the calculus is non-standard rules for dealing with TBox and RBox statements. Whereas in existing tableau approaches two fixed rules are used for dealing with TBox and RBox statements, our tableau calculus uses a dynamically generated set
of refined rules. Using this approach has become practical because reasoners with…The paper shows that the description logic SHOI has the finite model property and presents a tableau calculus with several refinements for reasoning in SHOI. A novelty of the calculus is non-standard rules for dealing with TBox and RBox statements. Whereas in existing tableau approaches two fixed rules are used for dealing with TBox and RBox statements, our tableau calculus uses a dynamically generated set
of refined rules. Using this approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover generation prototype MetTeL. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting, and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox elements from the application of blocking can be seen as two separate instances of this technique. Experiments show the refinements lead to fewer rule applications and improved performance.Other authors -
-
A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI
DL 2013
The paper shows that the description logic SHOI has the finite model property and presents a tableau calculus with several refinements for reasoning in SHOI. A novelty of the calculus is nonstandard rules for dealing with TBox and RBox statements. Whereas in existing tableau approaches two fixed rules are used for dealing with TBox and RBox statements, our tableau calculus uses a dynamically generated set of refined rules. Using this approach has become practical because reasoners with flexible…
The paper shows that the description logic SHOI has the finite model property and presents a tableau calculus with several refinements for reasoning in SHOI. A novelty of the calculus is nonstandard rules for dealing with TBox and RBox statements. Whereas in existing tableau approaches two fixed rules are used for dealing with TBox and RBox statements, our tableau calculus uses a dynamically generated set of refined rules. Using this approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover
generation prototype MetTeL. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting, and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox elements from the application of blocking can be seen as two separate instances of this technique. Experiments show the refinements lead to fewer rule applications and improved performance.Other authors -
-
The Tableau Prover Generator MetTeL2
Jelia 2012
This paper introduces MetTeL , a tableau prover generator producing Java code from the specification of a tableau calculus for a logical language. MetTeL is intended to provide an easy to use system for non-technical users and allow technical users to extend the generated
implementations.
Other authors -
-
MetTeL2: Towards a prover generation platform
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning (PAAR-2012)
Introduces MetTeL2, a tableau prover generator producing Java code from the specification of a logical syntax and a tableau calculus. It is intended to provide an easy to use system for non-technical users and allow technical users to extend the generated implementations.
Other authors -
-
Synthesizing and Implementing Tableau Calculi for Interrogative Epistemic Logics
PAAR 2012
This paper presents a labelled tableau approach for deciding interrogative-epistemic logics (IEL). Tableau calculi for these logics have been derived using a recently introduced tableau synthesis method. We also consider an extension of the framework for a setting
with questioning modalities over sequences of formulae called sequential questioning logic (SQL). We have implemented the calculi using two approaches. The rst implementation has been obtained with the tableau prover generation…This paper presents a labelled tableau approach for deciding interrogative-epistemic logics (IEL). Tableau calculi for these logics have been derived using a recently introduced tableau synthesis method. We also consider an extension of the framework for a setting
with questioning modalities over sequences of formulae called sequential questioning logic (SQL). We have implemented the calculi using two approaches. The rst implementation has been obtained with the tableau prover generation software MetTeL2, while the other implementation is a prover implemented in Haskell.Other authors -
-
An Abstract Tableau Calculus for the Description Logic SHOI Using Unrestricted Blocking and Rewriting
Proceedings of the 25th International Workshop on Description Logics (DL 2012)
This paper presents an abstract tableau calculus for the description logic SHOI. SHOI is the extension of ALC with singleton concepts, role inverse, transitive roles and role inclusion axioms. The presented tableau calculus is inspired by a recently introduced tableau synthesis framework. Termination is achieved by a variation of the unrestricted blocking mechanism that immediately rewrites terms with respect to the conjectured equalities. This approach leads to reduced search space for…
This paper presents an abstract tableau calculus for the description logic SHOI. SHOI is the extension of ALC with singleton concepts, role inverse, transitive roles and role inclusion axioms. The presented tableau calculus is inspired by a recently introduced tableau synthesis framework. Termination is achieved by a variation of the unrestricted blocking mechanism that immediately rewrites terms with respect to the conjectured equalities. This approach leads to reduced search space for decision procedures based on the calculus. We also discuss restrictions of the application of the blocking rule by means of additional side conditions and/or additional premises.
Other authors -
-
METTEL2: Towards a Prover Generation Platform
ARW 2012
This paper introduces METTEL2 , a tableau prover generator producing JAVA code from the specifications of a logical syntax and a tableau calculus. It is intended to provide an easy to use system for non-technical users and allow technical users to extend the implementation of generated provers.
Other authors -
-
Multi-Agent Interrogative-Epistemic Logics, Privacy, Sequential Queries and Tableau Reasoning
Manuscript
This paper presents three logical formalizations extending dynamic epistemic modal logic with multi-agent features. The first feature consists in considering interrogative components which are modelled by dynamic questioning modalities encoding model-changing operations. The multi-agent
aspects specific to these dynamic actions are captured using preconditions for executing questioning and resolution actions. The second feature consists in considering a special
kind of privacy of dynamic…This paper presents three logical formalizations extending dynamic epistemic modal logic with multi-agent features. The first feature consists in considering interrogative components which are modelled by dynamic questioning modalities encoding model-changing operations. The multi-agent
aspects specific to these dynamic actions are captured using preconditions for executing questioning and resolution actions. The second feature consists in considering a special
kind of privacy of dynamic actions. We formalise group opaque dynamic questioning effects via a new semantics accounting for the possibility that some agents are aware of interrogative-epistemic events taking place while other agents are oblivious to these events. The third feature extends the formalization to accommodate sequences of questioning actions. For all these logics we present sound and complete tableau calculi with the property that they can be used as finite model generators for any formulae with finite models. The presented calculi have been derived using
tableau synthesis methods.Other authors -
-
Terminating tableau calculi for modal logic K with global counting operators
Manuscript
This paper presents the first systematic treatment of tableau calculi for modal logic K with global counting operators. Using a recently introduced tableau synthesis framework we establish two terminating tableau calculi for the logic. Whereas the first calculus is a prefix tableau calculus, the second is a refinement that internalises the semantics of the logic without using nominals. We prove the finite model property for the logic and show that adding the unrestricted blocking mechanism does…
This paper presents the first systematic treatment of tableau calculi for modal logic K with global counting operators. Using a recently introduced tableau synthesis framework we establish two terminating tableau calculi for the logic. Whereas the first calculus is a prefix tableau calculus, the second is a refinement that internalises the semantics of the logic without using nominals. We prove the finite model property for the logic and show that adding the unrestricted blocking mechanism does not break soundness and completeness of the calculi and ensures termination in both cases. We have successfully implemented the prefix tableau calculus in the MetTeL tableau
prover generation platform.Other authors -
-
MetTeL: A Generic Tableau Prover
Tableaux 2011
MetTeL is a generic tableau prover for various modal, intuitionistic, hybrid, description and metric logic. The core component of MetTeL is a logic-independent tableau inference engine. A novel feature is that users have the ability to flexibly specify the set of tableau rules to be used in derivations. Termination can be achieved via a generalisation of a standard loop checking mechanism or unrestricted blocking.
Other authors -
-
METTEL: A Generic Tableau Prover
ARW 2011
METTEL is a generic tableau prover for various modal, description, hybrid, intuitionistic and metric logics. The core component of METTEL is a logic-independent tableau inference engine. A novel feature is that users have the ability to specify the set of tableau rules to be used in derivations. Termination can be achieved via a generalisation of a standard loop checking mechanism, or
unrestricted blocking.Other authors -
Patents
-
System for extracting semantic triples for building a knowledge base
Issued US US10482384B1
The present disclosure relates to a computer-implemented method of generating a semantic triple for building a knowledge base to include data patterns associated with semantic triples derived from unstructured text. The method includes providing a sentence associated with unstructured text including a main verb and a taxonomic verb, generating a first frame, generating a second frame, identifying a common sub-string in the first subject and either the second subject or the second object, or a…
The present disclosure relates to a computer-implemented method of generating a semantic triple for building a knowledge base to include data patterns associated with semantic triples derived from unstructured text. The method includes providing a sentence associated with unstructured text including a main verb and a taxonomic verb, generating a first frame, generating a second frame, identifying a common sub-string in the first subject and either the second subject or the second object, or a common sub-string in the first object and either the second subject or the second object; generating a semantic triple using the first frame and replacing the first subject or the first object having the common sub-string with the second subject or the second object having the common sub-string; and transmitting the semantic triple for inclusion as a data pattern in the knowledge base.
-
Computer Implemented Method for Extracting and Reasoning with Meaning from Text
Issued US US20200004832A1
A text processing method for improving the accuracy of a response to a query directed to a system comprising concepts and relations defined by a knowledge base, wherein the method comprises:
(i) producing a dependency tree from the query, wherein the dependency tree has at least one branch containing nodes and at least one connection between those nodes, wherein each node has a node label which corresponds to a term within the query, and wherein each connection has a label which corresponds…A text processing method for improving the accuracy of a response to a query directed to a system comprising concepts and relations defined by a knowledge base, wherein the method comprises:
(i) producing a dependency tree from the query, wherein the dependency tree has at least one branch containing nodes and at least one connection between those nodes, wherein each node has a node label which corresponds to a term within the query, and wherein each connection has a label which corresponds to the linguistic relationship between terms within the query;
(ii) from the dependency tree, generating a query concept using concepts and relations defined by the knowledge base;
(iii) checking if the query concept has a subsumption relationship with a candidate concept retrieved from the system, and if no subsumption relationship is initially identified, optimising the dependency tree by changing the nodes, followed by repeating steps (ii) and (iii);
and wherein the query concept and the candidate concept comprise at least one atomic concept. -
Method and system of combining knowledge stores
Issued US US20200004856A1
A computer implemented method of combining two knowledge bases, each knowledge base comprising concepts that are linked by relations, the method comprising:
assigning one of the knowledge bases as a first knowledge base and the other of said knowledge bases as an additional knowledge base;
matching concepts between the first knowledge base and the additional knowledge base to define mapping relations between concepts of the first and additional knowledge base;
assessing defined mapping…A computer implemented method of combining two knowledge bases, each knowledge base comprising concepts that are linked by relations, the method comprising:
assigning one of the knowledge bases as a first knowledge base and the other of said knowledge bases as an additional knowledge base;
matching concepts between the first knowledge base and the additional knowledge base to define mapping relations between concepts of the first and additional knowledge base;
assessing defined mapping relations to determine if they cause a violation with relations already present in the first or second knowledge base;
modifying relations within the additional knowledge base to repair violations; and
storing an extended first knowledge base comprising the first knowledge base, the defined mapping relations and the additional knowledge base with the modified relations within the additional knowledge base. -
Adding new electronic events into an electronic user profile using a language-independent data format
US 16/353,816
-
Computing device for logging changes in a person's mood over time
US PN834693US
-
Identifying valid medical data for facilitating accurate medical diagnosis
US PN832005US
-
Reducing a search space for a match to a query
US PN831993US
Honors & Awards
-
UK Tech exceptional talent residency
Tech city
Being selected as one of the 200 yearly batch of exceptional talent to stay and contribute to the UK technology sector.
-
Sirius Programme for graduate entrepreneurs
UK Trade & Investment
48£k funding and 12 month mentorship
-
EPSRC Doctoral Scholarship
The Engineering and Physical Sciences Research Council
Languages
-
English
Full professional proficiency
-
Persian
Native or bilingual proficiency
Recommendations received
31 people have recommended Mo
Join now to viewOther similar profiles
Explore collaborative articles
We’re unlocking community knowledge in a new way. Experts add insights directly into each article, started with the help of AI.
Explore More