Contents


General

Personal

Personal

Name Geoff Sutcliffe
Date of birth 28 October 1961
Place of birth N'dola, Zambia
Citizenship Australia and United Kingdom
Residency USA (Green Card)
Education

Education

1992 PhD University of Western Australia (Thesis: A Linear Deduction System with Integrated Semantic Guidance)
1986 MSc University of Natal (Thesis: Computerised Representation and Manipulation of Graphs)
1983 BSc (Hons) University of Natal
Employment

Employment

2014- Professor University of Miami, USA.
2001-2014 Associate Professor University of Miami, USA.
1996-2000 Senior Lecturer (Associate Professor) James Cook University, Australia.
2000 spring Visiting Associate Professor University of Miami, USA.
1993-1995 Lecturer (Assistant Professor) James Cook University, Australia.
1986-1992 Lecturer (Assistant Professor) Edith Cowan University, Australia.
1985 Lecturer University of Durban/Westville, South Africa.
1981-1985 Tutor (Teaching Assistant) University of Natal, South Africa.

Research

Research Interests

Research Interests

: Publications

Invited Talks

2024 Invited speaker: Stepping Stones in the TPTP World 12th International Joint Conference on Automated Reasoning (Nancy, France).
2024 Invited speaker: The TPTP World - Infrastructure for Automated Reasoning, International Symposium on Artificial Intelligence and Mathematics 2024, (Ft Lauderdale, USA).
2023 Invited talk: TPTP World Standards and Tools for Tarskian and Kripke Interpretations, Dagstuhl Seminar 23471: The Next Generation of Deduction Systems: from Composition to Compositionality (Schloss Dagstuhl, Germany).
2022 Invited speaker: The Logic Languages of the TPTP World, 8th Workshop on Practical Aspects of Automated Reasoning, (Haifa, Israel).
2021 Invited talk: The TPTP World - Infrastructure for Automated Reasoning, Coloquio Nacional de Intelligencia Artificial (Online, YouTube).
2019 Invited talk: The TPTP World - Infrastructure for Automated Reasoning, Czech Institute of Informatics, Robotics and Cybernetics (Prague, Czech Republic, YouTube).
2019 Invited talk: The CADE ATP System Competition, TOOLympics at TACAS'19 (Prague, Czech Republic).
2015 Invited speaker: Things that you can't do with a Vampire, 2nd Vampire Workshop (Berlin, Germany).
2015 Lecturer: The TPTP World - Infrastructure for Automated Reasoning, 11th Reasoning Web Summer School (Berlin, Germany).
2014 Invited speaker: The TPTP Process Instruction Language, 11th International Workshop on User Interfaces for Theorem Provers (Vienna, Austria).
2014 Invited speaker: QED and the TPTP World, Twenty Years of the QED Manifesto (Vienna, Austria).
2014 Invited speaker: The TPTP Typed First-order Form with Arithmetic: The Language and Some Applications, 6th Podlasie Conference on Mathematics (Bialystok, Poland).
2010 Invited speaker: The TPTP World - Infrastructure for Automated Reasoning, 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning (Dakar, Senegal).
2009 Invited speaker: Evaluating Automated Theorem Proving Systems, AAAI Spring Symposium on Benchmarking of Qualitative Spatial and Temporal Reasoning Systems (Stanford, USA).
2008 Invited speaker: Management and Analysis of ATP System Proofs, New Waves in Philosophy of Mathematics (Miami, USA).
2007 Invited speaker: TPTP, TSTP, CASC, etc., 2nd International Computer Science Symposium in Russia (Ekaterinburg, Russia).
2007 Invited speaker: SRASS - a Semantic Relevance Axiom Selection System, 14th Automated Reasoning Workshop (London, United Kingdom).
2003 Panelist: SMT-LIB - The Satisfiability Modulo Theories Library, Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 19th International Conference on Automated Deduction (Miami, USA).
2003 Invited speaker: A Grand Challenge of Theorem Discovery, Workshop on Challenges and Novel Applications for Automated Reasoning, 19th International Conference on Automated Deduction (Miami, USA).
2002 Invited speaker: Mathematics in the TPTP Problem Library, Special Session on Automated Reasoning in Mathematics and Logic, 2002 AMS and MAA Spring Southeastern Section Meetings (Atlanta, USA).
2001 Panelist: Artificial Intelligence Competitions, Boon or Bane?, 17th International Joint Conference on Artificial Intelligence (Seattle, USA).
2001 Panelist: Benchmark Libraries and Algorithm Competitions, Workshop on Empirical Methods in Artificial Intelligence, 17th International Joint Conference on Artificial Intelligence (Seattle, USA).
2001 Invited speaker: Evaluation of 1st Order ATP Systems, Workshop on Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, International Joint Conference on Automated Reasoning (Siena, Italy).
: Publications

Invited Publications

Sutcliffe G. (2024), Stepping Stones in the TPTP World, Benzmüller C., Heule M., Schmidt R., Proceedings of the 12th International Joint Conference on Automated Reasoning (Nancy, France) To appear.
Sutcliffe G. (2016), Things You Can't do With a Vampire, Kovacs L., Voronkov A., Proceedings of the 1st and 2nd Vampire Workshops (Berlin, Germany), EPiC Series in Computing 38, 8-28.
Sutcliffe G. (2010), The TPTP World - Infrastructure for Automated Reasoning, Clarke E., Voronkov A., Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning (Dakar, Senegal), Lecture Notes in Artificial Intelligence 6355, 1-12, DOI 10.1007/978-3-642-17511-4_1.
Sutcliffe G. (2007), TPTP, TSTP, CASC, etc., Diekert V., Volkov M., Voronkov A., Proceedings of the 2nd International Computer Science Symposium in Russia (Ekaterinburg, Russia), Lecture Notes in Computer Science 4649, 7-23, DOI 10.1007/978-3-540-74510-5_4.
Sutcliffe G. (2006), Report on the 19th International FLAIRS Conference, AI Magazine 27(4), 111-112.
Sutcliffe G., Gao Y., Colton S. (2003), A Grand Challenge of Theorem Discovery, Gow J. Walsh T. Colton S. Sorge V., Proceedings of the Workshop on Challenges and Novel Applications for Automated Reasoning, 19th International Conference on Automated Reasoning (Miami, USA), 1-11. (PDF)
Sutcliffe G. (2002), Review of: Newborn M., Automated Theorem Proving: Theory and Practice, AI Magazine (Spring 2002), 121-122.

Journal Publications

Sutcliffe G., Desharnais M. (2024), The 29th CADE Automated Theorem Proving System Competition - CASC-29, AI Communications, To appear.
Sutcliffe G. (2023), The Logic Languages of the TPTP World, Logic Journal of the IGPL 31(6), 1153-1169, DOI 10.1093/jigpal/jzac068.
Sutcliffe G., Desharnais M. (2023), The 11th IJCAR Automated Theorem Proving System Competition - CASC-J11, AI Communications 36(2), 73-91, DOI 10.3233/AIC-220244.
Benzmüller C., Fuenmayor D., Steen A., Sutcliffe G. (2023), Who Finds the Short Proof? An Exploration of Boolos' Curious Inference using Higher-order Automated Theorem Proving, Logic Journal of the IGPL, DOI 10.1093/jigpal/jzac082.
Fu H., Liu J., Wu G., Xu Y., Sutcliffe G. (2022), Improving Probability Selection Based Weights for Satisfiability Problems, Knowledge-Based Systems 245, DOI 10.1016/j.knosys.2022.108572.
Sutcliffe G., Desharnais M. (2022), The CADE-28 Automated Theorem Proving System Competition - CASC-28, AI Communications 34(4), 259-276, DOI 10.3233/AIC-210235
Beeson M, Bonancina M.P., Kinyon M., Sutcliffe G. (2022), Larry Wos - Visions of Automated Reasoning, Journal of Automated Reasoning 66(4), 439-461, DOI 10.1007/s10817-022-09620-8.
Sutcliffe G. (2021), The 10th IJCAR Automated Theorem Proving System Competition - CASC-J10, AI Communications 34(2), 163-177.
Sutcliffe G. (2020), The CADE-27 Automated Theorem Proving System Competition - CASC-27, AI Communications 32(5-6), 373-389.
Sutcliffe G. (2018), The 9th IJCAR Automated Theorem Proving System Competition - CASC-J9, AI Communications 31(6), 495-507.
Sutcliffe G. (2017), The CADE-26 Automated Theorem Proving System Competition - CASC-26, AI Communications 30(6), 419-432, DOI 10.3233/AIC-170744.
Sutcliffe G. (2017), The TPTP Problem Library and Associated Infrastructure - From CNF to TH0, TPTP v6.4.0, Journal of Automated Reasoning 59(4), 483-502, DOI 10.1007/s10817-017-9407-7.
Sutcliffe G. (2016), The 8th IJCAR Automated Theorem Proving System Competition - CASC-J8, AI Communications 29(5), 607-619, DOI 10.3233/AIC-160709.
Sutcliffe G. (2016), The CADE ATP System Competition - CASC, AI Magazine 37(2), 99-101, DOI 10.1609/aimag.v37i2.2620.
Sutcliffe G., Urban J. (2016), The CADE-25 Automated Theorem Proving System Competition - CASC-25, AI Communications 29(3), 423-433, DOI 10.3233/AIC-150691.
Sutcliffe G. (2015), The 7th IJCAR Automated Theorem Proving System Competition - CASC-J7, AI Communications 28(4), 683-692.
Schulz S., Sutcliffe G. (2015), Proof Generation for Saturating First-Order Theorem Provers, Delahaye D., Woltzenlogel Paleo B., All about Proofs, Proofs for All, Mathematical Logic and Foundations 55, College Publications, 45-61.
Sutcliffe G. (2014), The CADE-24 Automated Theorem Proving System Competition - CASC-24, AI Communications 27(4), 405-416.
Brown C.H., Mohr D., Gallo C., Mader C., Palinkas L., Wingood G., Prado G., Kellam S., Pantin H., Poduska J., Gibbons R., McManus J., Ogihara M., Valente T., Wulczyn F., Czaja S., Sutcliffe G., Villamar J., Jacobs C. (2013), A Computational Future for Preventing HIV in Minority Communities: How Advanced Technology Can Improve Implementation of Effective Programs, Journal of Acquired Immune Deficiency Syndromes 63(S), 72-84.
Sutcliffe G. (2013), The 6th IJCAR Automated Theorem Proving System Competition - CASC-J6, AI Communications 26(2), 211-223, DOI 10.3233/AIC-130550.
Urban J., Rudnicki P., Sutcliffe G. (2013), ATP and Presentation Service for Mizar Formalizations, Journal of Automated Reasoning 50(2), 229-241, DOI 10.1007/s10817-012-9269-y.
Sutcliffe G. (2012), The CADE-23 Automated Theorem Proving System Competition - CASC-23, AI Communications 25(1), 49-63, DOI 10.3233/AIC-2012-0512.
Sutcliffe G. (2011), The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5, AI Communications 24(1), 75-89.
Sutcliffe G., Benzmüller C. (2010), Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure Journal of Formalized Reasoning 3(1), 1-27, DOI 10.6092/issn.1972-5787/1710.
Pease A., Sutcliffe G., Siegel N., Trac S. (2010), Large Theory Reasoning with SUMO at CASC, AI Communications 23(2-3), 137-144, DOI 10.3233/AIC-2010-0466.
Sutcliffe G. (2010), The CADE-22 Automated Theorem Proving System Competition - CASC-22, AI Communications 23(1), 47-60, DOI 10.3233/AIC-2010-0469.
Urban J., Sutcliffe G., Trac S., Puzis Y. (2009), Combining Mizar and TPTP Semantic Presentation and Verification Tools, Studies in Logic, Grammar and Rhetoric, Special Issue on Computer Reconstruction of the Body of Mathematics 18(31), 121-136.
Sutcliffe G. (2009), The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0, Journal of Automated Reasoning 43(4), 337-362, DOI 10.1007/s10817-009-9143-8.
Hoefner P., Struth G., Sutcliffe G. (2009), Automated Verification of Refinement Laws, Annals of Mathematics and Artificial Intelligence 55(1), 35-62, DOI 10.1007/s10472-009-9151-8.
Urban J., Sutcliffe G. (2009), ATP-based Cross Verification of Mizar Proofs: Method, Systems, and First Experiments, Mathematics in Computer Science 2(2), 231-251, DOI 10.1007/s11786-008-0053-7
Sutcliffe G. (2009), The 4th IJCAR Automated Theorem Proving System Competition - CASC-J4, AI Communications 22(1), 59-72, DOI 10.3233/AIC-2009-0441.
Rabe F., Pudlak P., Sutcliffe G., Shen W. (2009), Solving the $100 Modal Logic Challenge, Journal of Applied Logic 7(1), 113-130, DOI 10.1016/j.jal.2007.07.007.
Sutcliffe G. (2008), The CADE-21 Automated Theorem Proving System Competition, AI Communications 21(1), 71-82.
Sutcliffe G. (2007), The 3rd IJCAR Automated Theorem Proving Competition, AI Communications 20(2), 117-126.
Sutcliffe G. (2006), Semantic Derivation Verification: Techniques and Implementation, International Journal on Artificial Intelligence Tools 15(6), 1053-1070, DOI 10.1142/S0218213006003119.
Sutcliffe G. (2006), The CADE-20 Automated Theorem Proving Competition, AI Communications 19(2), 173-181.
Sutcliffe G., Suttner, C. (2006), The State of CASC, AI Communications 19(1), 35-48.
Sutcliffe G. (2005), The IJCAR-2004 Automated Theorem Proving Competition, AI Communications 18(1), 33-40.
Sutcliffe G., Suttner C.B. (2004), The CADE-19 ATP System Competition, AI Communications 17(3), 103-110.
Sutcliffe G., Zimmer J., Schulz S. (2004), TSTP Data-Exchange Formats for Automated Theorem Proving Tools, Zhang W., Sorge V., Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications 112, 201-215.
Sutcliffe G., Suttner C.B., (2003), The CADE-18 ATP System Competition, Journal of Automated Reasoning 31(1), 23-32.
Pelletier F.J., Sutcliffe G., Suttner C.B. (2002), The Development of CASC, AI Communications 15(2-3), 79-90.
Sutcliffe G., Suttner C.B., Pelletier F.J. (2002), The IJCAR ATP System Competition, Journal of Automated Reasoning 28(3), 307-320.
Sutcliffe G. (2001), The CADE-17 ATP System Competition, Journal of Automated Reasoning 27(3), 227-250.
Sutcliffe G., Suttner C. (2001), Evaluating General Purpose Automated Theorem Proving Systems, Artificial Intelligence Journal 131(1-2), 39-54, DOI 10.1016/S0004-3702(01)00113-8.
Sutcliffe G. (2000), The CADE-16 ATP System Competition, Journal of Automated Reasoning 24(3), 371-396.
Gunn A., Sutcliffe G., Walker D. (1999), Knowledge Acquisition for Natural Resource Management, Computers and Electronics in Agriculture 23(1), 71-82.
Sutcliffe G., Suttner C.B. (1999), The CADE-15 ATP System Competition, Journal of Automated Reasoning 23(1), 1-23.
Suttner C.B., Sutcliffe G. (1998), The CADE-14 ATP System Competition, Journal of Automated Reasoning 21(1), 99-134.
Sutcliffe G., Suttner C.B. (1998), The TPTP Problem Library: CNF Release v1.2.1, Journal of Automated Reasoning 21(2), 177-203.
Pelletier F.J., Sutcliffe G. (1997), An Erratum for Some Errata to ATP Problems, Journal of Automated Reasoning 18(1), 135-135.
Suttner C.B., Sutcliffe G. (1997), The Design of the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), 139-162.
Sutcliffe G., Suttner C.B. (1997), The Procedures of the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), 163-169.
Sutcliffe G., Suttner C.B. (1997), The Results of the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), 271-286.
Pelletier F.J., Sutcliffe G., Suttner C.B. (1997), Conclusions about the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), 287-296.
Sutcliffe G., Melville S. (1996), The Practice of Clausification in Automated Theorem Proving, South African Computer Journal, 57-68. (PDF)
Sutcliffe G., Suttner C. (1995), The TPTP Problem Library, Release v1.2.0 Logic Journal of the IGPL 3(6), 957-959.
Sutcliffe G. Tabada W. (1991), Compulsory Reduction in Linear Derivation Systems, Bibel W., Artificial Intelligence (Letters to the Editor) 50, 131-132.
Sutcliffe G. (1985), A Comparison of Methods used to Represent Graphs on a Computer, Bishop J., Quaestiones Informatica 4(1), 1-11.
Sutcliffe G. (1985), GRAPHIX - A Graph Theory Sub-language, The International Journal of Computer Mathematics 17(3&4), 257-276.

Refereed Conference Publications

Sutcliffe G., Suttner C., Kotthoff L. Perrault C.R., (2024), An Empirical Assessment of Progress in Automated Theorem Proving, Benzmüller C., Heule M., Schmidt R., Proceedings of the 12th International Joint Conference on Automated Reasoning (Nancy, France), Lecture Notes in Computer Science TBA, To appear.
Steen A., Sutcliffe G., Scholl T., Benzmüller C. (2023), Solving Modal Logic Problems by Translation to Higher-order Logic, Herzig A., Luo J., Pardo P., Proceedings of the 5th International Conference on Logic and Argumentation (Hangzhou, China), Lecture Notes in Computer Science 14156, 25-43 (Best paper award).
Steen A., Sutcliffe G., Fontaine P., McKeown J. (2023), Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic, Piskac R., Voronkov A., Proceedings of the 24th International Conference on Logic for Programming Artificial Intelligence and Reasoning (Manizales, Colombia), EPiC Series in Computing 94, 369-385.
McKeown J., Sutcliffe G. (2023), An Interactive Interpretation Viewer for Typed First-order Logic, Ae Chun A., Franklin M., Proceedings of the 36th International FLAIRS Conference (Clearwater Beach, USA), DOI 10.32473/flairs.36.133073.
McKeown J., Sutcliffe G. (2023), Reinforcement Learning for Guiding the E Theorem Prover, Ae Chun A., Franklin M., Proceedings of the 36th International FLAIRS Conference (Clearwater Beach, USA), DOI 10.32473/flairs.36.133334.
Tammet T., Sutcliffe G. (2021), Combining JSON-LD with First Order Logic, Marx E., Soru T., Proceedings of the 15th IEEE International Conference on Semantic Computing (Laguna Hills, USA), 256-261.
Branning C., Sutcliffe G., Beavers T., Visser U., Schutt R. (2020), Statistical Analysis of Sailing Forecasts, Larsson L., Proceedings of the 5th International Conference on Innovation in High Performance Sailing Yachts and Sail-Assisted Ship Propulsion (Gothenburg, Sweden - Online), 99-106.
Sutcliffe G., Pelletier J. (2019), JGXYZ - An ATP System for Gap and Glut Logics, Fontaine P., Proceedings of the 27th International Conference on Automated Deduction (Natal, Brazil), Lecture Notes in Computer Science 11716, 526-537.
Brown C., Gauthier T., Kaliszyk C., Sutcliffe G., Urban J. (2019), GRUNGE: The Grand Unified ATP Challenge, Fontaine P., Proceedings of the 27th International Conference on Automated Deduction (Natal, Brazil), Lecture Notes in Computer Science 11716, 123-141.
Sutcliffe G. (2019), The CADE-27 ATP System Competition - CASC-27, Fontaine P., Proceedings of the 27th International Conference on Automated Deduction (Natal, Brazil), xviii-xx.
Bartocci E., Beyer D., Black P.E., Fedyukovich G., Garavel H., Hartmanns A., Huisman M., Kordon F., Nagele J., Sighireanu M., Steffen B., Suda M., Sutcliffe G., Weber T., Tamada A. (2019), TOOLympics 2019: An Overview of Competitions in Formal Methods, Vojnar T., Zhang L., Proceedings of the 2019 International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Prague, Czech Republic), Lecture Notes in Computer Science 11429, 3-24.
Sutcliffe G., Pelletier J., Hazen A. (2018), Making Belnap's "Useful Four-Valued Logic" Useful, Brawner K., Rus V., Proceedings of the 31st International FLAIRS Conference (Melbourne, USA), 116-121.
Schulz S., Sutcliffe G., Urban J., Pease A. (2017), Detecting Inconsistencies in Large First-Order Knowledge Bases, de Moura L., Proceedings of the 26th International Conference on Automated Deduction (Gothenburg, Sweden), 310-325.
Pelletier J., Sutcliffe G., Hazen A. (2017), Automated Reasoning for the Dialetheic Logic RM3, Rus V., Markov Z., Proceedings of the 30th International FLAIRS Conference (Marco Island, USA), 110-115.
Sutcliffe G., Pelletier J. (2016), Hoping for the Truth - A Survey of the TPTP Logics, Markov Z., Russell I., Proceedings of the 29th International FLAIRS Conference (Key Largo, USA), 110-115.
Stump A., Sutcliffe G., Tinelli C. (2014), StarExec: a Cross-Community Infrastructure for Logic Solving, Demri S., Kapur D., Weidenbach C., Proceedings of the 7th International Joint Conference on Automated Reasoning (Vienna, Austria), Lecture Notes in Artificial Intelligence 8562, 367-373, DOI 10.1007/978-3-319-08587-6_28.
Carpenter C., Osterberg L., Sutcliffe G. (2012), SAMHT - Suicidal Avatars for Mental Health Training, Youngblood M., McCarthy P., Proceedings of the 25th International FLAIRS Conference (Marco Island, USA), 484-487.
Sutcliffe G., Schulz S., Claessen K., Baumgartner P. (2012), The TPTP Typed First-order Form with Arithmetic, Bjørner N., Voronkov A., Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Merida, Venezuela), Lecture Notes in Artificial Intelligence 7180, 406-419, DOI 10.1007/978-3-642-28717-6_32.
Schneider M., Sutcliffe G. (2011), Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving, Bjørner N., Sofronie-Stokkermans V., Proceedings of the 23rd International Conference on Automated Deduction (Wroclaw, Poland), 461-475.
Carpenter C., Sutcliffe G. (2011), Sporcle goes AI, McCarthy P., Murray C., Proceedings of the 24th International FLAIRS Conference (Palm Beach, USA), 89-90.
Urban J., Sutcliffe G. (2010), Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar: Challenges and Initial Solutions Autexier S., Proceedings of the 10th International Conference on Artificial Intelligence and Symbolic Computation (Paris, France), Lecture Notes in Artificial Intelligence 6167, 132-146. (arXiv)
Sutcliffe G. (2010), The TPTP World - Infrastructure for Automated Reasoning. Clarke E., Voronkov A., Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning (Dakar, Senegal), Lecture Notes in Artificial Intelligence 6355, 1-12, DOI 10.1007/978-3-642-17511-4_1.
Sutcliffe G., Suda M., Teyssandier A., Dellis N., de Melo G. (2010), Progress Towards Effective Automated Reasoning with World Knowledge, Murray C., Lane H., Proceedings of the 23rd International FLAIRS Conference (Daytona Beach, USA), 110-115.
Suda M., Sutcliffe G., Wischnewsk P., Lamotte-Schubert M., de Melo G. (2009), External Sources of Axioms in Automated Theorem Proving, Mertsching B., Proceedings of the 32nd Annual Conference on Artificial Intelligence (Paderborn, Germany), Lecture Notes in Artificial Intelligence 5803. 281-288.
Sutcliffe G., Benzmüller C., Brown C.E., Theiss F. (2009), Progress in the Development of Automated Theorem Proving for Higher-order Logic, Schmidt R., Proceedings of the 22nd International Conference on Automated Deduction (Montreal, Canada), Lecture Notes in Artificial Intelligence 5663, 116-130.
Roederer A., Puzis Y., Sutcliffe G. (2009), Divvy: A ATP Meta-system based on Axiom Relevance Ordering , Schmidt R., Proceedings of the 22nd International Conference on Automated Deduction (Montreal, Canada), Lecture Notes in Artificial Intelligence 5663, 157-162.
Sutcliffe G., Yerikalapudi A., Trac S. (2009), Multiple Answer Extraction for Question Answering with Automated Theorem Proving Systems, Guesgen H., Lane C., Proceedings of the 22nd International FLAIRS Conference (Sanibel Island, USA), 105-110.
Benzmüller C., Rabe F., Sutcliffe G. (2008), THF0 - The Core TPTP Language for Classical Higher-Order Logic, Baumgartner P., Armando A., Gilles D., Proceedings of the 4th International Joint Conference on Automated Reasoning (Sydney, Australia), Lecture Notes in Artificial Intelligence 5195, 491-506.
Urban J., Sutcliffe G., Pudlák P., Vyskocil J. (2008), MaLARea SG1: Machine Learner for Automated Reasoning with Semantic Guidance, Baumgartner P., Armando A., Gilles D., Proceedings of the 4th International Joint Conference on Automated Reasoning (Sydney, Australia), Lecture Notes in Artificial Intelligence 5195, 441-456.
Urban J., Sutcliffe G. (2007), ATP Cross-verification of the Mizar MPTP Challenge Problems, Dershowitz N., Voronkov A., Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Yerevan, Armenia), Lecture Notes in Artificial Intelligence 4790, 546-560.
Sutcliffe G., Puzis Y. (2007), SRASS - a Semantic Relevance Axiom Selection System, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), Lecture Notes in Artificial Intelligence 4603, 295-310.
Sutcliffe G., Schulz S., Claessen K, Van Gelder A. (2006), Using the TPTP Language for Writing Derivations and Finite Interpretations, Furbach U., Shankar N., Proceedings of the 3rd International Joint Conference on Automated Reasoning (Seattle, USA), Lecture Notes in Artificial Intelligence 4190, 67-81.
Van Gelder A., Sutcliffe G. (2006), Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation, Furbach U., Shankar N., Proceedings of the 3rd International Joint Conference on Automated Reasoning (Seattle, USA), Lecture Notes in Artificial Intelligence 4190, 156-161.
Puzis Y., Gao Y., Sutcliffe G. (2006), Automated Generation of Interesting Theorems, Sutcliffe G., Goebel R., Proceedings of the 19th International FLAIRS Conference (Melbourne Beach, USA), 49-54.
Mueller E., Sutcliffe G. (2005), Reasoning in the Event Calculus using First-Order Automated Theorem Proving, Russell I., Markov Z., Proceedings of the 18th International FLAIRS Conference (Clearwater Beach, USA), 840-841.
Sutcliffe G., Belfiore D. (2005), Semantic Derivation Verification, Russell I., Markov Z., Proceedings of the 18th International FLAIRS Conference (Clearwater Beach, USA), 641-646, (3rd best paper award).
Sutcliffe G., Dvorsky A. (2003), Proving Harder Theorems by Axiom Reduction, Russell I. Haller S., Proceedings of the 16th International FLAIRS Conference (St. Augustine, USA), 108-112.
Schulz S., Sutcliffe G. (2002), System Description: GrAnDe 1.0, Voronkov A., Proceedings of the 18th International Conference on Automated Deduction, (Copenhagen, Denmark), Lecture Notes in Artificial Intelligence 2392, 280-284.
Fuchs M., Sutcliffe G. (2002), Homogeneous Sets of ATP Problems, Proceedings of the 15th International FLAIRS Conference (Pensecola, USA), 57-61.
Colton S., Sutcliffe G. (2002), Automatic Generation of Benchmark Problems for Automated Theorem Proving Systems, 7th International Symposium on Artificial Intelligence and Mathematics (Ft Lauderdale, USA). (PS)
Brown M., Sutcliffe G. (2000), PTTP+GLiDeS - Semantically Guided PTTP, McAllester D., Proceedings of the 17th International Conference on Automated Deduction (Pittsburgh, USA), Lecture Notes in Artificial Intelligence 1831, 411-416.
Sutcliffe G. (2000), SystemOnTPTP, McAllester D., Proceedings of the 17th International Conference on Automated Deduction (Pittsburgh, USA), Lecture Notes in Artificial Intelligence 1831, 406-410.
Brown M., Sutcliffe G. (1999), PTTP+GLiDeS: Guiding Linear Deductions with Semantics, Foo N., Proceedings of the 12th Australian Joint Conference on Artificial Intelligence (Sydney, Australia), Lecture Notes in Artificial Intelligence 1747, Springer-Verlag, 244-254. (PDF)
Sutcliffe G., Seyfang D. (1999), Smart Selective Competition Parallelism ATP, Kumar A., Russell I., Proceedings of the 12th International FLAIRS Conference (Orlando, USA), AAAI Press, 341-345.
Suttner C.B., Sutcliffe G. (1996), The Design of the CADE-13 ATP System Competition, McRobbie M., Slaney J., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), Lecture Notes in Artificial Intelligence 1104, 146-160.
Melville S., Sutcliffe G., Fraser D. (1996), Using Artificial Neural Networks for Meteor-Burst Communications Trail Prediction, Foo N., Goebel R., Proceedings of PRICAI'96: The 4th Pacific Rim Conference on Artificial Intelligence (Cairns, Australia), Lecture Notes in Computer Science 1114, 423-434.
Sutcliffe G., Suttner C., Yemenis T. (1994), The TPTP Problem Library, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), Lecture Notes in Artificial Intelligence 814, 252-266. (PS)
Sutcliffe G., Wu X. (1994), Extracting Rule Schemas from Rules, for an Intelligent Learning Database System, Zhang C., Debenham J., Proceedings of the 7th Australian Joint Conference on Artificial Intelligence (Armidale, Australia), 132-139. (PDF)
Sutcliffe G. (1993), A Comparison of Mechanisms for Avoiding Repetition of Subdeductions in Chain Format Linear Deduction Systems, Voronkov A., Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (St Petersburg, Russia), Lecture Notes in Artificial Intelligence 698, 321-332.
Sutcliffe G. (1992), Linear-Input Subset Analysis, Kapur D., Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, USA), Lecture Notes in Artificial Intelligence 607, 268-280.
Sutcliffe G. (1992), The Semantically Guided Linear Deduction System, Kapur D., Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, USA), Lecture Notes in Artificial Intelligence 607, 677-680.
Chaplin H.G., Singh GP., Sutcliffe G., Watson A.C. (1991), An Eye Movement Tracking System for Measurement of Human Interaction with Personal Computers, Jackson A., Proceedings of the Australian Computer Conference'91 (Adelaide, Australia), 77-86.
Sutcliffe G. (1990), A General Clause Theorem Prover, Stickel M.E., Proceedings of the 10th International Conference on Automated Deduction (Kaiserslautern, Germany), Lecture Notes in Artificial Intelligence 449, 675-676.
Sutcliffe G. Pinakis J. (1990), Prolog-Linda - An Embedding of Linda in muProlog, Tsang C.P., Proceedings of the 4th Australian Conference on Artificial Intelligence (Perth, Australia), 331-340. (PDF)

Refereed Workshop Publications

Sutcliffe G., McKeown J., Steen A. (2023), A Chat with Bard, Schulz S., Korovin K., Rawson M., Proceedings of the 14th International Workshop on the Implementation of Logics (Manizales, Colombia), EasyChair Preprints 10329, EasyChair Publications.
Steen A., Fuenmayor D., Gleißner T., Sutcliffe G., Benzmüller C. (2022), Automated Reasoning in Non-classical Logics in the TPTP World, Konev B., Schon C., Steen A., Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning (Haifa, Italy), CEUR Workshop Proceedings 3201, Online.
Saidy N., Siegfried H., Schulz S., Sutcliffe G. (2020), Cutting down the TPTP language (and others), Fontaine P., Ruemmer P., Tourret S., Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (Online, Earth), CEUR Workshop Proceedings 2752, 134-147.
Liu Q., Wu Z., Wang Z., Sutcliffe G. (2020), Evaluation of Axiom Selection Techniques, Fontaine P., Ruemmer P., Tourret S., Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (Online, Earth), CEUR Workshop Proceedings 2752, 63-75.
Benzmüller C., Sutcliffe G. (2019), Explicit Normative Reasoning and Machine Ethics, Suda M., Winkler S., Proceedings of the Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (Natal, Brazil).
Sutcliffe G., Kotelnikov E. (2018), TFX: The TPTP Extended Typed First-order Form, Konev B., Urban J., Schulz S., Proceedings of the 6th Workshop on the Practical Aspects of Automated Reasoning (Oxford, United Kingdom), CEUR Workshop Proceedings 1080, 72-87.
Kaliszyk C., Sutcliffe G., Rabe F. (2016), TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism, Fontaine P., Schulz S., Urban J., Proceedings of the 5th workshop on Practical Aspects of Automated Reasoning (Coimbra, Portugal), 41-55.
Sutcliffe G., Schulz S. (2016), The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps, Konev B., Schulz S., Simon L., Proceedings of the 11th International Workshop on the Implementation of Logics (Suva, Fiji), EPiC Series in Computing 40, 106-121.
Arhami N., Sutcliffe G. (2014), The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics, Schulz S., de Moura L., Konev B., Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, (Vienna, Austria), EasyChair Proceedings in Computing (31), 2-11.
Nassar M., Sutcliffe G. (2014), Automated Theorem Proving using the TPTP Process Instruction Language, Schulz S., de Moura L., Konev B., Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, (Vienna, Austria), EasyChair Proceedings in Computing (31), 67-75.
Sutcliffe G. (2013), The TPTP Process Instruction Language, Konev B., Schulz S., Sutcliffe G., Proceedings of the 10th International Workshop on the Implementation of Logics (Stellenbosch, South Africa).
Schneider M., Rudolph S., Sutcliffe G. (2013), Modeling in OWL 2 without Restrictions, Srinivas K., Jupp S., Proceedings of the 10th OWL Experiences and Directions Workshop (Montpellier, France), CEUR Workshop Proceedings 1080.
Sutcliffe G., Chang C., McGuinness D., Ding L., Lebo T., Pinheiro da Silva P. (2011), Combining Proofs to form Different Proofs, Fontaine P., Stump A., Proceedings of the 1st Workshop on Proof eXchange for Theorem Proving (Wroclaw, Poland). (PDF)
Otten J., Sutcliffe G. (2010), Using the TPTP Language for Representing Derivations in Tableau and Connection Calculi, Konev B., Schmidt R., Schulz S., Proceedings of the IJCAR 2010 Workshop on Practical Aspects of Automated Reasoning (Edinburgh, United Kingdom), 90-100. (PDF)
Sutcliffe G., Chang C., Ding L., McGuinness D., Pinheiro da Silva P. (2010), Different Proofs are Good Proofs, McGuinness D., Stump A., Sutcliffe G., Tinelli C., Proceedings of the IJCAR 2010 Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions (Edinburgh, United Kingdom). (PDF)
Sutcliffe G. (2008), The SZS Ontologies for Automated Reasoning Software, Rudnicki P., Sutcliffe G., Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics (Doha, Qattar), CEUR Workshop Proceedings 418, 38-49. (PDF)
Pinheiro da Silva P., del Rio N., McGuinness D., Ding L., Chang C., Sutcliffe G. (2008), User Interfaces for Portable Proofs, Autexier S., Benzmueller C., Proceedings of the 8th International Workshop On User Interfaces for Theorem Provers (Montreal, Canada). (PDF)
Pease A., Sutcliffe G., Siegel N., Trac S. (2008), The Annual SUMO Reasoning Prizes at CASC, Schmidt R., Konev B., Schulz S., Proceedings of the IJCAR 2008 Workshop on Practical Aspects of Automated Reasoning (Sydney, Australia), CEUR Workshop Proceedings 373, 66-70. (PDF)
Trac S., Sutcliffe G., Pease A. (2008), Integration of the TPTPWorld into SigmeKEE, Schmidt R., Konev B., Schulz S., Proceedings of the IJCAR 2008 Workshop on Practical Aspects of Automated Reasoning (Sydney, Australia), 103-114. (PDF)
Pinheiro da Silva P., Sutcliffe G., Chang C., Ding L., del Rio N., McGuinness D. (2008), Presenting TSTP Proofs with Inference Web Tools, Schmidt R., Konev B., Schulz S., Proceedings of the IJCAR 2008 Workshop on Practical Aspects of Automated Reasoning (Sydney, Australia), 81-93. (PDF)
Pease A., Sutcliffe G. (2007), First Order Reasoning on a Large Ontology, Urban J., Sutcliffe G., Schulz S., Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (Bremen, Germany). (PDF)
Urban J., Trac S., Sutcliffe G., Puzis Y. (2007), Combining Mizar and TPTP Semantic Presentation Tools, Libbrecht P., Proceedings of the Mathematical User-Interfaces Workshop 2007 (Linz, Austria). (PDF)
Trac S., Puzis Y., Sutcliffe G. (2006), An Interactive Derivation Viewer, Autexier S., Benzmüller C., Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 3rd International Joint Conference on Automated Reasoning (Seattle, USA), Electronic Notes in Theoretical Computer Science 174(2), 109-124. (PDF)
Sutcliffe G., Denney E., Fischer B. (2005), Practical Proof Checking for Program Certification, Sutcliffe G., Fischer B., Schulz S., Proceedings of the CADE-20 Workshop on Empirically Successful Classical Automated Reasoning (Tallinn, Estonia). (PDF)
Mueller E., Sutcliffe G. (2005), Discrete Event Calculus Deduction using First-Order Automated Theorem Proving, Konev B., Schulz S., 5th International Workshop on Implementation of Logics, 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning, (Montevideo, Uruguay), 43-56. (PDF)
Zhang Y., Sutcliffe G. (2005), Lemma Management Techniques for Automated Theorem Proving, Konev B., Schulz S., 5th International Workshop on Implementation of Logics, 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning, (Montevideo, Uruguay), 87-94. (PDF)
Zimmer J., Meier A., Sutcliffe G., Zhang Y. (2004), Integrated Proof Transformation Services, Benzmüller C., Windsteiger W., Proceedings of the Workshop on Computer-Supported Mathematical Theory Development, 2nd International Joint Conference on Automated Reasoning (Cork, Ireland), Electronic Notes in Theoretical Computer Science. (PDF)
Sutcliffe G., Zimmer J., Schulz S. (2003), Communication Formalisms for Automated Theorem Proving Tools, Sorge V. Colton S. Fisher M. Gow J., Proceedings of the Workshop on Agents and Automated Reasoning, 18th International Joint Conference on Artificial Intelligence, (Acapulco, Mexico), 52-57. (PDF)
Zimmer J., Franke A., Colton S., Sutcliffe G. (2002), Integrating HR and tptp2X into MathWeb to Compare Automated Theorem Provers, Sutcliffe G., Pelletier J., Suttner C., Proceedings of the CADE-18 Workshop - Problem and Problem Sets for ATP (Copenhagen, Denmark). (PS)
Sutcliffe G. (2001), The Design and Implementation of a Compositional Competition-Cooperation Parallel ATP System, de Nivelle H. and Schulz S. 2nd International Workshop on Implementation of Logics, 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, (Havana, Cuba), Max-Planck-Institut fur Informatik Research Report MPI-I-2001-2-006, 92-102. (PDF)
Pelletier J., Sutcliffe G. (2001), CASC: Effective Evaluation having an Effect, Workshop on Empirical Methods in Artificial Intelligence, 17th International Joint Conference on Artificial Intelligence, (Seattle, USA), 33-40. (PDF)
Sutcliffe G., Fuchs M., Suttner C. (2001), Progress in Automated Theorem Proving, 1997-1999, Workshop on Empirical Methods in Artificial Intelligence, 17th International Joint Conference on Artificial Intelligence, (Seattle, USA), 53-60. (PDF)
Brown M., Sutcliffe G. (2000), PTTP+GLiDeS - Using Models to Guide Linear Deductions, Baumgartner P., Fermueller C., Peltier N., Zhang H., Proceedings of the CADE-17 Workshop: Model Computation - Principles, Algorithms, Applications (Pittsburgh, USA). (PDF)
Sharpe M., Ahmed N., Sutcliffe G. (1994), An Intelligent Document Understanding and Reproduction System, Proceedings of MVA'94 : IAPR Workshop on Machine Vision Applications (Kawasaki, Japan), 267-271.
Sutcliffe G., and Pinakis J. (1992), Prolog-D-Linda : An Embedding of Linda in SICStus Prolog, DeGroot D., Kacsuk P., Succi G., Talia D., Proceedings of the Joint Workshop on Distributed and Parallel Implementation of Logic Programming Systems (Washington, USA), 70-79. (PDF)
Sutcliffe G. (1992), A Heterogeneous Parallel Deduction System, Hasegawa R., Stickel M.E., Proceedings of the Workshop on Automated Deduction: Logic Programming and Parallel Computing Approaches, FGCS'92 (Tokyo, Japan), Institute for New Generation Computer Technology, Tokyo, Japan. (PS)
Sutcliffe G. (1991), A Parallel Linear and UR-Derivation System, Kanal L.N., Suttner C.B., Proceedings of PPAI-91, International Workshop on Parallel Processing for Artificial Intelligence (Sydney, Australia), 211-215. (PDF)

Other Publications

Sutcliffe G. (2023), Proceedings of the CADE-29 ATP System Competition (CASC-29).
Benzmüller C., Fuenmayor D., Steen A., Sutcliffe G. (2022), Automation of Boolos' Curious Inference in Isabelle/HOL Archive of Formal Proofs, Online https://www.isa-afp.org/entries/Boolos_Curious_Inference_Automated.html.
Steen A., Sutcliffe G., Gleißner T, Benzmüller C., (2022), Solving QMLTP Problems by Translation to Higher-order Logic, arXiv, DOI 10.48550/arXiv.2212.09570.
Sutcliffe G. (2022), Proceedings of the 11th IJCAR ATP System Competition (CASC-J11).
Sutcliffe G. (2021), Proceedings of the CADE-28 ATP System Competition (CASC-28).
Suttner C., Sutcliffe G., Perrault R. (2021), Automated Theorem Proving (ATP), Zhang D., Mishra S., Brynjolfsson E., Etchemendy J., Ganguli D., Grosz B., Lyons T., Manyika J., Niebles J.C., Sellitto M., Shoham Y., Clark J., Perrault R., The AI Index 2021 Annual Report, AI Index Steering Committee, Human-Centered AI Institute, Stanford University, USA, 74-75, 201-202. (Online)
Sutcliffe G. (2020), Proceedings of the 10th IJCAR ATP System Competition (CASC-J10). (PDF)
Sutcliffe G. (2019), Proceedings of the CADE-27 ATP System Competition (Natal, Brazil). (PDF)
Sutcliffe G. (2018), Proceedings of the 9th IJCAR ATP System Competition (Oxford, United Kingdom). (PDF)
Sutcliffe G. (2017), Proceedings of the CADE-26 ATP System Competition (Gothenburg, Sweden). (PDF)
Sutcliffe G. (2016), Proceedings of the 8th IJCAR ATP System Competition (Coimbra, Portugal). (PDF)
Sutcliffe G. (2016), Thousands of Models for Theorem Provers - The TMTP Model Library Bjorner, N. and Blanchette, J. and Sofronie-Stokkermans, V. and Weidenbach, C., Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381) (Dagstuhl, Germany), Dagstuhl Reports 5(9), 33-24.
Arhami N., Sutcliffe G. (2015), Automated Theorem Proving by Translation to Description Logic, McIver A., Fehnker A., Voronkov, A., Presentation Papers of the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Suva, Fiji), EasyChair Proceedings in Computing 35, 1-14.
Sutcliffe G. (2015), The TPTP World - Infrastructure for Automated Reasoning, Faber W., Paschke A., Reasoning Web. Web Logic Rules - Lecture Notes of the 11th Reasoning Web Summer School (Berlin, Germany), Lecture Notes in Computer Science 9203, 327-329.
Sutcliffe G. (2015), Proceedings of the CADE-25 ATP System Competition (Berlin, Germany). (PDF)
Arhami N., Sutcliffe G. (2015), Poster abstract: Automated Theorem Proving by Translation to Description Logic, Russell I., Eberle, W., Proceedings of the 27th International FLAIRS Conference (Hollywood, USA), 611-612.
Sutcliffe G. (2014), Proceedings of the 7th IJCAR ATP System Competition (Vienna, Austria). (PDF)
Nassar M., Sutcliffe G. (2014), Poster abstract: Automated Theorem Proving using the TPTP Process Instruction Language, Boonthum-Denecke C., Eberle W., Proceedings of the 27th International FLAIRS Conference (Pensacola, USA), 524-524.
Sutcliffe G. (2013), Proceedings of the CADE-24 ATP System Competition (Lake Placid, USA). (PDF)
Sutcliffe G. (2012), Proceedings of the 6th IJCAR ATP System Competition (Manchester, United Kingdom). (PDF)
Schneider M., Sutcliffe G. (2011), Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving, (Extended version of CADE-23 paper). (arXiv)
Sutcliffe G. (2011), Proceedings of the CADE-23 ATP System Competition (Wroclaw, Poland). (PDF)
Sutcliffe G. (2011), How to Run a Logic-Solver Competition - The CASC Experience, Proceedings of the Deep Knowledge Representation Challenge Workshop (Banff, Canada). (PDF)
Sutcliffe G., Pease A. (2011), Why is Surface Area Important to Normal Cell Function?, Proceedings of the Deep Knowledge Representation Challenge Workshop (Banff, Canada). (PDF)
Sutcliffe G. (2010), Proceedings of the 5th IJCAR ATP System Competition (Edinburgh, United Kingdom). (PDF)
Sutcliffe G. (2009), Proceedings of the CADE-22 ATP System Competition (Montreal, Canada). (PDF)
Sutcliffe G. (2008), Proceedings of the 4th IJCAR ATP System Competition (Sydney, Australia). (PDF)
Sutcliffe G. (2007), Proceedings of the CADE-21 ATP System Competition (Bremen, Germany). (PDF)
Sutcliffe G. (2006), Proceedings of the 3rd IJCAR ATP System Competition (Seattle, USA). (PDF)
Sutcliffe G. (2005), Proceedings of the CADE-20 ATP System Competition (Tallinn, Estonia). (PDF)
Sutcliffe G. (2004), Proceedings of the 2nd IJCAR ATP System Competition (Cork, Ireland). (PDF)
Sutcliffe G. (2003), Proceedings of the CADE-19 ATP System Competition (Miami, USA). (PDF)
Sutcliffe G. (2002), Proceedings of the CADE-18 ATP System Competition (Copenhagen, Denmark). (PDF)
Sutcliffe G., Suttner C., Pelletier J. (2001), The IJCAR ATP System Competition: All the Details, Technical Report UM-CSC-2001-001, Department of Computer Science, University of Miami (Miami, USA). (PDF)
Sutcliffe G. (2001), Proceedings of the IJCAR ATP System Competition (Siena, Italy). (PS)
Sutcliffe G., Fuchs M., Suttner C. (2000), Progress in Theorem Proving, 1997-1999, Technical Report TR-ARP-11-00, Automated Reasoning Project, Australian National University (Canberra, Australia). (PDF)
Fuchs M., Sutcliffe G. (2000), Homogeneous Sets of ATP Problems, Technical Report TR-ARP-09-00, Automated Reasoning Project, Australian National University (Canberra, Australia). (.ps.gz)
Sutcliffe G. (2000), Proceedings of the CADE-17 ATP System Competition (Pittsburgh, USA). (PS)
Sutcliffe G., Suttner C. (2000), Evaluating General Purpose Automated Theorem Proving Systems, Technical Report 00/02, School of Information Technology, James Cook University (Townsville, Australia).
Brown M., Sutcliffe G. (2000), System Description: PTTP+GLiDeS - Semantically Guided PTTP, Technical Report 00/01, School of Information Technology, James Cook University (Townsville, Australia). (PS)
Sutcliffe G. (1999), Proceedings of the CADE-16 ATP System Competition (Trento, Italy). (PS)
Sutcliffe G., Suttner C. (1998), Proceedings of the CADE-15 ATP System Competition (Lindau, Germany). (PS)
Sutcliffe G., Suttner C. (1998), The CADE-14 ATP System Competition, Technical Report 98/01, Department of Computer Science, James Cook University (Townsville, Australia). (PS)
Suttner C., Sutcliffe G. (1996), The TPTP Problem Library (TPTP v2.1.0), Technical report AR-97-01, Institut fuer Informatik, Technische Universitaet Muenchen (Munich, Germany), Technical Report 97/04, Department of Computer Science, James Cook University (Townsville, Australia).
Melville S., Sutcliffe G., Fraser D. (1996), Using Artificial Neural Networks for Meteor-Burst Communications Trail Prediction, Technical Report 96/5, Department of Computer Science, James Cook University (Townsville, Australia).
Sutcliffe G., Melville S. (1996), The Practise of Clausification in Automated Theorem Proving, Technical Report 96/6, Department of Computer Science, James Cook University (Townsville, Australia).
Suttner C., Sutcliffe G. (1996), The TPTP Problem Library (TPTP v1.2.1), Technical report AR-96-02, Institut fuer Informatik, Technische Universitaet Muenchen, Munich, Germany, Technical Report 96/09, Department of Computer Science, James Cook University (Townsville, Australia).
Sutcliffe G., Suttner C. (1996), Mathematics in the TPTP Problem Library (v1.2.1), Technical Report 96/15, Department of Computer Science, James Cook University (Townsville, Australia). (PS)
Sutcliffe G., Singh K. (1995), A Framework for Building Parallel ATP Systems, Gore R., Proceedings of the 2nd Symbolic Reasoning Systems Workshop (Canberra, Australia), Technical Report TR-SRS-1-95, Automated Reasoning Project, Research School of Information Sciences and Engineering and Centre for Information Science Research, Australian National University (Canberra, Australia). (PDF)
Suttner C., Sutcliffe G. (1995), The TPTP Problem Library (TPTP v1.2.0), Technical report AR-95-03, Institut fuer Informatik, Technische Universitaet Muenchen (Munich, Germany), Technical Report 95/6, Department of Computer Science, James Cook University (Townsville, Australia).
Nugroho L., Sutcliffe G. (1995), A Tool for Introducing Persistent Programming, Technical Report 95/13, Department of Computer Science, James Cook University (Townsville, Australia). (PS)
Sutcliffe G., Suttner C.B. (1995), The Design of the CADE-13 ATP System Competition, Technical Report 95/15, Department of Computer Science, James Cook University, Townsville, Australia. Technical report AR-95-05, Institut für Informatik, Technische Universität München (Munich, Germany). (PS)
Sutcliffe G., Suttner C.B. (1995), ATP System Results for the TPTP Problem Library (upto TPTP v1.1.3), Technical Report 95/16, Department of Computer Science, James Cook University (Townsville, Australia). Technical report AR-95-06, Institut für Informatik, Technische Universität München (Munich, Germany). (PS)
Sharpe M., Ahmed N., Sutcliffe G. (1994), Implementation of an Intelligent Document Understanding and Reproduction System, Technical Report 94/10, Department of Computer Science, James Cook University (Townsville, Australia).
Suttner C., Sutcliffe G. (1994), The TPTP Problem Library (TPTP v1.1.1), Technical report AR-94-03, Institut fuer Informatik, Technische Universitaet Muenchen, Munich, Germany (also available as Technical Report 93/11, Department of Computer Science, James Cook University (Townsville, Australia).
Sutcliffe G., Suttner C. (1994), An ATP System Competition. Part 1 : Choices and Decisions, Sattar A., Proceedings of the 2nd Automated Reasoning Day (Bribie Island, Australia), Research Report CIT-94-20, School of Computing and Information Technology, Griffith University, (Brisbane, Australia).
Sutcliffe G. (1993), Prolog-D-Linda v2: A New Embedding of Linda in SICStus Prolog, Technical Report 93/6, Department of Computer Science, James Cook University (Townsville, Australia). (PDF) (Better, unofficial version - PS)
Suttner C., Sutcliffe G., Yemenis T. (1993), The TPTP Problem Library for 1st Order Automated Theorem Provers, Technical Report FKI-184-93, Institut fuer Informatik, Technische Universitaet Muenchen, Munich, Germany; Technical Report 93/11, Department of Computer Science, James Cook University (Townsville, Australia).
Sutcliffe G. (1992), A Linear Deduction System with Integrated Semantic Guidance, PhD Thesis, Department of Computer Science, The University of Western Australia (Perth, Australia). (PDF)
Sutcliffe G., Pinakis J. (1991), Prolog-D-Linda : An Embedding of Linda in SICStus Prolog, Research Report 91/7, Department of Computer Science, The University of Western Australia (Perth, Australia). (PDF)
Tabada W., Sutcliffe G. (1990), An Analysis of the Selective Linear Model Inference System, Research Report 90/2, Department of Computer Studies, Western Australian College of Advanced Education (Perth, Australia).
Tabada W., Sutcliffe G. (1990), An Analysis and Comparative Study of Five Linear Derivation Strategies, Research Report 90/1, Department of Computer Studies, Western Australian College of Advanced Education (Perth, Australia).
Sutcliffe G., Tsang C.P. (1988), A Review of Methedologies for Specifying and Executing Logic Programs, Research Report 88/14, Department of Computer Science, The University of Western Australia (Perth, Australia).
Grants

Grants

2024 $70000 Sutcliffe G., Amazon Research Award: Automated Theorem Proving Community Infrastructure in the AWS Cloud. Additionally $20000 in AWS credits.
2024 €6130 Steen A., Fontaine P., Sutcliffe G., EuroProofNet WG2 TPTP Tea Party.
2024 €TBA Blanqui F., Sutcliffe G., ENS Paris-Saclay Visiting Scholar.
2023 US$4100
+ €1420
Sutcliffe G., Unrestricted gifts in support of the TPTP project.
2023 €6800 Blanqui F., Sutcliffe G., Steen A., Fontaine P., EuroProofNet WG2 TPTP Tea Party.
2023 €1014 Sutcliffe G., COST Action Inter-WG Developers Meeting.
2023 €3400 Blanqui F., Sutcliffe G., ENS Paris-Saclay Visiting Scholar.
2023 €2867 Benzmüller C., Sutcliffe G., University of Bamberg Visiting Scholar.
2022 US$2602
+ €3788
Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2021 US$3496 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2020 US$3210 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2018 US$912 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2018 US$990 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2017 US$3809 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2017-2020 US$1057499 Stump A. (PI), Sutcliffe G. (PI), Tinelli C. (co-PI), StarExec: Cross-Community Infrastructure for Logic Solving, NSF Computing Research Infrastructure Grant. ($446850 to Sutcliffe)
2016 US$1740 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2015 US$3818 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2014-2015 US$57219 Sutcliffe G., SystemOnTPTP - Online Services for Automated Theorem Proving in Classical Logic, NSF Computing Research Infrastructure Grant.
2014 US$2071 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2013 US$528 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2012 US$5468 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project.
2011-2014 US$1959838 Stump A. (PI), Sutcliffe G. (PI), Tinelli C. (co-PI), StarExec: Cross-Community Infrastructure for Logic Solving, NSF Computing Research Infrastructure Grant. ($150295 to Sutcliffe)
2011 US$500 Sutcliffe G., Unrestricted gift to the University of Miami in support of CASC-23.
2010 US$726 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project, Various donors.
2010 US$84197 Stump A. (PI), Sutcliffe G. (PI), Tinelli C. (co-PI), *-EXEC: A Cross-Community Solver Execution Service, NSF Computing Research Infrastructure Grant. ($15750 to Sutcliffe)
2009 US$1268 Sutcliffe G., Unrestricted gifts to the University of Miami in support of the TPTP project, Various donors.
2008 €240 Sutcliffe G. (Researcher), Rabe F., Kohlhase M. (Hosts), A TPTP-OMDoc Bridge, Jacobs University Bremen ICTS Fellowship.
2008 €130109 Sutcliffe G. (Researcher), Benzmüller C. (Host), An Infrastructure for Typed Higher-order Form Automated Theorem Proving, European Union Marie Curie International Incoming Fellowship.
2007‑2011 US$467575 Sutcliffe G. (PI), Kocak H. (co-PI), Pestien V. (co-PI), Rosenberg B. (co-PI), Computer Science and Mathematics for Scientists, NSF Scholarships in Science, Technology, Engineering, and Mathematics.
2007 US$20000 Sutcliffe G., Unrestricted gift to the University of Miami in support of Research in Automated Reasoning, Articulate Software.
2007 US$1500 Sutcliffe G., Unrestricted gift to the University of Miami in support of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Microsoft Research.
2006‑2007 €176076 Urban J. (Researcher), Sutcliffe G. (Host), Automating Reasoning in Large Formal Mathematical Knowledge Bases, European Union Marie Curie International Outgoing Fellowship.
2005 US$2500 Voronkov A., Sutcliffe G., Unrestricted gift to the University of Miami in support of the 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Microsoft Research.
2004‑2005 US$27281 Sutcliffe G. (PI), The Use of Relevance, Axiom Selection, and Lemmas, in Automated Theorem Proving, University of Miami Small Grant.
2000‑2002 AU$100000 Antoniou G. (PI), Sutcliffe G. (Co-PI), Stuckey P. (Co-PI), Foo N. (Co-PI), A National Distributed Facility for Logic- and Constraint-Based Software Tools, Research Infrastructure Equipment and Facilities Scheme, Australian Research Council.
1995 AU$3800 Sutcliffe G. (PI), The TPTP Problem Library, James Cook University MRG.
1994 AU$5000 Sutcliffe G. (PI), The TPTP Problem Library, James Cook University MRG.
1994 DM4000 Suttner C. (PI), Sutcliffe G. (Co-PI), The TPTP Problem Library, Grant from the Bundesministerium fuer Forschung und Technology (German Ministry for Research).
1992 AU$1725 Sutcliffe G. (PI), The TPTP Problem Library, Edith Cowan University grant.
1992 AU$5000 Sutcliffe G. (PI), Automated Reasoning on a Distributed Computer Network, Edith Cowan University grant.

Professional

Editing

Editing

2023-ongoing Editorial Board, Logic Journal of the IGPL
2015-ongoing Editorial Board, Acta Informatica
2014-ongoing Editorial Board, Formalized Mathematics
2003 Benchmarks Area Editor, QPQ Repository for Deductive Software Components

Edited Volumes

Platzer A., Sutcliffe G. (2022), Selected Extended Papers of CADE 2021, Journal of Automated Reasoning 66, Springer Nature.
Platzer A., Sutcliffe G. (2021), Proceedings of the 28th International Conference on Automated Deduction (Pittsburgh, USA), Lecture Notes in Artificial Intelligence 12699, Springer-Verlag.
Danoy G., Pang J., Sutcliffe G. (2020), Proceedings of the 6th Global Conference on Artificial Intelligence (Online, Earth), EPiC Series in Computing 72.
Barthe G., Korovin K., Schulz S., Suda M., Sutcliffe G., Veanes M. (2018), Proceedings of the LPAR-22 Workshops and Short Papers (Awassa, Ethiopia), Kalpa Publications in Computing 9.
Eiter T., Sands D., Sutcliffe G., Voronkov A. (2017), Proceedings of the IWIL 2017 Workshop and LPAR-21 Short Presentations (Maun, Botswana), Kalpa Publications in Computing 1.
Benzmüller C., Sutcliffe G., Rojas R. (2016), Proceedings of the 2nd Global Conference on Artificial Intelligence (Berlin, Germany), EPiC Proceedings in Computing 41.
Gottlob G., Sutcliffe G., Voronkov A. (2015), Proceedings of the 2015 Global Conference on Artificial Intelligence (Tbilisi, Georgia), EPiC Proceedings in Computing 36.
Fehnker A., McIver A., Sutcliffe G., Voronkov A. (2015), Short Presentation Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Suva, Fiji), EPiC Proceedings in Computing 35.
Konev B., Schulz S., Sutcliffe G. (2013), Proceedings of the 10th International Workshop on the Implementation of Logics (Stellenbosch, South Africa).
Klebanov V., Beckert B., Biere A., Sutcliffe G. (2012), Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (Manchester, England), CEUR Workshop Proceedings 873. (PDF)
Schmidt R., Sutcliffe G., Schulz S. (2009), Special Issue: Empirically Successful Computerized Reasoning, Journal of Applied Logic 7(1).
Rudnicki P., Sutcliffe G., Konev B., Schmidt R., Schulz S. (2008), Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics (Doha, Qattar), CEUR Workshop Proceedings 418. (PDF)
Sutcliffe G., Colton S., Schulz S. (2008), Proceedings of the CICM Workshop on Empirically Successful Automated Reasoning in Mathematics, (Birmingham, United Kingdom), CEUR Workshop Proceedings 378. (PDF)
Sutcliffe G., Urban J., Schulz S. (2007), Proceedings of the Workshop on Empirically Successful Automated Reasoning in Large Theories, 21st International Conference on Automated Deduction (Bremen, Germany), CEUR Workshop Proceedings 257. (PDF)
Wilson, D., Sutcliffe G. (2007), Proceedings of the 20th International FLAIRS Conference (Key West, USA), AAAI Press.
Fischer B., Sutcliffe G., Schulz S. (2007), Special Issue: Empirically Successful Automated Reasoning - Applications, Journal of Automated Reasoning 37(1-2).
Fischer B., Sutcliffe G., Schulz S. (2007), Special Issue: Empirically Successful Automated Reasoning - Systems, Journal of Automated Reasoning 36(4).
Benzmueller C., Fischer B. Sutcliffe G., (2006), Proceedings of the 6th International Workshop on the Implementation of Logics (Phnom Penh, Cambodia), CEUR Workshop Proceedings 212. (PDF)
Sutcliffe G., Schmidt R., Schulz S. (2006), Proceedings of the Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning (Seattle, USA), CEUR Workshop Proceedings 192. (PDF)
Sutcliffe G., Goebel, R. (2006), Proceedings of the 19th International FLAIRS Conference (Melbourne Beach, USA), AAAI Press.
Schulz S., Sutcliffe G., Tammet T. (2006), Special Issue: Empirically Successful First Order Reasoning, International Journal on Artificial Intelligence Tools 15(1).
Sutcliffe G., Voronkov, A. (2005), Proceedings of the 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (Montego Bay, Jamaica), Lecture Notes in Artificial Intelligence 3835, Springer-Verlag.
Sutcliffe G., Fischer B., Schulz S. (2005), Proceedings of the Workshop on Empirically Successful Classical Automated Reasoning, 20th International Conference on Automated Deduction (Tallinn, Estonia). (PDF)
Sutcliffe G., Schulz S., Tammet T. (2004), Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning (Cork, Ireland). (PDF)
Sutcliffe G., Pelletier, F.J., Suttner, C. (2002), Proceedings of the Workshop on Problems and Problems Sets for ATP, 18th International Conference on Automated Deduction (Copenhagen, Denmark). (PDF)
Sutcliffe G., Suttner C.B. (1997), Special Issue: The CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2).
Evaluations

Evaluations

2020 Sutcliffe G., Panel member, NSF 19-512 CISE Community Research Infrastructure (CCRI).
2020 Sutcliffe G., Panel member, Confluence Competition (CoCo) 2020.
2019 Sutcliffe G., Panel member, Confluence Competition (CoCo) 2019.
Program Committees

Program Committees

2024 Program Committee International Workshop on Quantification 2024 (Nancy, France).
2024 Program Committee 9th Workshop on Practical Aspects of Automated Reasoning (Nancy, France).
2024 Artifact Evaluation Committee 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Luxembourg City, Luxembourg).
2023 Program Committee 5th International Conference on Logic and Argumentation (Hangzhou, China).
2022 Technical Committee 1st International Workshop on Trustworthy AI for the Future of Risk Management (Belfast, United Kingdom).
2021 Program Committee 4th International Conference on Logic and Argumentation (Hangzhou, China).
2021 Program Committee 6th Conference on Artificial Intelligence and Theorem Proving (Aussois, France).
2021 Program Co-chair 28th International Conference on Automated Deduction (Pittsburgh, USA).
2021 Program Committee 7th Workshop on Proof eXchange for Theorem Proving (Pittsburgh, USA).
2021 Program Committee 2021 Workshop on Parallel and Distributed Automated Reasoning (Pittsburgh, USA).
2021 Program Committee 3rd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (Pittsburgh, USA).
2020 Program Committee, 13th Conference on Intelligent Computer Mathematics (Bertinoro, Italy).
2020 Program Committee, 10th International Joint Conference on Automated Reasoning (Paris, France).
2020 Program Committee, 7th Workshop on Practical Aspects of Automated Reasoning (Paris, France).
2020 Program Committee, 14th International Workshop on the Implementation of Logics (Alicante, Spain).
2020 Program Committee, 5th Conference on Artificial Intelligence and Theorem Proving (Aussois, France).
2019 Program Committee, 27th International Conference on Automated Deduction (Natal, Brazil).
2019 Program Committee, 2nd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (Natal, Brazil).
2019 Program Committee, 6th Workshop on Proof eXchange for Theorem Proving (Natal, Brazil).
2019 Program Committee, 4th Conference on Artificial Intelligence and Theorem Proving (Obergurgl, Austria).
2018 Program Committee, 13th International Workshop on the Implementation of Logics (Awassa, Ethiopia).
2018 Program Committee, 9th International Joint Conference on Automated Reasoning (Oxford, United Kingdom).
2018 Program Committee, 3rd Conference on Artificial Intelligence and Theorem Proving (Aussois, France).
2017 Program Committee, 5th Workshop on Proof Exchange for Theorem Proving (Brasilia, Brazil).
2017 Program Committee, 26th International Conference on Automated Deduction (Gothenburg, Sweden).
2017 Program Committee, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (Gothenburg, Sweden).
2017 Program Committee, 10th Conference on Intelligent Computer Mathematics (Edinburgh, United Kingdom).
2017 Program Committee, 30th International FLAIRS Conference (Marco Island, USA).
2017 Program Committee, 2nd Conference on Artificial Intelligence and Theorem Proving (Obergurgl, Austria).
2016 Program Committee, Mathematical Foundations of Informatics Conference, 2016 (Chisinau, Moldova).
2016 Program Committee, 5th Workshop on Practical Aspects of Automated Reasoning (Coimbra, Portugal).
2016 Program Committee, 9th Conference on Intelligent Computer Mathematics (Bialystok, Poland).
2016 Program Committee, 5th Workshop on Controlled Natural Language (Aberdeen, United Kingdom).
2016 Program Committee, 29th International FLAIRS Conference (Key Largo, USA).
2016 Program Committee, 1st on Artificial Intelligence and Theorem Proving (Obergurgl, Austria).
2015 Program Committee, 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Suva, Fiji).
2015 Program Committee, 11th International Workshop on the Implementation of Logics (Suva, Fiji).
2015 Program Co-chair, 1st Global Conference on Artificial Intelligence (Tbilisi, Georgia).
2015 Program Committee, Workshop on Foundations of Informatics (Chisinau, Republic of Moldova).
2015 Program Committee, 25th International Conference on Automated Deduction (Berlin, Germany).
2015 Program Committee, 4th Workshop on Proof eXchange for Theorem Proving (Berlin, Germany).
2015 Program Committee, Conference on Intelligent Computer Mathematics, Systems and Data Track, (Washington, USA).
2015 Program Committee, 28th International FLAIRS Conference (Hollywood, USA).
2014 Program Committee, 4th Workshop on Controlled Natural Language (Galway, Ireland).
2014 Program Committee, 7th International Joint Conference on Automated Reasoning (Vienna, Austria).
2014 Program Committee, IJCAR Workshop on Knowledge Intensive Automated Reasoning (Vienna, Austria).
2014 Program Committee, 4th Workshop on Practical Aspects of Automated Reasoning (Vienna, Austria).
2014 Program Committee, 27th International FLAIRS Conference (Pensacola Beach, USA).
2013 Program Committee, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Stellenbosch, South Africa).
2013 Program Committee, 3rd International Workshop on Proof Exchange for Theorem Proving (Lake Placid, USA).
2013 Program Committee, CADE-24 Workshop on Knowledge Intensive Automated Reasoning (Lake Placid, USA).
2013 Program Committee, Do-Form: Enabling Domain Experts to use Formalised Reasoning (Exeter, United Kingdom).
2012 Program Committee, 3rd Workshop on Controlled Natural Language (Zurich, Switzerland).
2012 Program Committee, 10th International Workshop On User Interfaces for Theorem Provers (Bremen, Germany).
2012 Program Committee, 2nd International Workshop on Proof Exchange for Theorem Proving (Manchester, United Kingdom).
2012 Program Committee, 3rd Workshop on Practical Aspects of Automated Reasoning (Manchester, United Kingdom).
2012 Program Committee, 6th International Joint Conference on Automated Reasoning (Manchester, United Kingdom).
2012 Program Committee, Alan Turing Centenary Conference (Manchester, United Kingdom).
2012 Program Committee, 9th International Workshop on the Implementation of Logics (Merida, Venezuela).
2011 Program Committee, 23rd International Conference on Automated Deduction (Wroclaw, Poland).
2011 Program Committee, 1st Workshop on Automated Theory Engineering (Wroclaw, Poland).
2011 Program Committee, 1st Workshop on Proof eXchange for Theorem Proving (Wroclaw, Poland).
2010 Program Committee, Workshop on Controlled Natural Language 2010 (Marettimo Island, Italy).
2010 Program Committee, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Yogyakarta, Indonesia).
2010 Program Committee, 5th International Joint Conference on Automated Reasoning (Edinburgh, United Kingdom).
2010 Program Committee, IJCAR 2010 Workshop on Practical Aspects of Automated Reasoning (Edinburgh, United Kingdom).
2010 Program Committee, 9th International Workshop on User Interfaces for Theorem Provers (Edinburgh, United Kingdom).
2010 Program Committee, 16th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Dakar, Senegal).
2009 Program Committee, IJCAI-09 workshop on Competitions in Artificial Intelligence and Robotics (Pasedena, USA).
2009 Program Committee, 32nd Annual Conference on Artificial Intelligence (Paderborn, Germany).
2009 Program Committee, 22nd International Conference on Automated Deduction (Montreal, Canada).
2008 Program Committee, 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning (Doha, Qatar).
2008 Program Committee, 7th International Workshop on the Implementation of Logics (Doha, Qatar).
2008 Program Committee, User Interfaces for Theorem Provers 2008 (Montreal, Canada).
2008 Program Committee, IJCAR 2008 Workshop on Practical Aspects of Automated Reasoning (Sydney, Australia).
2008 Program Committee, 4th International Joint Conference on Automated Reasoning (Sydney, Australia).
2007 Program Committee, IEEE International Conference on Tools with Artificial Intelligence (Patras, Greece).
2007 Program Co-chair, 20th International FLAIRS Conference (Key West, USA).
2006 Program Committee, 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (Phnom Penh, Cambodia).
2006 Program Committee, 3rd European STarting AI Researcher Symposium (Palacongressi, Italy).
2006 Program Committee, 3rd International Joint Conference on Automated Reasoning (Seattle, USA).
2006 Program Co-chair, 19th International FLAIRS Conference (Melbourne Beach, USA).
2006 Program Committee, Special Track on Natural Language and Knowledge Representation, 19th International FLAIRS Conference (Melbourne Beach, USA).
2005 Program Co-chair, 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (Montego Bay, Jamaica).
2005 Program Committee, LPAR-12 Workshop on Empirically Successful Reasoning in Higher Order Logic (Montego Bay, Jamaica).
2005 Program Committee, 20th International Conference on Automated Deduction (Tallinn, Estonia).
2005 Program Committee, 5th International Workshop on the Implementation of Logics (Montevideo, Uruguay).
2005 Program Committee, 18th International FLAIRS Conference (Clearwater Beach, USA).
2004 Program Committee, 17th International FLAIRS Conference (Miami, USA).
2003 Program Committee, Workshop on Agents and Automated Reasoning, 18th International Joint Conference on Artificial Intelligence (Acapulco, Mexico).
2003 Program Committee, 16th International FLAIRS Conference (St Augustine, USA).
2002 Program Committee, 18th International Conference on Automated Deduction (Copenhagen, Denmark).
2002 Program Committee, 15th International FLAIRS Conference (Pensacola, USA).
2001 Program Committee, 14th Australian Joint Conference on Artificial Intelligence (Adelaide, Australia).
2001 Program Committee, 2nd Australasian Workshop on Computational Logic (Gold Coast, Australia).
2001 Program Committee, Workshop on Empirical Methods in Artificial Intelligence, 17th International Joint Conference on Artificial Intelligence (Seattle, USA).
2000 Program Committee, Workshop on Empirical Methods in Artificial Intelligence, 14th European Conference on Artificial Intelligence (Berlin, Germany).
1999 Program Committee, Special Track on Parallel and Distributed Reasoning, 12th International Florida Artificial Intelligence Research Symposium (Orlando, USA).
1999 Program Committee, 12th Australian Joint Conference on Artificial Intelligence (Sydney, Australia).
1998 Program Committee, 6th International Conference on the Practical Application of Prolog (London, England).
1997 Program Committee, 14th International Conference on Automated Deduction (Townsville, Australia).
1997 Program Committee, Special Track on Using AI Methods to Control Automated Deduction, 10th Florida Artificial Intelligence Research Symposium, (Daytona Beach, USA).
1996 Program Committee, 13th International Conference on Automated Deduction (New York, USA).
1996 Program Committee, Special Track on Controlling Search in Automated Reasoning Systems, 9th Florida Artificial Intelligence Research Symposium (Key West, USA).
Conference Management

Conference Management

2024 Publicity Chair, 30th International Conference on Automated Deduction (Stuttgart, Germany).
2024 Conference Chair, 25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Balaclava, Mauritius).
2023 Workshop Chair, 13th TPTP Tea Party (Saclay, France).
2023 Conference Chair, 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Manizales, Colombia).
2022 Publicity Chair, 11th International Joint Conference on Automated Reasoning (Haifa, Israel).
2020 Conference Chair, 6th Global Conference on Artificial Intelligence (Hangzhou, China - Online).
2019 Publicity Chair, 27th International Conference on Automated Deduction (Natal, Brazil).
2018 Conference Chair, 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (Awassa, Ethiopia).
2018 LRG Representative, 4th Global Conference on Artificial Intelligence (Luxembourg).
2018 Publicity Chair, 9th International Joint Conference on Automated Reasoning (Oxford, United Kingdom).
2017 Conference Chair, 3rd Global Conference on Artificial Intelligence (Miami, USA).
2017 Conference Chair, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Maun, Botswana).
2017 Program Co-chair, 12th International Workshop on the Implementation of Logics (Maun, Botswana).
2016 Program Co-chair, 2nd Global Conference on Artificial Intelligence (Berlin, Germany).
2015‑ongoing Member of the Steering Committee, Linking Research Globally.
2013 Conference Co-chair, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Stellenbosch, South Africa).
2013 Co-organizer, 10th International Workshop on the Implementation of Logics (Stellenbosch, South Africa).
2013 Organizer, StarExec Workshop 2013 (Lake Placid, USA).
2013‑ongoing President, Florida Artificial Intelligence Research Society.
2012 Organizer, 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (Manchester, United Kingdom).
2012 Organizer, IJCAR 2012 StarExec Workshop (Manchester, United Kingdom).
2012 Satellite Events co-chair, 6th International Joint Conference on Automated Reasoning (Manchester, United Kingdom).
2012 Conference Chair, 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Merida, Venezuela).
2011‑2017 Member of the Board of Trustees, International Conference on Automated Deduction.
2006‑ongoing Member of the Steering Committee, International Conference on Logic for Programming Artificial Intelligence and Reasoning.
2005‑2013 Vice-president, Florida Artificial Intelligence Research Society.
2010 Organizer, Dagstuhl Workshop, QSTRLib: A Benchmark Problem Repository for Qualitative Spatial and Temporal Reasoning (Dagstuhl, Germany).
2010 Publicity Chair, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Yogyakarta, Indonesia).
2010 Organizer, 8th International Workshop on the Implementation of Logics, (Yogyakarta, Indonesia).
2010 Organizer, IJCAR 2010 Workshop on Evaluation Methods for Solvers, and Quality Metrics for Solutions, (Edinburgh, United Kingdom).
2004‑2010 Member of the Board of Trustees, International Conference on Automated Deduction.
2008 Organizer, The LPAR 2008 Workshop on Knowledge Exchange: Automated Provers and Proof Assistants (Doha, Qatar).
2008 Organizer, CICM 2008 Workshop on Empirically Successful Automated Reasoning for Mathematics (Birmingham, United Kingdom).
2008 Publicity chair, 4th International Joint Conference on Automated Reasoning (Sydney, Australia).
2008 Conference chair, 21st International FLAIRS Conference (Coconut Grove, USA).
2007 Organizer, Workshop on Empirically Successful Automated Reasoning in Large Theories, 21st International Conference on Automated Deduction (Bremen, Germany).
2007 Judge, 2007 SAT Competition.
2006 Organizer, 6th International Workshop on the Implementation of Logics, 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, (Phnom Penh, Cambodia).
2006 Organizer, Workshop on Empirically Successful Computerized Reasoning, 2006 Federated Logic Conference (Seattle, USA).
2005 Conference Chair, 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (Montego Bay, Jamaica).
2005 Organizer, Workshop on Empirically Successful Classical Automated Reasoning, 20th International Conference on Automated Deduction (Tallinn, Estonia).
2004 Organizer, Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning (Cork, Ireland).
2004 Local Arrangements Co-chair, 17th International FLAIRS Conference (Miami, USA).
2003 Conference Chair, 19th International Conference on Automated Deduction (Miami, USA).
2002 Organizer, Problems and Problem Sets Workshop, 18th International Conference on Automated Deduction (Copenhagen, Denmark).
2001 Coorganizer, Workshop on Empirical Methods in Artificial Intelligence, 17th International Joint Conference on Artificial Intelligence (Seattle, USA).
2000 Coorganizer, Workshop on Empirical Methods in Artificial Intelligence, 14th European Conference on Artificial Intelligence (Berlin, Germany).
1997 Conference Chair, 14th International Conference on Automated Deduction (Townsville, Australia).
1996‑ongoing Organizer, CADE ATP System Competition.
1996 Organising Committee, ECAI-96 Workshop on Empirical Artificial Intelligence, European Conference on Artificial Intelligence (Budapest, Hungary),
1996 Local Arrangements Committee, Pacific Rim International Conference on Artificial Intelligence (Cairns, Australia).
1995 Local Arrangements Committee, Winter School in Artificial Intelligence, Department of Computer Science, James Cook University (Magnetic Island, Australia).
1994 Co-organiser, Workshop 2C - Evaluation of Automated Theorem Proving Systems, 12th International Conference on Automated Deduction (Nancy, France).
Society Memberships

Society Memberships

2021-ongoing Association for Computing Machinery.
1994‑ongoing Association for Automated Reasoning.
1994-1995 Association for Logic Programming.
1994 IEEE.
Service and Consulting

Service and Consulting

2021‑ongoing Member of the Advisory Committee of the Artificial Intelligence Research Center, Ulster University.
2021-ongoing Chief Scientific Officer, Articulate Software
2021-ongoing Member of Technical Committee, National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University.
2013‑ongoing Partner, Model Accuracy
2006‑2007 Sutcliffe G., Translation of SUMO from SUO-KIF to TPTP, and integration of TPTP tools into the Sigma knowledge engineering environment, Articulate Software.

Teaching

Teaching Interests

Teaching Interests

Teaching Experience

Nominated for a "2004 Excellence in Teaching Award".
Students Supervised

Students Supervised

2021‑ongoing PhD Supervisor, McKeown J., Reinforcement Learning for Guiding an Automated Theorem Proving System, University of Miami.
2021‑2021 Fulbright Scholar Co-mentor, Largacha Martinez, C., Flourishing AI, Fundacion Universitaria del Area Andin.
2020‑2021 MS Supervisor, McKeown J., Clause Representation for Proof Guidance using Neural Networks, University of Miami.
2014‑2015 PhD Supervisor, Arhami N., Automated Theorem Proving by Translation to Description Logic, University of Miami.
2012‑2014 MS Supervisor, Arhami N., The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics, University of Miami.
2012‑2014 MS Supervisor, Nassar M., Automated Theorem Proving using the TPTP Process Instruction Language, University of Miami.
2008‑2010 MS Supervisor, Watson P., A Survey of Arithmetic in Automated Theorem Proving, University of the West Indies.
2008‑2010 MS Supervisor, Dellis N., Using Controlled Natural Language for World Knowledge Reasoning, University of Miami.
2008‑2009 MS Supervisor, Kakkad A., Machine Learning for Automated Theorem Proving, University of Miami.
2007‑2008 MS Supervisor, Yerikalapudi A., Answer Extraction in Automated Reasoning, University of Miami.
2005-2006 MS Supervisor, Shen W., Automated Proofs of Relationships Between Modal Logic Systems, University of Miami.
2004‑2006 MS Supervisor, Moynihan K., Lascaux - An Intelligent Artistic Agent, University of Miami.
2003‑2005 MS Supervisor, Zhang Y., The Use of Lemmas for Solving Hard Automated Theorem Proving Problems, University of Miami.
2003‑2004 MS Supervisor, Gao Y., Automated Generation of Interesting Theorems, University of Miami.
2002‑2003 MS Supervisor, Dashti S., Proof Checking for 1st Order Automated Theorem Proving Systems, University of Miami (not completed).
2002‑2003 MS Supervisor, Zhou P., Interactive and Automated Proof Manipulation, University of Miami (not completed).
1998‑2003 MSc Supervisor, Brown M., Semantic Guidance for Linear ATP Systems, James Cook University.
1999 MSc Supervisor, Clark P., Theory Construction using ATP Systems, James Cook University, (not completed).
1994‑1995 MSc Supervisor, Rush M., Evaluating the Effect of Semantic Guidance on Automated Theorem Proving Systems, James Cook University, (not completed).
1994 MSc Supervisor, Nugroho L., A Programmer's Tool for Managing Persistent Object Structures, James Cook University.
1990 MAppSc Supervisor, Tabada W., An Analysis and Implementation of Linear Derivation Strategies, Edith Cowan University.
1999 BSc (Hons) Supervisor, Laki A., Tools for the Easy Realisation of Distributed Systems, (Hons 2A), James Cook University.
1999 BSc (Hons) Supervisor, Hutton C., DIGInet: A Prototype for a Digital Spatial Library with an Interactive GIS Interface for the Internet, (Hons 2A), James Cook University.
1998 BSc (Hons) Supervisor, Johnstone K., Intelligent WWW Search, (Hons 2A), James Cook University.
1998 BSc (Hons) Supervisor, Seyfang D., A Smart Switch ATP System, (Hons 2B), James Cook University.
1997 BSc (Hons) Supervisor, Fontana K., Automatic Analysis of Images: Segmentation of Lichen Areas on Leaves, (1st class), James Cook University
1997 BSc (Hons) Supervisor, Gunn A., POSEIDON: Processing of Electronic Source Information for Decision Ontogony, (1st class), James Cook University.
1995 BSc (Hons) Supervisor, Singh K., A Graphical User Interface for Automated Theorem Provers, (1st class), James Cook University.
1995 BSc (Hons) Supervisor, Cooney J., The TPTP Database System, James Cook University (with C. Dyreson).
1995 BSc (Hons) Supervisor, Brown M., An Intelligent Prolog Editor, (1st class), James Cook University (with A. Sloane).
1994 BSc (Hons) Supervisor, Jones K., FOLL - A Library of Routines for ATP Systems, James Cook University.
1994 BSc (Hons) Supervisor, Sharpe M., An Intelligent Document Understanding and Reproduction System, (1st class), James Cook University (With Ahmed N.).
1993 BSc (Hons) Supervisor, Ingham J., C-Linda, James Cook University.
1992 BAppSci (Hons) Supervisor, Bettermann S., An Implementation of DOS C-Linda, and Associated Problems, Edith Cowan University.
Theses Examined

Theses Examined

2024 Bachelor Thesis Examiner, Johns M., Modal Logic Problem Collection, Universität Greifswald.
2023 PhD Committee, Bonnell J., Natural Language Processing in Cultural Heritage Domains: Integrating Pretrained Language Models with Rule-based Systems for Historical Japanese Corpora, Department of Computer Science, University of Miami.
2023 PhD Monitoring Committee, Al Wardani F., Formal Reasoning using Distributed Assertions, Institut Polytechnique de Paris.
2022 PhD Committee, Vukmirović P., Implementation of Higher-Order Superposition, Theoretical Computer Science, Vrije Universiteit Amsterdam.
2017‑2019 PhD Reading Committee, Groenouwe C., Fostering Technically Augmented Human Collective Intelligence, Department of Information and Computing Sciences, Universiteit Utrecht.
2019 MS Committee, Peña P., An Omni-directional Kick Engine for NAO Humanoid Robot, Department of Computer Science, University of Miami.
2018‑2019 PhD Committee, Dhrif H., Multi-Objective Particle Swarm Optimization Algorithms for Feature Engineering in Bioinformatics, Department of Computer Science, University of Miami.
2018 PhD Committee, Steen A., Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III, Department of Mathematics and Computer Science, Freie Universität Berlin.
2017‑2018 PhD Committee member, Küçük-McGinty H., Knowledge Acquisition and Representation Methodology and its Applications, Department of Computer Science, University of Miami.
2016‑2017 PhD Committee, Sidker F., Faulty and Reliable Sensors Detection, Human Fall Detection, and Activity Recognition and Monitoring from Sensor Readings, Department of Computer Science, University of Miami.
2016 MS Committee, Maheshwari P., A Model-based Sensor Database for the Internet of Things, Department of Computer Science, University of Miami.
2016 Licentiate Discussion Leader, Kotelnikov E., First-order Boolean Logic, Department of Computer Science and Engineering, Chalmers University.
2015‑2016 Habilitation Thesis Reviewer, Kaliszyk C., Learning Assisted Automated Reasoning, Institute of Computer Science, University of Innsbruck.
2015 MS Committee, Rossembayev A., Secure Data Aggregation for Sensor Networks in the Presence of Collusion Attack using Local Outlier Factors, Department of Computer Science, University of Miami.
2015 PhD Committee, Seekircher A., Stable and Flexible Walking Motions for Physical Humanoid Robots, Department of Computer Science, University of Miami.
2014‑2015 MSc Examiner, Rose Z-A., Artificial Intelligence E-Learning - A Flash Based Approach, Mona Institute of Applied Sciences, University of the West Indies.
2010‑2015 PhD Committee, Osterberg L., Technology-Based Training for Evidence-Based Practive in Mental Health, Department of Psychology, University of Miami.
2009‑2011 PhD Committee, Dendamrongvit S., Induction of Hierarchical Multi-label Text-categorizers, Department of Computer Systems Engineering, University of Miami.
2010 MS Committee, Alkhawaja M., Semantic Geospatial Search and Ranking in the Context of the Geographical Information System TerraFly, Department of Computer Science, University of Miami.
2010 MS Committee, Abeyruwan A., PrOntoLearn: Unsupervised Lexico-Semantic Ontology Generation using Probabilistic Methods, Department of Computer Science, University of Miami.
2006‑2008 PhD Committee, Trac S., Robust Explicit Construction of 3D Configuration Spaces using Controlled Linear Perturbation, Department of Computer Science, University of Miami.
2005‑2008 PhD Committee, Kool J., An Individual-based Approach for Modelling Genetic Processes in Population Networks, Rosenstiel School of Marine and Atmoshperic Science, University of Miami.
2007 MS Committee, Roach R., Focus Based Semantic Analysis, Department of Electrical and Computer Engineering, University of Miami.
2006‑2007 MS Committee, Puzis Y., Robust Arrangement Construction Using Linear Programming, Department of Computer Science, University of Miami.
2004 PhD Committee, Haroun P., Enhancing Theorem Provers by Delayed Clause Construction and Attribute Sequences, McGill University.
2003 MS Committee, Rupenaguntla S., FAM-based Call Admission Control Algorithms for Interference Limited Mobile Cellular CDMA Systems, Department of Computer Science, University of Miami.
2002 MS Committee, Niu A., SSH Wizard, Department of Computer Science, University of Miami.
2000 MS Committee, Mei X., Medical Information Systems, University of Miami.
1990 MSc Examiner, Roberts T., The Development of an Expert System for the Diagnosis of Diseases in Fibre and Dairy Goats, Western Australian College of Advanced Education.

Service

University Service

University Service

2024 Member of the Prototype Research Collaboration Network, University of Miami.
2023 Member of the Faculty Search Committee, Department of Computer Science, University of Miami.
2023-ongoing Member of the University Curriculum Committee, University of Miami.
2023-ongoing Chairman of the College of Arts and Science Council, University of Miami.
2023 Designed the BA DS&AI major for the Department of Computer Science, University of Miami.
2022-ongoing Chairman of the College of Arts and Sciences General Education Review Committee, University of Miami.
2022 Designed the BS DS&AI major for the Department of Computer Science, University of Miami.
2021-2023 Member of the College of Arts and Science Council, University of Miami.
2021-ongoing Disciplinary Hearing Faculty Panelist for the Dean of Students Office, University of Miami.
2020-2020 Member of the College of Arts and Science Curriculum Committee, University of Miami.
2018 Interviewer for Singer/Hammond Scholarships, University of Miami.
2017-ongoing Member of the University Termination for Cause Committee University of Miami.
2017 Interviewer for Singer/Hammond Scholarships, University of Miami.
2014-2020 Chairman of the Department of Computer Science, University of Miami.
2014-2018 Board of Advisors for UMiami Scientifica Magazine, University of Miami.
2012-2019 Chairman of the College of Arts and Science Curriculum Committee, University of Miami.
2011-2017 Member of the University Curriculum Committee, University of Miami.
2011 Member of the Faculty Search Committee, Department of Computer Science, University of Miami.
2007 Member of the Science Leadership Committee, College of Arts and Sciences, University of Miami.
2006-2010 Member of the University Curriculum Committee, University of Miami.
2005-2012 Member of the College of Arts and Science Curriculum Committee, University of Miami.
2003-2008 Advisor to the University of Miami SCUBA Club, University of Miami.
2002-2010 Convener of Seminar Series, Department of Computer Science, University of Miami.
2001-2014 Director of Undergraduate Studies, Department of Computer Science, University of Miami.
2001-2003 Member of the Working Group on General Education/Distribution Requirements, University of Miami.
2000 Academic Advisor, School of Information Technology, James Cook University.
1999-2000 Faculty Executive, Faculty of Science and Engineering, James Cook University.
1998-1999 Head of Computer Science, School of Computer Science, Mathematics, and Physics, James Cook University.
1997-2000 Board of Studies, Faculty of Science and Engineering, James Cook University.
1997-1999 School Executive, School of Computer Science, Mathematics, and Physics, James Cook University.
1997-1999 Academic Advisor, School of Computer Science, Mathematics, and Physics, James Cook University.
1997 Teaching Committee, Department of Computer Science, James Cook University.
1995 Teaching Committee, Department of Computer Science, James Cook University.
1995 Administration Committee, Department of Computer Science, James Cook University.
1993-1995 Library Liason Officer, Department of Computer Science, James Cook University.
1993 Equal Opportunity planning, James Cook University.
1993 Board of Environmental Studies, James Cook University.
Community Service

Community Service

2019 Judge, Congressional App Challenge.
2007 Final Presentation Examiner, McFatter Technical Center.
2006 Java Engagement for Teacher Training (JETT) Workshop II, University of Miami.
2006 Java Engagement for Teacher Training (JETT) Workshop I, University of Miami.

Awards

Awards

2023 Listed in the Stanford University list of " World's Top 2% Scientists".
2023 Best Paper Award
Steen A., Sutcliffe G., Scholl T., Benzmüller C. (2023), Solving Modal Logic Problems by Translation to Higher-order Logic, Herzig A., Luo J., Pardo P., Proceedings of the 5th International Conference on Logic and Argumentation (Hangzhou, China), Lecture Notes in Computer Science 14156, 25-43.
2023 Thoralf Skolem Award (for CADE papers that have passed the test of time)
Sutcliffe G., Suttner C., Yemenis T. (1994), The TPTP Problem Library, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), Lecture Notes in Artificial Intelligence 814, 252-266.