Certifying standard and stratified Datalog inference engines in SSReflect

DOI10.1007/978-3-319-66107-0_12zbMath1483.68057OpenAlexW2748190963MaRDI QIDQ1687733

Véronique Benzaken, Stefania Dumbrava, Evelyne Contejean

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_12

Mathematics Subject Classification ID

Database theory (68P15) Logic programming (68N17) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (1)

Certified Graph View Maintenance with Regular Datalog

Uses Software

• Coq
• Coq/SSReflect
• Yedalog

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Datalog in academia and industry. Second international workshop, Datalog 2.0, Vienna, Austria, September 11--13, 2012. Proceedings
• A lattice-theoretical fixpoint theorem and its applications
• Completeness and Decidability Results for CTL in Coq
• Point-Free, Set-Free Concrete Linear Algebra
• The Semantics of Predicate Logic as a Programming Language
• A Machine-Checked Proof of the Odd Order Theorem
• Programming Languages and Systems

This page was built for publication: Certifying standard and stratified Datalog inference engines in SSReflect