My current research interests are in biometrics, automated reasoning and 3D information visualization. My work in biometrics is a continuation of the work I did for my post-doctoral fellowship and my work in automated reasoning follows from my dissertation. My interest in 3D information visualization began when teaching a computer graphics course at Bridgewater College in the spring of 2016.

I'm very grateful to be able to work with incredibly talented undergraduate students at Bridgewater College. Over the past 3 years I've had the privilege to work with 2 students on summer research projects and 3 students on their Honors projects. Below are descriptions of the recent work that we've done and where the projects are headed.

In this project, Tayseer extended my post-doctoral research by modifying the biometric software that I wrote to identify individuals using thoracic signals. The software is named Thoracic Identification System or TIS. Among the many modifications to the software that Tayseer made were a rewriting of the beat detection algorithm and the beat selection algorithm. Her modifications increased the carotid pulse identification rate from 23% to 63% (+40). She presented her results at the 2015 ASPIRE poster session and a eport was sent to the Intelligence Community agency that sponsored the original study.

In this work Troy performed an IRB approved data collection to collect carotid pulse signals from multiple subjects. Each of 15 subjects were tested in two sessions, with sessions approximately two weeks apart. During each session he collected pulse signals before and after exercise. Troy also worked on the software and increased the carotid pulse recognition rate to 65% (+2). He presented his work and results at the 2016 ASPIRE poster session. The data collected can be found on GitHub. This research was funded by a Research Experience @ Bridgewater College grant.

Dylan Tokotch's Honor project was originally titled “Normalizing Carotid Pulses Using Dynamic Time Warping (DTW) And It’s Use in Biometric Identification”. But shortly after the research began we found a paper which suggested that DTW was not helpful in thoracic biometric identification. So we changed course and instead of implementing DTW in the thoracic biometric software, Dylan implemented the heart beat detection algorithm written by Bridgewater College Mathematics Professor Dr. Verne Leininger and student Jose Corona for their 2015 Research Experience @ Bridgewater College grant. Dylan’s work resulted in an increased recognition rate of 69% (+4). We are currently writing a paper describing the heart beat detection algorithm and our results. We hope to submit it for publication in 2017.

In this project John and I created a JavaScript graph library called YAGL (pronouned 'yæ gəl) for the Babylon.js 3D framework. This library allows programmers to easily create and manipulate 3-dimensional graphs (nodes and edges) in a 3D Babylon scene and perform a few algorithms on the graph as described in our final report. We believe this library could be helpful in transmitting important visual information, such as disease transmission paths or disaster recovery routes, to a wide audience (anyone with a browser). The source code can be found on GitHub and a demonstration page can be found here. This research was funded by a 2016 Research Experience @ Bridgewater College grant.

In Spring 2017, the students above expanded the capabilities of YAGL to include directed graphs, weighted graphs, centrality measurements and created a new graphical user interface. Their work was presented at the 2017 A.S.P.I.R.E Poster Session. The new graphical user interface can be viewed here

For his Honor's Project and Senior Seminar, Trevor created a 3D simulation of an 8-bit computer using Unreal Engine 4. The simulation is similar to the design discussed in the text "But How Do It Know?" by J. Clark Scott and was inpired by the large scale Megaprocessor built by James Newman at Cambridge. As Trevor writes in his proposal, "the goal is to create a simulation that will help students learn and understand how a computer functions at a low level." His work can be viewed in the videos he produced and on his webpage.

My graduate thesis advisor, Dr. Christopher Lynch, and I are also currently working on an extension to my dissertation. In my dissertation we proposed an inference system called Γ+Λ. It allows pairs of inference systems (with restrictions of course) to be combined into a single inference system. This, for instance, can be used to combine the Inst-Gen-Eq (Instance Generation with equality) inference system with the Superposition inference. This new inference system, in theory, allows the solver to benefit from the strengths of each of the inference systems. We are finishing proofs that show Γ+Λ is sound and complete. We hope to have the paper finished before February 2017.

The goals of this research project were to determine biometric performance measurements for the acoustic, electrical and pulse signals produced by the heart, referred to as thoracic signals, and to identify if a relationship exists between the electrical and pulse signals. Our results can be found in our final report and the Thoracic Identification System was released as open source.

The first refutationally complete inference systems for first-order logic, called instance- based systems, were based on Herbrand’s theorem which implies that first-order logic sat- isfiability can be reduced to propositional logic satisfiability (SAT). Out of this line of research came the landmark SAT solving DPLL algorithm. Soon after DPLL made its debut, Robinson introduced the simple combinatorial resolution rule which detracted interest in instance-based systems. Recently, with the increase in computational power of the personal computer, there has been renewed interest in systems for first-order logic theorem proving that utilize SAT solvers. In my dissertation we present three novel solutions for the first-order logic validity problem that utilize SAT.