Building Decision Procedures in the Calculus of Inductive Constructions

DOI10.1007/978-3-540-74915-8_26MaRDI QIDQ3608422zbMATH OpenOpenAlexFDO

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)

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

zbMATH Keywords

calculus of inductive constructionsdecision procedurestheorem provers

Mathematics Subject Classification ID

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

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.

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

Cited in

(10)

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

Describes a project that uses

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)