Exploring First-Order Models
Many automated reasoning tools for first-order logic produce interpretations of first-order signatures (i.e. "implementations" of functions and predicates). These interpretations can be rather large. Build a tool with which a first-order interpretation can be explored interactively, perhaps using a graph drawing tool such as Dot. This tool could be used for research purposes as well as educational purposes (when teaching people about logic).
Background: Intro.FP, Datastructures, First-order logic. Number of people: 1. Contact person: Koen