Coinductive logic programming

Luke Simon, Ajay Mallya, Ajay Bansal, Gopal Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

44 Citations (Scopus)

Abstract

We extend logic programming's semantics with the semantic dual of traditional Herbrand semantics by using greatest fixed-points in place of least fixed-points. Executing a logic program then involves using coinduction to check inclusion in the greatest fixed-point. The resulting coinductive logic programming language is syntactically identical to, yet semantically subsumes logic programming with rational terms and lazy evaluation. We present a novel formal operational semantics that is based on synthesizing a coinductive hypothesis for this coinductive logic programming language. We prove that this new operational semantics is equivalent to the declarative semantics. Our operational semantics lends itself to an elegant and efficient goal directed proof search in the presence of rational terms and proofs. We describe a prototype implementation of this operational semantics along with applications of coinductive logic programming.

Original languageEnglish (US)
Title of host publicationLogic Programming - 22nd International Conference, ICLP 2006, Proceedings
PublisherSpringer Verlag
Pages330-345
Number of pages16
ISBN (Print)9783540366355
StatePublished - Jan 1 2006
Externally publishedYes
Event22nd International Conference on Logic Programming, ICLP 2006 - Seattle, WA, United States
Duration: Aug 17 2006Aug 20 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4079 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other22nd International Conference on Logic Programming, ICLP 2006
CountryUnited States
CitySeattle, WA
Period8/17/068/20/06

Fingerprint

Logic programming
Logic Programming
Operational Semantics
Semantics
Fixed point
Programming Languages
Coinduction
Proof Search
Computer programming languages
Formal Semantics
Term
Logic Programs
Inclusion
Prototype
Evaluation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Simon, L., Mallya, A., Bansal, A., & Gupta, G. (2006). Coinductive logic programming. In Logic Programming - 22nd International Conference, ICLP 2006, Proceedings (pp. 330-345). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4079 LNCS). Springer Verlag.

Coinductive logic programming. / Simon, Luke; Mallya, Ajay; Bansal, Ajay; Gupta, Gopal.

Logic Programming - 22nd International Conference, ICLP 2006, Proceedings. Springer Verlag, 2006. p. 330-345 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4079 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Simon, L, Mallya, A, Bansal, A & Gupta, G 2006, Coinductive logic programming. in Logic Programming - 22nd International Conference, ICLP 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4079 LNCS, Springer Verlag, pp. 330-345, 22nd International Conference on Logic Programming, ICLP 2006, Seattle, WA, United States, 8/17/06.
Simon L, Mallya A, Bansal A, Gupta G. Coinductive logic programming. In Logic Programming - 22nd International Conference, ICLP 2006, Proceedings. Springer Verlag. 2006. p. 330-345. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Simon, Luke ; Mallya, Ajay ; Bansal, Ajay ; Gupta, Gopal. / Coinductive logic programming. Logic Programming - 22nd International Conference, ICLP 2006, Proceedings. Springer Verlag, 2006. pp. 330-345 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{ff63d16450a34cfb878961fde6148e03,
title = "Coinductive logic programming",
abstract = "We extend logic programming's semantics with the semantic dual of traditional Herbrand semantics by using greatest fixed-points in place of least fixed-points. Executing a logic program then involves using coinduction to check inclusion in the greatest fixed-point. The resulting coinductive logic programming language is syntactically identical to, yet semantically subsumes logic programming with rational terms and lazy evaluation. We present a novel formal operational semantics that is based on synthesizing a coinductive hypothesis for this coinductive logic programming language. We prove that this new operational semantics is equivalent to the declarative semantics. Our operational semantics lends itself to an elegant and efficient goal directed proof search in the presence of rational terms and proofs. We describe a prototype implementation of this operational semantics along with applications of coinductive logic programming.",
author = "Luke Simon and Ajay Mallya and Ajay Bansal and Gopal Gupta",
year = "2006",
month = "1",
day = "1",
language = "English (US)",
isbn = "9783540366355",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "330--345",
booktitle = "Logic Programming - 22nd International Conference, ICLP 2006, Proceedings",

}

TY - GEN

T1 - Coinductive logic programming

AU - Simon, Luke

AU - Mallya, Ajay

AU - Bansal, Ajay

AU - Gupta, Gopal

PY - 2006/1/1

Y1 - 2006/1/1

N2 - We extend logic programming's semantics with the semantic dual of traditional Herbrand semantics by using greatest fixed-points in place of least fixed-points. Executing a logic program then involves using coinduction to check inclusion in the greatest fixed-point. The resulting coinductive logic programming language is syntactically identical to, yet semantically subsumes logic programming with rational terms and lazy evaluation. We present a novel formal operational semantics that is based on synthesizing a coinductive hypothesis for this coinductive logic programming language. We prove that this new operational semantics is equivalent to the declarative semantics. Our operational semantics lends itself to an elegant and efficient goal directed proof search in the presence of rational terms and proofs. We describe a prototype implementation of this operational semantics along with applications of coinductive logic programming.

AB - We extend logic programming's semantics with the semantic dual of traditional Herbrand semantics by using greatest fixed-points in place of least fixed-points. Executing a logic program then involves using coinduction to check inclusion in the greatest fixed-point. The resulting coinductive logic programming language is syntactically identical to, yet semantically subsumes logic programming with rational terms and lazy evaluation. We present a novel formal operational semantics that is based on synthesizing a coinductive hypothesis for this coinductive logic programming language. We prove that this new operational semantics is equivalent to the declarative semantics. Our operational semantics lends itself to an elegant and efficient goal directed proof search in the presence of rational terms and proofs. We describe a prototype implementation of this operational semantics along with applications of coinductive logic programming.

UR - http://www.scopus.com/inward/record.url?scp=33749319976&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33749319976&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:33749319976

SN - 9783540366355

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 330

EP - 345

BT - Logic Programming - 22nd International Conference, ICLP 2006, Proceedings

PB - Springer Verlag

ER -