Practical deduction via dynamic semantic resolution

Research areas

Temporary Supervisor

Professor John Slaney

Description

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

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:  1 June 2019/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing