CIS Seminar: Zachary Ernst
"Automata for Discovering First-Order Models with Infinite Domains"
Wednesday, September 29, 3:00 p.m.
235 Weir Hall
Dr. Zachary Ernst, Research Professor
Center for Intelligence and Security Studies (CISS)
Abstract: A number of open problems in logic involve showing that a formula is not a theorem of a logic. Their solution will typically require the discovery of a countermodel. Although finite model finders such as SEM, Mace4, and Paradox have produced many original and publishable results, there is no practical system for discovering countermodels with infinite domains. Dr. Ernst will present a new approach using tree automata, and which uses existing finite model finders to specify models having infinite domains.
Bio: Dr. Ernst is a new member of the Center for Intelligence and Security Studies (CISS), having just left the University of Missouri-Columbia, where he was was an Associate Professor of Philosophy. His published work is mainly in game theory, rational choice theory, logic, and the philosophy of science. He worked for several years while in graduate school for the Mathematics and Computer Science Division of Argonne National Labs, where he worked on automated reasoning.