Alex Hertel's Web Page


I recently completed my Ph.D. under the supervision of Dr. Alasdair Urquhart in the Department of Computer Science at the University of Toronto .

 

Contact Information:

  Department of Computer Science
University of Toronto
10 King's College Rd,
Sanford Fleming Building, Room 4306A
Toronto, Ontario, Canada
M5S 3G4
     
  E-Mail:

  

Résumé:

My Résumé is located here (.pdf) and here (.ps).

 

Conference & Journal Publications:

   

Algorithms & Complexity Results for Input & Unit Resolution, A. Hertel & A. Urquhart, Journal on Satisfiability, Boolean Modeling and Computation Volume 6, 2009, pages 141-164.
  Download: .pdf version .ps version
   

Game Characterizations and the PSPACE-Completeness of Tree Resolution Space, A. Hertel & A. Urquhart, Proceedings of CSL 2007: Springer LNCS 4646, pages 527-541.
  Download: .pdf version .ps version
   
Formalizing Dangerous SAT Encodings, A. Hertel, P. Hertel, & A. Urquhart, Proceedings of SAT 2007: Springer LNCS 4501, pages 159-172.
  Download: .pdf version .ps version
   
A Sound and Complete Proof Theory for Propositional Logical Contingencies, A. Hertel, P. Hertel, & C. Morgan, Notre Dame Journal of Formal Logic Vol. 48 No. 4, 2007, pages 521-530.
  Download: .pdf version .ps version
   

An O(pn+1.151p)-Algorithm for p-Profit Cover and its Practical Implications for Vertex Cover, U. Stege, I. van Rooij, A. Hertel, & P. Hertel, Proceedings ISAAC 2002: Springer LNCS 2518, pages 249-261.
  Download: .pdf version .ps version
   

 

Papers Submitted / in Progress:

   

The Resolution Width Problem is EXPTIME-Complete, A. Hertel & A. Urquhart, Withdrawn from Theory of Computing due to a bug in a proof.
  Download: .pdf version .ps version
   

The Proof Complexity of Intuitionistic Propositional Logic, A. Hertel & A. Urquhart, In Preparation.
  Download: .pdf version .ps version
   

A Non-Hamiltonicity Proof System, A. Hertel, In Preparation.
  Download: .pdf version .ps version See implementation below.
   

 

Unrefereed Papers:

Prover / Delayer Game Upper Bounds For Tree Resolution, A. Hertel & A. Urquhart,  2006.
  Download: .pdf version .ps version
   
A Survey & Strengthening of Barnette's Conjecture, A. Hertel, 2005.
  Download: .pdf version .ps version
   

 

Ph.D. & M.Sc. Theses:

Ph.D. Thesis: Applications of Games to Propositional Proof Complexity. A. Hertel, University of Toronto, Defended May 2nd, 2008.
  Download: .pdf version .ps version
   
Thesis Proposal Paper: Thesis Proposal: An Application of Game Characterizations to Propositional Proof Complexity, A. Hertel, University of Toronto, 2007.
  Download: .pdf version .ps version
   
Research Proposal Paper: Research Proposal & Progress Report, A. Hertel, University of Toronto, 2006.
  Download: .pdf version .ps version
   
Depth Oral (Candidacy) Paper: Propositional Proof Complexity: A Depth Oral Survey, A. Hertel, University of Toronto, 2005.
  Download: .pdf version .ps version
   
Master's Thesis: Hamiltonian Cycles in Sparse Graphs,  A. Hertel, University of Toronto, 2004.
  Download: .pdf version .ps version
  An implementation of the Stone Carver Algorithm together with some test graphs is located here.  This program also contains an implementation of a proof system for non-Hamiltonicity found in the paper "A Non-Hamiltonicity Proof System", above.

 

Graduate Course Papers & Projects:

Genome Assembly Algorithms for New Sequencing Technologies, A. Hertel & P. Hertel, 2006
Download: .pdf version .ps version
The implementation of the main algorithm together with test genomes is located here.
Machine Learning & the Automatizability of Proof Systems, A. Hertel & P. Hertel, 2005.
Download: .pdf version .ps version
Secure Electronic Elections, A. Hertel & P. Hertel, 2004.
Download: .pdf version .ps version
Collaborative Motion Graphs, A. Hertel & P. Hertel, 2003.
Download: .pdf version .ps version
The project implementation is located here.
Motion From Primitives Using Motion Graphs, A. Hertel & P. Hertel, 2002
Download: .pdf version .ps version
The project implementation is located here.

 

Other Stuff:

Here is a fractal-viewing program which allows you to zoom in on the Mandelbrot Set.
   

 

Read This!

Note that some of the programs above were programmed for Windows XP using C++ and MFC.  Disclaimer: for all I know, running any or all of these programs on your computer will cause the world to end; I assume no liability.  For that matter, reading any of the above papers may cause you to go blind and / or may cause your hard drive to to be erased, so don't come looking to sue me if you didn't heed this warning!