Rewriting modulo in deduction modulo

DOI10.1007/3-540-44881-0_28MaRDI QIDQ4447247zbMATH OpenFDO

Authors Frédéric Blanqui

Publication date 16 February 2004

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2706/27060395.htm

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Termination Modulo Combinations of Equational Theories
• scientific article; zbMATH DE number 3870640
• Dependency pairs for equational rewriting
• Termination modulo equations by abstract commutation with an application to iteration
• Modularity of termination and confluence in combinations of rewrite systems with _

Cited in

(7)

• Aligning concepts across proof assistant libraries
• Variants of the basic calculus of constructions
• Combining deduction modulo and logics of fixed-point definitions
• Algorithmic Equality in Heyting Arithmetic Modulo
• scientific article; zbMATH DE number 1231675 (Why is no real title available?)
• Sharing proofs with predicative theories through universe-polymorphic elaboration
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

This page was built for publication: Rewriting modulo in deduction modulo

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