Bauer ’10 Solves Open Problem in Computability Logic
February 24, 2012
The Villanova University Department of Computing Science reports that graduate student Matt Bauer ’10, in the course of working on his master's thesis in computer science, "solved an open problem in Computability Logic, showing that the basic first-order fragments of it is PSPACE-complete. The nontrivial proof idea for this theorem was found by him independently, without any help or hints from the adviser. The result is exposed in A PSPACE-complete First-Order Fragment of Computability Logic, which has a good chance of being published in a decent professional journal, and is currently under review."
Bauer is a 2010 graduate of Arcadia University, majoring in Mathematics and Computer Science. He is employed full-time as a software engineer at Gnostech. Read about his undergraduate research on the computability of real functions with Dr. Xizhong Zheng, Assistant Professor of Computer Science at Arcadia. "The personal attention that I received from faculty at Arcadia really laid the foundation for me moving forward in my career."
"Doing research with faculty was my most valuable experience at Arcadia," Bauer adds. "It allowed me to develop closer bonds with my professors and to extend my knowledge far beyond what I learned in the classroom. My project with Dr. Zheng also lead to a joint publication that I had opportunity to present at the 10th annual Computability and Complexity in Analysis conference in China. This experience gave me a tremendous advantage when applying to graduate schools, and I received a scholarship to attend Villanova University."
“The skills, discipline and persistence that our students learn in conducting research are never lost or forgotten,” says Arcadia President Carl (Tobey) Oxholm III. "When you can successfully combine the creative imagination with the scientific method, that's when knowledge is created, and that's when our students realize that they will succeed in whatever career they choose. We are very proud of our faculty who live to transform our students each and every day."
Bauer's abstract: "In a recently launched research program for developing logic as a formal theory of (interactive) computability, several very interesting logics have been introduced and axiomatized. These fragments of the larger Computability Logic aim not only to describe "what" can be computed, but also provide a mechanism for extracting computational algorithms from proofs. Among the most expressive and fundamental of these is CL4, known to be (constructively) sound and complete with respect to the underlying computational semantics. Furthermore, the fragment of CL4 not containing blind quantifiers was shown to be decidable in polynomial space. The present work extends this result and proves that this fragment is, in fact, PSPACE-complete."