Coinductive Uniform Proof and its Soundness: Revealing a General Coinduction Property of Horn Clauses

Yue Li
Heriot-Watt University

Wednesday 24 July 2019
14:15 - 15:15
Room EM 1.70


I will introduce Coinductive Uniform Proof (CUP), its soundness properties, and the proof of the soundness properties. For an overview of CUP, I will define the language of CUP called Horn clause, and give the inference rules of Uniform Proof (without coinduction). Horn clauses will be introduced following a narrowing process, starting from the language of first-order predicate logic, then narrow it to Harrop formula, then further narrow to hereditary Harrop formula , then Core formula and finally Horn clause. Next, I will explain what it means for a proof to be Uniform. After these basic set-up, I will introduce the notion of coinduction in the setting of logic programming. Then the idea of CUP will be introduced. Afterwards, the proof of CUP's soundness will be explained incrementally, starting with a simple case and then moving on to the general case. By the simple case I will present the central techniques of the proof, and by the general case I will explain how the techniques developed for the simple case are reused with necessary generalisation. By the end of the talk the listener should have an impression about the formal languages related to CUP, the way of reasoning in CUP, and how to prove the soundness of CUP.

Host: Katya Komendantskaya