Deciding Equality in the Constructor Theory

DOI10.1007/978-3-540-74464-1_6zbMATH Open1178.03022OpenAlexW1554187855MaRDI QIDQ3612437FDOQ3612437

Authors: Pierre Corbineau 

Publication date: 10 March 2009

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

Full work available at URL: https://doi.org/10.1007/978-3-540-74464-1_6

Recommendations

• Proving ground confluence and inductive validity in constructor based equational specifications
• scientific article; zbMATH DE number 3870639
• Publication:4938605
• Automatic proofs by induction in theories without constructors
• scientific article; zbMATH DE number 1538019

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Cited In (3)

• The constructive equality theory
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• A Declarative Language for the Coq Proof Assistant

Uses Software

• Coq

This page was built for publication: Deciding Equality in the Constructor Theory

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