Certifying Standard and Stratified Datalog Inference Engines in SSReflect

ITP, pp. 171-188, 2017.

Cited by: 3|Bibtex|Views0|Links
EI

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments