Structural Resolution

This page supports the EPSRC grant Coalgebraic Logic Programming for Type Inference: parallelism and corecursion for a new generation of programming languages for parallelism and corecursion, 2013-2017. Joint with John Power, University of Bath.

A Breif Description

This research project arose from our studies of coalgebraic semantics for logic programming and SLD-resolution. That work resulted in a few papers introducing "Coalgebraic Logic Programming (CoALP)" in 2010-11 (you can find those few papers below). CoALP helped us to discover a method of ``Structural Resolution" - a proof method hybrid between Term-rewriting and First-order resolution. As such, it allows to give a structural reformulation for proof-search algorithms in logic programming and related automated provers. (You can find more details in a few introductory papers published in 2015 and given below).

Currently, the project investigates:

  1. ...whether Structural resolution can make Automated Theorem Proving better:
  2. And whether this will bring more precise methods of operational semantics to automated proof search, leading to richer coinductive algorithms.

  3. ... whether structural resolution can enrich programming language design via new Type Inference algorithms.

    P.Fu, E.Komendantskaya, T.Schrijvers, A.Pond. Proof Relevant Corecursive Resolution Accepted to FLOPS'2016, Japan, 3-6 March 2016.

See also: Workshop on Type inference and Automated Proving, 12 May 2015.

Past and Present Project members:

  1. Katya Komendantskaya, University of Dundee, PI
  2. John Power, University of Bath, co-PI
  3. Peng Fu, University of Dundee, RA
  4. Frantisek Farka, PhD student
  5. Jonathan Heras, University of Rioja, former RA
  6. Martin Schmidt, University of Osnabrueck, visiting PhD student
  7. Vladimir Komendantsky, Moixa UK , London, former RA
  8. Andrew Pond, University of Dundee, internship student

Project partners:

  1. Davide Ancona, Genova University
  2. Tarmo Uustalu, Tallinn University of Technology
  3. Kevin Hammond, University of St Andrews
  4. Neil Ghani,University of Strathclyde
  5. Gopal Gupta, University of Texas at Dallas

Project Software and Prototype Implementations

Structural resolution: three-tier calculus for proofs in first-order Horn logic programming, semi-decision for productivity of logic programs via guardednes checks.