Building Decision Procedures in the Calculus of Inductive Constructions

DOI10.1007/978-3-540-74915-8_26zbMATH Open1179.68135arXiv0707.1266OpenAlexW1628824908MaRDI QIDQ3608422FDOQ3608422

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

Publication date: 5 March 2009

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

Abstract: It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof of a proposition P by the proof of an equivalent proposition P' obtained from P thanks to possibly complex calculations. In this paper, we investigate a new version of the calculus of inductive constructions which incorporates arbitrary decision procedures into deduction via the conversion rule of the calculus. The novelty of the problem in the context of the calculus of inductive constructions lies in the fact that the computation mechanism varies along proof-checking: goals are sent to the decision procedure together with the set of user hypotheses available from the current context. Our main result shows that this extension of the calculus of constructions does not compromise its main properties: confluence, subject reduction, strong normalization and consistency are all preserved.

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

Recommendations

• Inductive consequences in the calculus of constructions
• scientific article; zbMATH DE number 4014064
• scientific article; zbMATH DE number 4074451
• Types for Proofs and Programs
• A calculus for conditional inductive theorem proving
• A New Elimination Rule for the Calculus of Inductive Constructions
• scientific article; zbMATH DE number 1990014
• Ambient calculus and its logic in the calculus of inductive constructions
• Inductive Decidability Using Implicit Induction
• A compact kernel for the calculus of inductive constructions

zbMATH Keywords

decision procedurestheorem proverscalculus of inductive constructions

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Cited In (10)

• High-Level Theories
• A decision procedure for von Wright's OBS-calculus
• Computer Science Logic
• Automated Reasoning
• Constructive decision via redundancy-free proof-search
• Theory of types and decision procedures
• Inductive consequences in the calculus of constructions
• Title not available (Why is that?)
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Types for Proofs and Programs

Uses Software

• Automath

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3608422)