[1] He began his research in the field of automated theorem proving, developing both SL-resolution[2] with Donald Kuehner and the connection graph proof procedure.

[3] He developed SLD resolution and the procedural interpretation of Horn clauses,[4] which underpin the operational semantics of backward reasoning in logic programming.

[12][13] This work led to the demonstration with Phan Minh Dung and Francesca Toni that most logics for default reasoning can be regarded as special cases of assumption-based argumentation.

In his 2011 book, Computational Logic and Human Thinking - How to be Artificially Intelligent,[17] he argues that the use of computational logic can help ordinary people to improve their natural language communication skills, and that in combination with decision theory, it can be used to improve their practical problem-solving abilities.

The authors' seminal article, "The British Nationality Act as a Logic Program," published in 1986 in the Communications of the ACM journal, is one of the first and best-known works in computational law, and one of the most widely cited papers in the field.