# Logical reduction of higher-order Horn clauses

## Supervisor

## Suitable for

## Abstract

"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