There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners

DOI10.1007/978-3-662-48899-7_23zbMath1471.68318OpenAlexW2253333731MaRDI QIDQ3460064

Alexander Steen, Christoph Benzmüller

Publication date: 12 January 2016

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-48899-7_23

Mathematics Subject Classification ID

Data structures (68P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Making higher-order superposition work ⋮ Making higher-order superposition work

Uses Software

• Beluga
• TPTP
• Twelf
• Abella
• QMLTP
• LeoPARD
• Teyjus

This page was built for publication: There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners