Uploaded June 2017 | Updated September 2026, 1 hour ago
This talk was given by undergraduate Mark Molinaro during the 11th Annual Computer Science Undergraduate Research Symposium in 2016. Mark‘s research was supervised by Dr. David Plaisted.
“Exploring the Efficiency of First-Order Proving Methods”
Many automated theorem proving applications rely on the DPLL algorithm for deciding the satisfiability of a set of propositional logic formulae. For first-order logic formulae, ground clauses within the Herbrand universe may be exhaustively enumerated below an incrementing size-bound and fed as input to DPLL. From even a cursory investigation of these enumerated clauses, it is evident that many of them have multiple repeated terms. Here, we explore a potential method for exploiting the size-bound by “cheating in” larger clauses with many repeating terms that may be relevant to the proof.
Mark Mollinaro is a junior computer science major and research assistant within the Carolina Institute for Developmental Disabilities. He is left-handed and his favorite candy is M&M’s.
cs.unc.edu/academics/undergraduate/symposium/symposium-2017/
This talk was given by undergraduate Mark Molinaro during the 11th Annual Computer Science Undergraduate Research Symposium in 2016. Mark‘s research was supervised by Dr. David Plaisted.
“Exploring the Efficiency of First-Order Proving Methods”
Many automated theorem proving applications rely on the DPLL algorithm for deciding the satisfiability of a set of propositional logic formulae. For first-order logic formulae, ground clauses within the Herbrand universe may be exhaustively enumerated below an incrementing size-bound and fed as input to DPLL. From even a cursory investigation of these enumerated clauses, it is evident that many of them have multiple repeated terms. Here, we explore a potential method for exploiting the size-bound by “cheating in” larger clauses with many repeating terms that may be relevant to the proof.
Mark Mollinaro is a junior computer science major and research assistant within the Carolina Institute for Developmental Disabilities. He is left-handed and his favorite candy is M&M’s.
cs.unc.edu/academics/undergraduate/symposium/symposium-2017/
