| 2026 | FlAIRS | Interactive Solution Viewers for Automated Theorem Proving. | Daniel Li, Esteban Morales, Geoff Sutcliffe, Jack McKeown |
| 2026 | FlAIRS | ShZZaM - An LLM+ATP Natural Language to Logic Translator. | Geoff Sutcliffe, Danial Haroon |
| 2026 | IJCAR | Finite Model Finding in First-Order Modal Logics. | Happy Khairunnisa Sariyanto, Alexander Steen, Geoff Sutcliffe |
| 2025 | FlAIRS | Proof Verification with GDV and LambdaPi - It's a Matter of Trust. | Geoff Sutcliffe, Frdric Blanqui, Guillaume Burel |
| 2024 | IJCAR | Stepping Stones in the TPTP World. | Geoff Sutcliffe |
| 2024 | IJCAR | An Empirical Assessment of Progress in Automated Theorem Proving. | Geoff Sutcliffe, Christian B. Suttner, Lars Kotthoff, C. Raymond Perrault, Zain Khalid |
| 2023 | FlAIRS | Reinforcement Learning for Guiding the E Theorem Prover. | Jack McKeown, Geoff Sutcliffe |
| 2023 | FlAIRS | An Interactive Interpretation Viewer for Typed First-order Logic. | Jack McKeown, Geoff Sutcliffe |
| 2023 | LPAR | Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic. | Alexander Steen, Geoff Sutcliffe, Pascal Fontaine, Jack McKeown |
| 2020 | CADE | Evaluation of Axiom Selection Techniques. | Qinghua Liu, Zishi Wu, Zihao Wang, Geoff Sutcliffe |
| 2020 | CADE | Cutting Down the TPTP Language (And Others). | Nahku Saidy, Hanna Siegfried, Stephan Schulz, Geoff Sutcliffe |
| 2019 | CADE | GRUNGE: A Grand Unified ATP Challenge. | Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban |
| 2019 | CADE | JGXYZ: An ATP System for Gap and Glut Logics. | Geoff Sutcliffe, Francis Jeffry Pelletier |
| 2019 | TACAS | TOOLympics 2019: An Overview of Competitions in Formal Methods. | Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber, Akihisa Yamada |
| 2018 | CADE | TFX: The TPTP Extended Typed First-Order Form. | Geoff Sutcliffe, Evgenii Kotelnikov |
| 2018 | FlAIRS | Making Belnap's "Useful 4-Valued Logic" Useful. | Geoff Sutcliffe, Francis Jeffry Pelletier, Allen Hazen |
| 2017 | CADE | Detecting Inconsistencies in Large First-Order Knowledge Bases. | Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease |
| 2017 | FlAIRS | Automated Reasoning for the Dialetheic Logic RM3. | Geoff Sutcliffe, Francis Jeffry Pelletier, Allen P. Hazen |
| 2016 | CADE | TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. | Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe |
| 2016 | FlAIRS | Hoping for the Truth - A Survey of the TPTP Logics. | Geoff Sutcliffe, Francis Jeffry Pelletier |
| 2015 | CADE | Things You Can't do With a Vampire. | Geoff Sutcliffe |
| 2015 | LPAR | Automated Theorem Proving by Translation to Description Logic. | Negin Arhami, Geoff Sutcliffe |
| 2015 | LPAR | The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps. | Geoff Sutcliffe, Stephan Schulz |
| 2014 | CADE | The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics. | Negin Arhami, Geoff Sutcliffe |
| 2014 | CADE | Automated Theorem Proving using the TPTP Process Instruction Language. | Muhammad Nassar, Geoff Sutcliffe |
| 2014 | CADE | StarExec: A Cross-Community Infrastructure for Logic Solving. | Aaron Stump, Geoff Sutcliffe, Cesare Tinelli |
| 2012 | CADE | Introducing StarExec: a Cross-Community Infrastructure for Logic Solving. | Aaron Stump, Geoff Sutcliffe, Cesare Tinelli |
| 2012 | FlAIRS | SAMHT - Suicidal Avatars for Mental Health Training. | Cameron Carpenter, Leticia Osterberg, Geoff Sutcliffe |
| 2012 | LPAR | The TPTP Typed First-Order Form with Arithmetic. | Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Peter Baumgartner |
| 2011 | CADE | Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving. | Michael Schneider, Geoff Sutcliffe |
| 2011 | FlAIRS | Sporcle Goes AI. | Cameron Carpenter, Geoff Sutcliffe |
| 2010 | AISC | Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar. | Josef Urban, Geoff Sutcliffe |
| 2010 | CADE | Different Proofs are Good Proofs. | Geoff Sutcliffe, Cynthia Chang, Li Ding, Deborah L. McGuinness, Paulo Pinheiro da Silva |
| 2010 | FlAIRS | Progress Towards Effective Automated Reasoning with World Knowledge. | Geoff Sutcliffe, Martin Suda, Alexandra Teyssandier, Nelson Dellis, Gerard de Melo |
| 2010 | LPAR | The TPTP World - Infrastructure for Automated Reasoning. | Geoff Sutcliffe |
| 2009 | CADE | Divvy: An ATP Meta-system Based on Axiom Relevance Ordering. | Alex Roederer, Yury Puzis, Geoff Sutcliffe |
| 2009 | CADE | Progress in the Development of Automated Theorem Proving for Higher-Order Logic. | Geoff Sutcliffe, Christoph Benzmller, Chad E. Brown, Frank Theiss |
| 2009 | FlAIRS | Multiple Answer Extraction for Question Answering with Automated Theorem Proving Systems. | Geoff Sutcliffe, Aparna Yerikalapudi, Steven Trac |
| 2009 | KI | External Sources of Axioms in Automated Theorem Proving. | Martin Suda, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard de Melo |
| 2008 | CADE | THF0 - The Core of the TPTP Language for Higher-Order Logic. | Christoph Benzmller, Florian Rabe, Geoff Sutcliffe |
| 2008 | CADE | Evaluation of Systems for Higher-order Logic (ESHOL). | Christoph Benzmller, Florian Rabe, Carsten Schrmann, Geoff Sutcliffe |
| 2008 | CADE | The Annual SUMO Reasoning Prizes at CASC. | Adam Pease, Geoff Sutcliffe, Nick Siegel, Steven Trac |
| 2008 | CADE | Presenting TSTP Proofs with Inference Web Tools. | Paulo Pinheiro da Silva, Geoff Sutcliffe, Cynthia Chang, Li Ding, Nicholas Del Rio, Deborah L. McGuinness |
| 2008 | CADE | CASC-J4 The 4th IJCAR ATP System Competition. | Geoff Sutcliffe |
| 2008 | CADE | Integration of the TPTPWorld into SigmaKEE. | Steven Trac, Geoff Sutcliffe, Adam Pease |
| 2008 | CADE | MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance. | Josef Urban, Geoff Sutcliffe, Petr Pudlk, Jir Vyskocil |
| 2008 | LPAR | The SZS Ontologies for Automated Reasoning Software. | Geoff Sutcliffe |
| 2007 | CADE | First Order Reasoning on a Large Ontology. | Adam Pease, Geoff Sutcliffe |
| 2007 | CADE | SRASS - A Semantic Relevance Axiom Selection System. | Geoff Sutcliffe, Yury Puzis |
| 2007 | CSR | TPTP, TSTP, CASC, etc. | Geoff Sutcliffe |
| 2007 | LPAR | ATP Cross-Verification of the Mizar MPTP Challenge Problems. | Josef Urban, Geoff Sutcliffe |
| 2006 | CADE | Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. | Allen Van Gelder, Geoff Sutcliffe |
| 2006 | CADE | CASC-J3 - The 3rd IJCAR ATP System Competition. | Geoff Sutcliffe |
| 2006 | CADE | Using the TPTP Language for Writing Derivations and Finite Interpretations. | Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Allen Van Gelder |
| 2006 | FlAIRS | Automated Generation of Interesting Theorems. | Yury Puzis, Yi Gao, Geoff Sutcliffe |
| 2005 | FlAIRS | Reasoning in the Event Calculus Using First-Order Automated Theorem Proving. | Erik T. Mueller, Geoff Sutcliffe |
| 2005 | FlAIRS | Semantic Derivation Verification. | Geoff Sutcliffe, Diego Belfiore |
| 2004 | CADE | The CADE ATP System Competition. | Geoff Sutcliffe, Christian B. Suttner |
| 2003 | CADE | The CADE-19 ATP System Competition. | Geoff Sutcliffe, Christian B. Suttner |
| 2003 | FlAIRS | Proving Harder Theorems by Axiom Reduction. | Geoff Sutcliffe, Alexander Dvorsk |
| 2002 | CADE | System Description: GrAnDe 1.0. | Stephan Schulz, Geoff Sutcliffe |
| 2002 | FlAIRS | Homogeneous Sets of ATP Problems. | Matthias Fuchs, Geoff Sutcliffe |
| 2002 | ISAIM | Automatic Generation of Benchmark Problems for Automated Theorem Proving Systems. | Simon Colton, Geoff Sutcliffe |
| 2000 | CADE | System Description: PTTP+GLiDes: Semantically Guided PTTP. | Marianne Brown, Geoff Sutcliffe |
| 2000 | CADE | System Description: SystemOn TPTP. | Geoff Sutcliffe |
| 1999 | FlAIRS | Smart Selective Competition Parallelism ATP. | Geoff Sutcliffe, Darryl Seyfang |
| 1996 | CADE | The Design of the CADE-13 ATP System Competition. | Christian B. Suttner, Geoff Sutcliffe |
| 1996 | PRICAI | Using Artificial Neural Networks for Meteor-Burst Communications Trail Prediction. | Stuart Melville, Geoff Sutcliffe, David Fraser |
| 1994 | CADE | The TPTP Problem Library. | Geoff Sutcliffe, Christian B. Suttner, Theodor Yemenis |
| 1994 | MVA | An Intelligent Document Understanding & Reproduction System. | Michael Sharpe, Nizam Ahmed, Geoff Sutcliffe |
| 1993 | ICLP | Prolog-D-Linda v2: A New Embedding of Linda in SICStus Prolog. | Geoff Sutcliffe |
| 1993 | LPAR | A Comparison of Mechanisms for Avoiding Repetition of Subdeductions in Chain Formal Linear Deduction Systems. | Geoff Sutcliffe |
| 1992 | CADE | Linear-Input Subset Analysis. | Geoff Sutcliffe |
| 1992 | CADE | The Semantically Guided Linear Deduction System. | Geoff Sutcliffe |
| 1990 | CADE | A General Clause Theorem Prover. | Geoff Sutcliffe |