Show simple item record

dc.contributor.advisorKomendantskaya, Dr Ekaterina
dc.contributor.advisorLawson, Professor Mark V.
dc.contributor.authorLi, Yue
dc.date.accessioned2021-10-15T10:06:45Z
dc.date.available2021-10-15T10:06:45Z
dc.date.issued2019-09
dc.identifier.urihttp://hdl.handle.net/10399/4349
dc.description.abstractThe thesis is on coinduction in Horn clauses. Specifically, it considers productive corecursion, and presents a framework called Coinductive Uniform Proof as a principled approach to coinduction in first-order Horn clause logic. It addresses the challenges of 1) discovering sufficient conditions for logic programs to be productive, 2) providing an explanation of why unification (without occur-check) between goals in a SLD derivation can be exploited to capture productive corecursion, and 3) identifying the principle that unifies the diverse approaches to Horn clause coinduction which are scattered across the literature. The thesis advances the state of the art by 1) providing a sufficient condition for productive corecursion which requires that a logic program does not admit perpetual term-rewriting steps nor existential variables, 2) showing that the goal-unification technique can be used to capture productive corecursion if a goal is no less general than some previous goal to which it unifies, and 3) defining a coinductively sound proof construction method for Horn clauses where a Horn clause to be proved is first asserted as an assumption and then used for its own proof.en
dc.language.isoenen
dc.publisherHeriot-Watt Universityen
dc.publisherMathematical and Computer Sciencesen
dc.titleA proof-theoretic approach to coinduction in Horn clause logicen
dc.typeThesisen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record