Issues in machine-checking the decidability of implicational ticket entailment
scientific article; zbMATH DE number 6833566