Updated 05 July 2017
Post Graduate Research Student (Sept. 2016 -- ) in Computer Science
Dependable Systems Group
School of Mathematical and Computer Sciences, Heriot-Watt University
Supervisor: Ekaterina Komendantskaya
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 .
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.
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 .