Skip navigation
The Australian National University

Student research opportunities

Practical deduction via dynamic semantic resolution

Project Code: CECS_970

This project is available at the following levels:
Please note that this project is only for higher degree (postgraduate) applicants.


automated reasoning logic theorem proving


Professor John Slaney


This is a project in the field of automated reasoning. We shall take the very old idea of letting resolution be guided by models discovered at runtime (dynamic semantic resolution) [1], implement it fully and efficiently, and experiment with the use of different model-generation techniques in place of the SAT-like ones which have been tried to date. In particular, we shall attempt to use the model elimination calculus [2] to provide the semantics. This promises to advance the state of the art in reasoning for first order problems which are "essentially propositional", falling into the fragment of logic known as the "Bernays-Schoenfinkel" fragment or "disjunctive datalog". Many problems arising from real applications of reasoning are of this sort, and existing automatic reasoners find them difficult.
The project requires skills in programming and experimentation as well as aptitude for logic. It offers an opportunity to get quickly to the forefront of research in automated reasoning, and to advance the state of the art in an aspect of reasoning that really matters.

Goals of this project

A full implementation of dynamic semantic resolution within an existing high-performance theorem prover
Integration with instance-based reasoning by using a model elimination prover as the semantic component
Experimental validation especially on disjunctive datalog problems

Background Literature

[1] John Slaney. SCOTT: a model-guided theorem prover. Proceedings of the International Joint Conference on Artificial Intelligence (1993): 109-115.
[2] Peter Baumgartner and Cesare Tinelli. The model evolution calculus as a first-ordser DPLL method. Artificial Intelligence, 172 (2008): 591-632.




Updated:  10 August 2015 / Responsible Officer:  JavaScript must be enabled to display this email address. / Page Contact:  JavaScript must be enabled to display this email address. / Powered by: Snorkel 1.4