Department of CS newsletter

Please join us for the March Atlas Talk! Details below:

Date: 1st March 2023

Time: 14:00 - 16:00

Venue:   Kilburn Theatre 1.3

Speaker:   Cláudia Nalon

Title:    From Global to Local: Reductions from the Modal Cube into K

Abstract: 

Modal logics are applied to represent and reason about a large variety of complex problems: from the formalisation of Mathematics and philosophical problems to applications in Computer Science and Engineering. Such applications might require specific extensions of modal logics that better represent constraints for a particular given domain, which can be achieved by adding to K (normality) the axioms B (symmetry), D (seriality), T (reflexivity), 4 (transitivity), and 5 (Euclideaness). The logics arising from these axioms and their combinations comprise what is known as the modal cube. 

Given the wide range of applications, the availability of automatic tools for reasoning about problems represented in these logics is highly desirable. But that is not the case. Although both model and proof theory for the considered logics are well developed and understood, there is a lack of automatic modal reasoners. Therefore, automated reasoning for modal logics often exploits the fact that their languages can be translated into stronger logics, as first-order logic, for which there are readily available, reliable provers. This is however problematic, as the translation might not retain complexity and might not even lead to a decision procedure.

In this talk, we will argue in the other direction: many modal logics can also be efficiently translated into weaker logics whilst preserving decidability and (often) complexity results. We provide translations directly into a clausal normal form for K which is suitable for automatic reasoning via modal resolution. Experimental evaluation with our own prover, KSP, shows that we can achieve good performance for all the logics in the modal cube. Other automated tools for local reasoning in K, whose availability is higher than those for specific modal logics, could also benefit from the techniques utilised in our translation.
 

Bio:

Cláudia Nalon is a full professor at the Department of Computer Science at the University of Brasília. Her research is focused on both the theoretical foundations and practical aspects related to the implementation of proof methods for non-classical logics and their combinations. She has developed and implemented proof systems for non-monotonic logics, many-valued logics, and for several modal logics (normal multimodal logics and their extensions, and parameterised multi-modal confluent logics; interacting epistemic and temporal modal logics; dynamic logics; non-normal modal logics for cooperative agency; preferential logics; etc).

Dear All

If you would like to invite a visitor to the Department, please send an email to csops@manchester.ac.uk so that we can send you the relevant forms and information. 

There can be significant delays due to ATAS processing times and queries from the Global Mobility Team, so please contact us at the earliest possible opportunity to start the process. 

Many thanks

Erika Buzink-Wallis

As part of the UKRI move to 'Simpler, Better Funding' (SBF), EPSRC are starting to move away from using the JeS application system to a new UKRI Funding Service.

Je-S will be closed to new applications from 30 March 2023 for the following schemes:

• EPSRC standard research grant
• EPSRC new investigator award
• EPSRC overseas travel grant
• EPSRC network grant
• EPSRC discipline-hopping in information and communications technologies
• EPSRC working with overseas scientists

with others to follow

Internal review deadline: noon on Friday 17-Feb-2023
External deadline: 11-Apr-2023

https://raeng.org.uk/programmes-and-prizes/programmes/uk-grants-and-prizes/support-for-research/chair-in-emerging-technologies
Chairs in Emerging Technologies are professorial appointments. Applicants who haven’t been awarded a Professorial title but have demonstrated research achievements such that they would be strongly considered for Professorial promotion at present, are eligible to apply, with awardees expected to gain a Professorial title upon award.

£2.5M is available over 10 years (5 years initially) with an annual payment of £250k per annum.
N.B. Resubmissions are now allowed (but must clearly articulate where modifications and improvements have been made based on feedback)
 
As per previous calls, there will be a light touch internal review process for submissions. Prospective applicants should submit a 2 page outline to daniel.twiddy@manchester.ac.uk cc’ing their RSM (sarah.chatwin@manchester.ac.uk) by noon on Friday 17th February 2023. Outlines will be reviewed by a Faculty panel and should detail the following:
 
1.      Strategic significance, relationship between the emerging technology and wider UK technological priorities
2.      Fit with University research and investment strategy
3.      Impact of research
4.      Plans for self-sustainability once RAEng funding has ended
  
Queries regarding applications to this scheme should be referred to your Research Support Manager (Sarah Chatwin) in the first instance.