The field of automated reasoning has a legacy of interest in representing human inference. As formalized mathematics in automated reasoning grew more developed, however, connections to human inference were sometimes de-emphasized. My work may be seen as an attempt to re-unite these elements in automated reasoning. Seen from a different perspective, it was also an attempt to understand more about cognitive inference by grounding it in rigorous formalized mathematics.
Narrowly construed, my research was about creating formalized tactics for representing and implementing calculational logic inference. There was a particular focus on student inference, opening up issues in expert/novice distinctions. More generally, however, the research was about modeling high-level cognitive inference in highly structured logical contexts. The results are described in my dissertation, Tactic-Based Modeling of Cognitive Inference on Logically Structured Notation. The fundamental ideas are not system-specific.
Arriving at a formalized mathematical explanation of calculational logic required substantial creative and analytical effort. Presented in the book A Logical Approach to Discrete Mathematics (authors: David Gries and Fred Schneider), calculational logic supports reasoning about metalinguistic operations (such as textual substitution) without resorting to higher-order logic. It was not initially clear that this non-standard calculational approach could be explained using conventional semantic methods. Stuart Allen and I reported our analysis of calculational logic in our paper Justifying calculational logic by a conventional metalinguistic semantics. It was a significant innovation to realize calculational logic as a formalized metalogic.
For another aspect of my research, I experimentally studied the eye movements of students as they constructed calculational logic proofs. Such studies seem like an important tool for improving the descriptive accuracy of inference models. Some of my results are reported in Insight Into Theorem Proving via Eye Movements (co-author: Michael Spivey). The role of visual attention in high-level cognitive inference is a rich topic for further research; my work merely scratched the surface.