Sen Zheng

郑森
Room 2.100, Kilburn Building,
Dept. Computer Science, Univ. Manchester
Oxford Rd, Manchester M13 9PL, UK

Email: firstname.lastname@manchester.ac.uk

Biography

I am a postdoctoral research associate in the autonomy and verification group at the University of Manchester, investigating formal verification for swarm robotics, reporting to Prof. Michael Fisher and Prof. Clare Dixon. Previous to that, I completed my PhD in the formal methods group at the University of Manchester, supervised by Dr. Renate A. Schmidt and Dr. Giles Reger. I obtained my MSc degree at the same university and completed my bachelor's degree at Northwestern Polytechnical University in China. In my PhD, I developed saturation-based Boolean conjunctive query answering and rewriting procedures for guarded first-order fragments. In general my interests are in applying automated reasoning techniques to solve real-world problems, including

Publications

[23c] Sen Zheng, Michael Fisher, and Clare Dixon. Using the temporal monodic clique-guarded negation fragment to specify swarm properties. 2023. Accepted at the Workshop on First-order Modal and Temporal Logics: State of the Art and Perspectives (FOMTL'23).
paper   slides
[23b] Saturation-based querying procedures for the clique-guarded negation fragment. Sen Zheng and Renate A. Schmidt, Presented at the Workshop on the Decision Problem in First-Order Logic (DPFO'23).
paper   slides
[23a] Resolution-based Boolean conjunctive query answering and rewriting for guarded quantification fragments. Sen Zheng and Renate A. Schmidt, Journal of Automated Reasoning, accepted.
[20b] Querying the guarded fragment via resolution (Extended Abstract). Sen Zheng and Renate A. Schmidt, in Proc. PAAR’20, volume 2752 of CEUR Workshop Proceedings, pages 167--177. CEUR-WS.org, 2020.
paper   slides
[20a] Deciding the loosely guarded fragment and querying its Horn Fragment using resolution. Sen Zheng and Renate A. Schmidt, in Proc. AAAI'20. AAAI Press, 3080--3087. (oral, travelling sponsored by AAAI)
paper   slides   poster
[19] Querying clique guarded existential rules. Sen Zheng and Renate A. Schmidt, in Proc. ARW'19. Univ. Middlesex, 7--8.
paper   slides   poster
[18] Towards polynomial time forgetting and instance query rewriting in ontology languages. Sen Zheng and Renate A. Schmidt, in Proc. ARW'18. Univ. Cambridge, 35--36.
paper   slides   poster

Research Duties

Reviewer: KR'23, KR'21, DL'19.
PC: AAAI'24, IJCAI'23, AAAI'23, IJCAI'22, IJCAI'21, ECAI'20.

Teaching Duties

2020/2021 Spring COMP60332 Automated Reasoning and Verification Teaching Assistant (TA)
2020/2019/2017 Spring COMP28112 Distributed Computing TA
2018/2017 Autumn COMP16121 Object Oriented Programming with Java 1 TA
2018/2017 Autumn COMP16122 Object Oriented Programming with Java 2 TA
2018 Autumn COMP23111 Fundamentals of Databases TA
2018 Winter Logic School for College Students co-Lecturer (with Warren). Slides can be found here.
2018 Summer SAT/SMT/AR International Summer School Volunteer
Last modified: July 2023