Certifying Standard and Stratified Datalog Inference Engines in SSReflect
ITP, pp. 171-188, 2017.
We propose a SSReflect library for logic programming in the Datalog setting. As part of this work, we give a first mechanization of standard Datalog and of its extension with stratified negation. The library contains a formalization of the model theoretical and fixpoint semantics of the languages, implemented through bottom-up and, respec...More
Full Text (Upload PDF)
PPT (Upload PPT)