Developing and certifying Datalog optimizations in coq/mathcomp.

Pierre-Léo Bégay Pierre Crégut Jean-François Monin

Published in: CPP (2021)

Keyphrases

expressive power
query answering
logic programming
deductive databases
neural network
query language
transitive closure
real time
high level
data structure
data integration
theorem prover
formal methods