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 Publications

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.
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.
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.

Edited Volumes

Eiter T., Sands D., Sutcliffe G., Voronkov V. (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).

Journal Publications

Sutcliffe G. (2017), The TPTP Problem Library and Associated Infrastructure - From CNF to TH0, TPTP v6.4.0, Journal of Automated Reasoning, To appear.
Sutcliffe G. (2016), The 8th IJCAR Automated Theorem Proving System Competition - CASC-J8, AI Communications 29(5), 607-619.
Sutcliffe G. (2016), The CADE ATP System Competition - CASC, AI Magazine 37(2), 99-101.
Sutcliffe G., Urban J. (2016), The CADE-25 Automated Theorem Proving System Competition - CASC-25, AI Communications 29(3), 423-433.
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.
Urban J., Rudnicki P., Sutcliffe G. (2013), ATP and Presentation Service for Mizar Formalizations, Journal of Automated Reasoning 50(2), 229-241.
Sutcliffe G. (2012), The CADE-23 Automated Theorem Proving System Competition - CASC-23, AI Communications 25(1), 49-63.
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.
Pease A., Sutcliffe G., Siegel N., Trac S. (2010), Large Theory Reasoning with SUMO at CASC, AI Communications 23(2-3), 137-144.
Sutcliffe G. (2010), The CADE-22 Automated Theorem Proving System Competition - CASC-22, AI Communications 23(1), 47-60.
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)
Hoefner P., Struth G., Sutcliffe G. (2009), Automated Verification of Refinement Laws, Annals of Mathematics and Artificial Intelligence 55(1), 35-62. (DOI)
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)
Sutcliffe G. (2009), The 4th IJCAR Automated Theorem Proving System Competition - CASC-J4, AI Communications 22(1), 59-72. (DOI)
Rabe F., Pudlak P., Sutcliffe G., Shen W. (2009), Solving the $100 Modal Logic Challenge, Journal of Applied Logic 7(1), 113-130. (DOI)
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, International Journal on Artificial Intelligence Tools 15(6), 1053-1070.
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.
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. 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

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.
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.
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.
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

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. (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).
Invited Talks

Invited Talks

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).
Grants

Grants

2017-2020 US$999047 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$1857565 Stump A. (PI), Sutcliffe G. (PI), Tinelli C. (co-PI), StarExec: Cross-Community Infrastructure for Logic Solving, NSF Computing Research Infrastructure Grant. ($170297 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$99947 Stump A. (PI), Sutcliffe G. (PI), Tinelli C. (co-PI), *-EXEC: A Cross-Community Solver Execution Service, NSF Computing Research Infrastructure Grant. ($55742 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.
Consulting

Consulting

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.

Professional

Editing

Editing

2015-ongoing Editorial Board, Acta Informatica
2014-ongoing Editorial Board, Formalized Mathematics
2003 Benchmarks Area Editor, QPQ Repository for Deductive Software Components
Program Committees

Program Committees

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 - System & Projects track, 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

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‑ongoing 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.
1996‑ongoing Organizer, CADE ATP System Competition.
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 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).
Professional Society Memberships

Professional Society Memberships

1994-2010 Association for Automated Reasoning.
1994-1995 Association for Logic Programming.
1994 IEEE.

Teaching

Teaching Interests

Teaching Interests

Teaching Experience

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

Students Supervised

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

2017 PhD Reading Committee, Groenouwe C., Fostering Technically Augmented Human Collective Intelligence, Department of Information and Computing Sciences, Universiteit Utrecht.
2016‑2017 PhD Committee member, 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 member, 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 member, 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 member, 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 member, Osterberg L., Technology-Based Training for Evidence-Based Practive in Mental Health, Department of Psychology, University of Miami.
2009‑2011 PhD Committee member, Dendamrongvit S., Induction of Hierarchical Multi-label Text-categorizers, Department of Computer Systems Engineering, University of Miami.
2010 MS Committee member, 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 member, Abeyruwan A., PrOntoLearn: Unsupervised Lexico-Semantic Ontology Generation using Probabilistic Methods, Department of Computer Science, University of Miami.
2006‑2008 PhD Committee member, Trac S., Robust Explicit Construction of 3D Configuration Spaces using Controlled Linear Perturbation, Department of Computer Science, University of Miami.
2005‑2008 PhD Committee member, 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 member, Roach R., Focus Based Semantic Analysis, Department of Electrical and Computer Engineering, University of Miami.
2006‑2007 MS Committee member, Puzis Y., Robust Arrangement Construction Using Linear Programming, Department of Computer Science, University of Miami.
2004 PhD Examiner, Haroun P., Enhancing Theorem Provers by Delayed Clause Construction and Attribute Sequences, McGill University.
2003 MS Committee member, 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 member, Niu A., SSH Wizard, Department of Computer Science, University of Miami.
2000 MS Committee member, 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

2014-ongoing Board of Advisors for UMiami Scientifica Magazine, University of Miami.
2014-ongoing Chairman of the Department of Computer Science, University of Miami.
2012-ongoing Chairman of the College of Arts and Science Curriculum Committee, University of Miami.
2011-ongoing Member of the University Curriculum Committee, University of Miami.
2001-2014 Director of Undergraduate Studies, Department of Computer Science, University of Miami.
2011 Faculty Search Committee, Department of Computer Science, University of Miami.
2005-2012 Member of the College of Arts and Science Curriculum Committee, University of Miami.
2006-2010 Member of the University Curriculum Committee, University of Miami.
2002-2010 Convener of Seminar Series, Department of Computer Science, University of Miami.
2003-2008 Advisor to the University of Miami SCUBA Club, University of Miami.
2007 Member of the Science Leadership Committee, College of Arts and Sciences, 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.
1997-2000 Board of Studies, Faculty of Science and Engineering, James Cook University.
July 1998-1999 Head of Computer Science, School of Computer Science, Mathematics, and Physics, 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

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.