# Blog Post on Harrop Clauses and Scoped Dynamic Databases

**URL:** <https://swi-prolog.discourse.group/t/blog-post-on-harrop-clauses-and-scoped-dynamic-databases/6468>\
**Category:** Discussion\
**Created:** [April 17, 2023, 4:13am UTC](https://swi-prolog.discourse.group/t/blog-post-on-harrop-clauses-and-scoped-dynamic-databases/6468 "2023-04-17T04:13:03Z")\
**Posts on this page:** 1\
**Showing post:** 3

<div class="post-metadata">

**Author:** ![philzook58](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/philzook58/32/4342_2.png) [@philzook58](https://swi-prolog.discourse.group/u/philzook58)\
**Post date:** [April 17, 2023, 2:56pm UTC](https://swi-prolog.discourse.group/t/blog-post-on-harrop-clauses-and-scoped-dynamic-databases/6468/3 "2023-04-17T14:56:39Z")

</div>

I don’t tend to think of lambda prolog as being persay in the same arena as Coq/Agda/Lean, although it is a possible perspective. It is a programming language like prolog, just with support for some interesting logically motivated features. Now, since these features are inspired “computation=proof search” and improve the treatment of binding forms, it can make lambda prolog a more suitable place to do interactive or automatic theorem proving like activities than regular prolog. See [https://www.site.uottawa.ca/~afelty/dist/lprolog97.pdf](https://www.site.uottawa.ca/~afelty/dist/lprolog97.pdf)

ELPI [GitHub - LPCIC/elpi: Embeddable Lambda Prolog Interpreter](https://github.com/LPCIC/elpi) is a lambda prolog interpreter that was built as a metaprogramming language for Coq.

What my blog post is trying to do is understand if it is possible to get the meat of the extra things lambda prolog brings to the table as a library in prolog.

---

_[View the full topic](https://swi-prolog.discourse.group/t/blog-post-on-harrop-clauses-and-scoped-dynamic-databases/6468)._