Coinduction in Uniform : Foundations for Corecursive Proof Search with Horn Clauses
- Submitting institution
-
Heriot-Watt University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 24889658
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-030-17184-1_28
- Title of conference / published proceedings
- Programming Languages and Systems : ESOP 2019
- First page
- 783
- Volume
- 11423
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Compliant
- Month of publication
- April
- Year of publication
- 2019
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Output of the Platform grant EP/N014758/1, this paper provides a calculus for infinitary computations in logic programming. The quest for it has been open since 1980s, with a number of candidate systems proposed, including CoLP(2007) and CoALP(2015), all of which were incomplete and lacking a proof-theoretic interpretation. This paper gives the first definitive calculus for coinductive proofs in Horn clause logic, generalising all of the previously available approaches and establishing its soundness relative to intuitionsitic logic and coalgebraic Herbrand models. ESOP is an A-rated international conference. The results of this paper constitute core of PhD thesis of Komendantskaya's student Li.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
