Publications

HoCHC: a Refutationally-complete and Semantically-invariant System of Higher-order Logic Modulo Theories

We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC)—a system of higher-order logic modulo theories generalising (1st-order) constrained Horn clauses—and prove its soundness and refutational completeness w.r.t. both standard and Henkin semantics. As corollaries, HoCHC shares desirable properties (such as semi-decidability and a canonical model property) and deciable fragments with its 1st-order counterpart.

Talks

Recent & Upcoming

HoCHC: a Refutationally-complete and Semantically-invariant System of Higher-order Logic Modulo Theories

Theses

Resolution for Higher−Order Constrained Horn Clauses

Design and Implementation of a CDCL(LA) Calculus

Teaching

At the University of Oxford:

At Saarland University:

  • Teaching Assistant of Fundamentals of Algorithms and Data Structures (winter semester 2016 / 17)
  • Mentor of Mathematical Preparatory Course (Sep / Oct 2016 / 17)

Contact