scientific article; zbMATH DE number 2185672

MaRDI QIDQ3024848zbMATH OpenFDO

Authors Jaco van de Pol, Helmut Schwichtenberg

Publication date 4 July 2005

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03) Grammars and rewriting systems (68Q42)

Recommendations

• A termination ordering for higher order rewrite systems
• Semantic labelling for proving termination of combinatory reduction systems
• Normal higher-order termination
• scientific article; zbMATH DE number 1615229
• Higher-Order Orderings for Normal Rewriting

Cited in

(16)

• Higher-order rewrite systems and their confluence
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• Perpetual reductions in -calculus
• Non-strictly positive fixed points for classical natural deduction
• Termination Proofs for Recursive Functions in FoCaLiZe
• Normal higher-order termination
• The Computability Path Ordering: The End of a Quest
• Semantic labelling for proving termination of combinatory reduction systems
• scientific article; zbMATH DE number 88985 (Why is no real title available?)
• The variable containment problem
• Two \textit{different} strong normalization proofs?
• A recursive path ordering for higher-order terms in η-long β-normal form
• Polymorphic higher-order termination
• The practice of logical frameworks
• On the longest perpetual reductions in orthogonal expression reduction systems
• Verifying termination and reduction properties about higher-order logic programs

This page was built for publication:

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