Building Decision Procedures in the Calculus of Inductive Constructions

DOI10.1007/978-3-540-74915-8_26zbMath1179.68135arXiv0707.1266OpenAlexW1628824908MaRDI QIDQ3608422

Jean-Pierre Jouannaud, Frédéric Blanqui, Pierre-Yves Strub

Publication date: 5 March 2009

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0707.1266

zbMATH Keywords

decision procedurestheorem proverscalculus of inductive constructions

Mathematics Subject Classification ID

Related Items (2)

CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ High-Level Theories

Uses Software

• Automath

This page was built for publication: Building Decision Procedures in the Calculus of Inductive Constructions