ROS Theses Repository

View Item 
  •   ROS Home
  • Mathematical & Computer Sciences
  • Doctoral Theses (Mathematical & Computer Sciences)
  • View Item
  •   ROS Home
  • Mathematical & Computer Sciences
  • Doctoral Theses (Mathematical & Computer Sciences)
  • View Item
  •   ROS Home
  • Mathematical & Computer Sciences
  • Doctoral Theses (Mathematical & Computer Sciences)
  • View Item
  • Admin
JavaScript is disabled for your browser. Some features of this site may not work without it.

A proof-theoretic approach to coinduction in Horn clause logic

View/Open
LiY_0919_macs.pdf (678.7Kb)
Date
2019-09
Author
Li, Yue
Metadata
Show full item record
Abstract
The 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.
URI
http://hdl.handle.net/10399/4349
Collections
  • Doctoral Theses (Mathematical & Computer Sciences)

Browse

All of ROSCommunities & CollectionsBy Issue DateAuthorsTitlesThis CollectionBy Issue DateAuthorsTitles

ROS Administrator

LoginRegister
©Heriot-Watt University, Edinburgh, Scotland, UK EH14 4AS.

Maintained by the Library
Tel: +44 (0)131 451 3577
Library Email: libhelp@hw.ac.uk
ROS Email: open.access@hw.ac.uk

Scottish registered charity number: SC000278

  • About
  • Copyright
  • Accessibility
  • Policies
  • Privacy & Cookies
  • Feedback
AboutCopyright
AccessibilityPolicies
Privacy & Cookies
Feedback
 
©Heriot-Watt University, Edinburgh, Scotland, UK EH14 4AS.

Maintained by the Library
Tel: +44 (0)131 451 3577
Library Email: libhelp@hw.ac.uk
ROS Email: open.access@hw.ac.uk

Scottish registered charity number: SC000278

  • About
  • Copyright
  • Accessibility
  • Policies
  • Privacy & Cookies
  • Feedback
AboutCopyright
AccessibilityPolicies
Privacy & Cookies
Feedback