Better modelling of rich theories

Description

The reasoning program FINDER (Finite Domain Enumerator) has been around for over 20 years. It takes as input a many-sorted first order theory, in a user-friendly format, and generates (small) finite models of that theory if there are any. When it was written it was sufficiently cutting-edge to solve open problems in discrete maths and win a prize for the best paper at IJCAI in 1993, but it has since been overtaken by two generations of more modern solvers, and its limitations are now a handicap.

This project aims to replace FINDER with a completely new piece of software, keeping or enhancing the external functionality but with a contemporary high-performance SMT solver inside the wrapper. The new software should not only be an effective stand-alone reasoner, but should be capable of serving as the back end of the Logic for Fun website, enhancing that tool for the purposes of teaching, and should also be capable of being integrated into a first order theorem prover so as to provide semantic guidance for proof search. Using an SMT solver will give us access to a rich language, especially including arithmetic.

As an honours project, the goal would be to master the theory and practice of modern SMT reasoning, to integrate an existing open source SMT solver into a wrapper accepting similar input to that of FINDER and perhaps to see the resulting system replace FINDER behind Logic for Fun. As a project at the PhD or MPhil level, the goal would be to go on from there to investigate the use of SMT for model-guided theorem proving, to put together a prover which advances the state of the art in reasoning over some range of first order problems and to carry out a program of experimental research into semantic guidance techniques including (but not limited to) dynamic semantic resolution.

Requirements

Programming skills. Many solvers are written in C++, so familiarity with that would be very useful. Knowledge of elementary logic is also essential.

Background Literature

For the ancient background: John Slaney, 'FINDER: Finite Domain Enumdrator - Sysyem Description', Proceedings of the 12th International Conference on Automated Deduction (CADE), 1994: 798-801.

For background on SMT (SAT Modulo Theories), see the Wikipedia entry as a starting point.

For a description of Logic for Fun, see John Slaney, 'Logic Considered Fun', Proceedings of the 4th International Conference on Tools for Teaching Logic (TTL), 2015: 215-222.<br/>http://ttl2015.irisa.fr/TTL2015_proceedings.pdf.

For semantically guided theorem proving using FINDER, start with John Slaney, Arnold Binas and David Price, 'Guiding a theorem prover with soft constraints', Proceedings of the European Conference on Artificial Intelligence (ECAI), 2004: 221-225.

Keywords

first-order logic

constraint satisfaction

satisfiability

SMT

automated reasoning

Updated:  1 November 2018/Responsible Officer:  Head of School/Page Contact:  CECS Marketing