The computability path ordering

DOI10.2168/LMCS-11(4:3)2015zbMath1448.68253arXiv1506.03943MaRDI QIDQ3196359

Albert Rubio, Jean-Pierre Jouannaud, Frédéric Blanqui

Publication date: 29 October 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

reducibilityrewritingterminationinductive typeslambda-calculuspath order

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (7)

Size-based termination of higher-order rewriting ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Superposition for higher-order logic ⋮ A Lambda-Free Higher-Order Recursive Path Order ⋮ Unnamed Item ⋮ Superposition with lambdas ⋮ Superposition with lambdas

Uses Software

• Automath

This page was built for publication: The computability path ordering