Skip to main content

Logical reduction of higher-order Horn clauses


Suitable for

MSc in Computer Science
Mathematics and Computer Science, Part C
Computer Science and Philosophy, Part C
Computer Science, Part C


"The goal of this project is to study the logical redundancy of sets of higher-order Horn clauses. In particular, we want to know whether certain infinite sets of higher-order Horn clauses can be reduced to minimal finite sets. This work has implications for the field of program induction where higher-order Horn clauses are used as a form of inductive bias. This work is purely theoretical and builds on two existing papers [1,2]

[1] Cropper A., Tourret S. (2018) Derivation Reduction of Metarules in Meta-interpretive Learning. In: Riguzzi F., Bellodi E., Zese R. (eds) Inductive Logic Programming. ILP 2018. Lecture Notes in Computer Science, vol 11105. Springer, Cham [2] Cropper A., Muggleton S.H. (2015) Logical Minimisation of Meta-Rules Within Meta-Interpretive Learning. In: Davis J., Ramon J. (eds) Inductive Logic Programming. Lecture Notes in Computer Science, vol 9046. Springer, Cham"

Prerequisites: strong knowledge of mathematical logic and computational logic