Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic. - Johannes Niederhauser; Chad E. Brown; Cezary Kaliszyk (IJCAR (1), 2024)

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version). - Johannes Niederhauser; Chad E. Brown; Cezary Kaliszyk (CoRR, 2024)

The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting. - Johannes Niederhauser; Aart Middeldorp (CADE, 2025)

Left-Linear Completion with AC Axioms. - Johannes Niederhauser; Nao Hirokawa; Aart Middeldorp (Log. Methods Comput. Sci., 2025)

The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version). - Johannes Niederhauser; Aart Middeldorp (CoRR, 2025)