Automating inversion of inductive predicates in Coq

DOI10.1007/3-540-61780-9_64zbMATH Open1407.68433OpenAlexW1849370879MaRDI QIDQ4647573FDOQ4647573

Authors: Cristina Cornes, Delphine Terrasse 

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61780-9_64

Recommendations

• Nominal Inversion Principles
• Handcrafted inversions made operational on operational semantics
• scientific article; zbMATH DE number 512790
• Automatic proofs by induction in theories without constructors
• Types for Proofs and Programs

zbMATH Keywords

proof assistantlogic programminginductive definitionHorn clauseinductive type

Mathematics Subject Classification ID

Logic programming (68N17)

Cites Work

• Title not available (Why is that?)
• The calculus of constructions
• Title not available (Why is that?)
• Automating inversion of inductive predicates in Coq
• Automatizing termination proofs of recursively defined functions

Cited In (9)

• The theory of contexts for first order and higher order abstract syntax
• External and internal syntax of the \(\lambda \)-calculus
• Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts
• \(\pi\)-calculus in (Co)inductive-type theory
• An application of co-inductive types in Coq: verification of the alternating bit protocol
• Handcrafted inversions made operational on operational semantics
• Automating inversion of inductive predicates in Coq
• Nominal Inversion Principles
• Builtin types viewed as inductive families

Uses Software

• Coq

This page was built for publication: Automating inversion of inductive predicates in Coq

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