Name
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.
|
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11799573_25 | International Conference on Logic Programming/Joint International Conference and Symposium on Logic Programming |
Keywords | Field | DocType |
traditional herbrand semantics,coinductive logic programming language,rational term,logic programming,new operational semantics,operational semantics,coinductive logic programming,declarative semantics,novel formal operational semantics,logic program,lazy evaluation,fixed point | Functional logic programming,Operational semantics,Horn clause,Programming language,Computer science,Denotational semantics,Algorithm,Theoretical computer science,Logic programming,Game semantics,Well-founded semantics,Higher-order logic | Conference |
Volume | ISSN | ISBN |
4079 | 0302-9743 | 3-540-36635-0 |
Citations | PageRank | References |
31 | 1.51 | 14 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Luke Simon | 1 | 142 | 8.46 |
| Ajay Mallya | 2 | 150 | 8.77 |
| Ajay Bansal | 3 | 320 | 27.21 |
| Gopal Gupta | 4 | 1404 | 143.46 |