Publications

Drafts

[pdf]	Sean McLaughlin Thesis Proposal Practical Automated Theorem Proving with the Polarized Inverse Method
[pdf]	Sean McLaughlin and Frank Pfenning Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. Submitted to CADE 2009

[7]	Sean McLaughlin and Frank Pfenning Imogen: Focusing the Polarized Focused Inverse Method for Intuitionistic Propositional Logic LPAR 2008
[6]	Sean McLaughlin and Thomas C. Hales A Proof of the Dodecahedral Conjecture Accepted to the Journal of the American Mathematical Society
[5]	Sean McLaughlin An Interpretation of Isabelle/HOL in HOL Light IJCAR 2006, Lecture Notes in Computer Science, Springer, 2006.
[4]	Sean McLaughlin, John Harrison A Proof-Producing Decision Procedure for Real Arithmetic CADE-20, LNCS, Springer, 2005.
[3]	Sean McLaughlin, Clark Barrett, Yeting Ge Cooperating Theorem Provers: A Case Study Combining CVC Lite and HOL Light PDPAR 2005, Electronic Notes in Theoretical Computer Science, Elsevier, 2005.
[2]	Jim Grundy, Tom Melham, Sava Krstic, Sean McLaughlin Requirements for an API to First-Order Solvers PDPAR 2005, Electronic Notes in Theoretical Computer Science, Elsevier, 2005.
[1]	Kathy Bohrer, Xuan Liu, Sean McLaughlin, Edith Schonberg, Moninder Singh Objected Oriented XML Query by Example In Conceptual Modeling for Novel Application Domains, Lecture Notes in Computer Science, Springer, 2003.

[2]	Sean McLaughlin and Frank Pfenning The Inverse Method with Constraints APS4, at LPAR, 2008.
[1]	Florian Rabe, Christoph Lange and Sean McLaughlin Flyspeck in a Semantic Wiki -- Collaborating on a Large Scale Formalization of the Kepler Conjecture SemWiki, at MKM 2008.