| 2024 | ISAIM | Partial Boolean Functions for QBF Semantics. | Allen Van Gelder |
| 2023 | WoLLIC | Subsumption-Linear Q-Resolution for QBF Theorem Proving. | Allen Van Gelder |
| 2013 | CP | Primal and Dual Encoding from Applications into Quantified Boolean Formulas. | Allen Van Gelder |
| 2013 | SAT | Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. | Florian Lonsing, Uwe Egly, Allen Van Gelder |
| 2012 | CP | Contributions to the Theory of Practical Quantified Boolean Formula Solving. | Allen Van Gelder |
| 2012 | SAT | Extended Failed-Literal Preprocessing for Quantified Boolean Formulas. | Allen Van Gelder, Samuel B. Wood, Florian Lonsing |
| 2012 | VDA | Vortex core detection: back to basics. | Allen Van Gelder |
| 2011 | CP | Variable Independence and Resolution Paths for Quantified Boolean Formulas. | Allen Van Gelder |
| 2011 | IJCAI | A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas. | Alexandra Goultiaeva, Allen Van Gelder, Fahiem Bacchus |
| 2011 | SAT | Careful Ranking of Multiple Solvers with Timeouts and Ties. | Allen Van Gelder |
| 2011 | SAT | Generalized Conflict-Clause Strengthening for Satisfiability Solvers. | Allen Van Gelder |
| 2010 | SAT | Zero-One Designs Produce Small Hard SAT Instances. | Allen Van Gelder, Ivor T. A. Spence |
| 2009 | SAT | Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces. | Allen Van Gelder |
| 2008 | AAAI | Clause Learning Can Effectively P-Simulate General Propositional Resolution. | Philipp Hertel, Fahiem Bacchus, Toniann Pitassi, Allen Van Gelder |
| 2008 | ISAIM | Verifying RUP Proofs of Propositional Unsatisfiability. | Allen Van Gelder |
| 2007 | SAT | Verifying Propositional Unsatisfiability: Pitfalls to Avoid. | Allen Van Gelder |
| 2006 | CADE | Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. | Allen Van Gelder, Geoff Sutcliffe |
| 2006 | CADE | Using the TPTP Language for Writing Derivations and Finite Interpretations. | Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Allen Van Gelder |
| 2006 | SAT | Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs. | Allen Van Gelder |
| 2005 | LPAR | Independently Checkable Proofs from Decision Procedures: Issues and Progress. | Allen Van Gelder |
| 2005 | LPAR | Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning. | Allen Van Gelder |
| 2005 | SAT | Input Distance and Lower Bounds for Propositional Resolution Proof Length. | Allen Van Gelder |
| 2002 | ISAIM | Generalizations of Watched Literals for Backtracking Search. | Allen Van Gelder |
| 2002 | ISAIM | Extracting (Easily) Checkable Proofs from a Satisfiability Solver that Employs both Preorder and Postorder Resolution. | Allen Van Gelder |
| 2002 | SCA | Model-based reconstruction for creature animation. | Maryann Simmons, Jane Wilhelms, Allen Van Gelder |
| 1999 | CGI | Volume Decimation of Irregular Tetrahedral Grids. | Allen Van Gelder, Vivek Verma, Jane Wilhelms |
| 1997 | SIGGRAPH | Varying spring constants for accurate simulation of elastic materials. | Allen Van Gelder, Jane Wilhelms |
| 1997 | SIGGRAPH | Anatomically based modeling. | Jane Wilhelms, Allen Van Gelder |
| 1996 | CADE | Partitioning Methods for Satisfiability Testing on Large Formulas. | Tai Joon Park, Allen Van Gelder |
| 1993 | PODS | Multiple Join Size Estimation by Virtual Domains. | Allen Van Gelder |
| 1992 | ICDT | Optimizing Active Databases using the Split Technique. | Serge Abiteboul, Allen Van Gelder |
| 1992 | PODS | The Well-Founded Semantics of Aggregation. | Allen Van Gelder |
| 1991 | PODS | Termination Detection in Logic Programs using Argument Sizes. | Kirack Sohn, Allen Van Gelder |
| 1991 | SIGGRAPH | A coherent projection approach for direct volume rendering. | Jane Wilhelms, Allen Van Gelder |
| 1990 | LPNMR | A New Form of Circumscription for Logic Programs (Extended Abstract). | Allen Van Gelder |
| 1990 | PODS | Deriving Constraints Among Argument Sizes in Logic Programs. | Allen Van Gelder |
| 1989 | PODS | The Alternating Fixpoint of Logic Programs with Negation. | Allen Van Gelder |
| 1988 | PODS | Unfounded Sets and Well-Founded Semantics for General Logic Programs. | Allen Van Gelder, Kenneth A. Ross, John S. Schlipf |
| 1987 | PODS | Safety and Correct Translation of Relational Calculus Formulas. | Allen Van Gelder, Rodney W. Topor |
| 1986 | FOCS | Parallel Complexity of Logical Query Programs | Jeffrey D. Ullman, Allen Van Gelder |
| 1986 | ICLP | Design Overview of the NAIL! System. | Katherine A. Morris, Jeffrey D. Ullman, Allen Van Gelder |
| 1986 | SIGMOD | A Message Passing Framework for Logical Query Evaluation. | Allen Van Gelder |
| 1984 | CADE | A Satisfiability Tester for Non-Clausal Propositional Calculus. | Allen Van Gelder |