Updated 15 April 2018

Mr. Yue Li

Post Graduate Research Student (Sept. 2016 -- ) in Computer Science

Dependable Systems Group

School of Mathematical and Computer Sciences, Heriot-Watt University

Supervisor: Ekaterina Komendantskaya

Research Activity

(06/2017-) Proof theoretic study of coinductive invariants arsing from first-order Horn clause logic

A talk on this topic was given in Automated Reasoning Workshop 2018.

(03/2017-05/2017) Working on Productive Corecursion in Logic Programming

Formulated sufficient conditions that guarantees productivity of non-terminating logic programs, with a semi-decision algorithm for infinite regular terms that are SLD-computable at infinity.

The paper (joint with Ekaterina Komendantskaya) has been accepted for publication in Theory and Practice of Logic Programming --- the journal proceedings of ICLP 2017 in Melbourne.

A talk on this work was given on Scottish Theorem Proving Seminar .

(02/2017-03/2017) Developing Structural Resolution with Co-inductive Loop Detection

Developed operational semantics for co-S-resolution, and proved its soundness w.r.t. the greatest complete Herbrand model.

The paper is published in the EPTCS post-proceeding of CoALP-Ty'16 workshop.

The implementation is available on GitHub Co-inductive Structural Resolution.

(09/2016-01/2017) Implementing Structural Resolution

Besides the implementation, the operational semantics for structural resolution in the form of reduction rules was also developed, extending the original rewriting tree based operational semantics.

The work is discussed in the report Comparative Study of Search Strategies for Term-Matching and Unification Based Resolution in Prolog

The implementation is available on GitHub Structural Resolution in Prolog.

The background of the work is the CoALP project .