Datalog is a lightweight logic programming language, based on the logic of Horn clauses. Lean, on the other hand, is a proof assistant system and language based on the Calculus of Inductive Constructions (CIC). Datalog is more constrained and less expressive than Lean but has a long history of established deduction algorithms. Writing definitions and queries in the Datalog fragment of Lean would be more succinct and understandable than writing them in Lean itself. This paper outlines the design and implementation of a shallow embedding of Datalog as a Domain Specific Language (DSL) on top of Lean. Bidirectional interoperability between the Datalog DSL and Lean is a primary goal of this design. In addition to rules and facts, backward chaining queries are automatically translated into theorems with tactic-based proofs. The paper also includes three simple examples of how the DSL can be used.

翻译：Datalog是一种基于Horn子句逻辑的轻量级逻辑编程语言。而Lean则是一种基于归纳构造演算(CIC)的证明助手系统与语言。Datalog虽比Lean更具约束性且表达能力较弱,但拥有悠久的成熟演绎算法历史。在Lean的Datalog片段中编写定义和查询比直接用Lean编写更为简洁易懂。本文概述了在Lean之上将Datalog作为领域特定语言(DSL)进行浅嵌入的设计与实现。Datalog领域特定语言与Lean之间的双向互操作性是本设计的核心目标。除规则和事实外,逆向链接查询会被自动转化为带有策略化证明的定理。文中还包含三个简单示例展示该领域特定语言的使用方法。