Strimko by Resolution

Summary

Develop a Strimko solver by repeated and systematic application of the resolution inference procedure.

Topics

Knowledge representation (propositional logic), logical inference (resolution), backtracking search, Python programming

Audience

Undergraduate students in an introductory AI class.

Difficulty

Being meant for undergraduates, this is a fairly straighforward project. The basic project (without extra credits) should not take more than a week between assignment and due date.

Strengths

This project allows students to get an integrated view of logical inference and backtracking search in a small and manageable problem (Strimko). It also encourages goal-oriented research into an advanced topic. By avoiding the use of a black-box SAT solver in the base project, the students get a "look under the hood" of logical reasoning.

Weaknesses

Some Strimko puzzles cannot be represented due to limitations in the GUI. However, the solver (when completed) will work for all Strimko puzzles. The demo version does not include backtracking search.

Dependencies

Students should be able to translate formal pseudocode as well as less formal instruction into program, and also follow pseudocode logic to be able to answer questions about it. Knowledge of Python required.

Variants

An in-class demo variant could be developed that lists the disjunctions on the GUI, and highlights reduction by resolution, guesses made for backtracking, etc., to demonstrate inferences incrementally.