General

Personal

Personal

Name Geoff Sutcliffe
Date of birth 28 October 1961
Place of birth N'dola, Zambia
Citizenship Australian and British
Residence USA
Education

Education

1992 PhD The University of Western Australia
1986 MSc University of Natal
1983 BSc (Hons) University of Natal
Employment

Employment

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

Schmidt R., Sutcliffe G., Schulz S. (2009), Special Issue: Empirically Successful Computerized Reasoning, Journal of Applied Logic, To appear.
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. (2009), The 4th IJCAR Automated Theorem Proving System Competition - CASC-J4, AI Communications, To appear.
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, To appear.
Hoefner P., Struth G., Sutcliffe G. (2009), Automated Verification of Refinement Laws, Annals of Mathematics and Artificial Intelligence, Special Issue on First-order Theorem Proving, To appear.
Urban J., Sutcliffe G. (2009), ATP-based Cross Verification of Mizar Proofs, Journal of Mathematics in Computer Science, To appear.
Rabe F., Pudlak P., Sutcliffe G., Shen W. (2009), Solving the $100 Modal Logic Challenge, Journal of Applied Logic, To appear.
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

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$aacute;k P., Vyskocil J. (2007), 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. (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), 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. (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).
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

2007 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, England.
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 (IJCAR), Siena, Italy.
Grants

Grants

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

2003 Benchmarks Area Editor, QPQ Repository for Deductive Software Components
Program Committees

Program Committees

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

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).
2004‑2008 Member of the Board of Trustees, International Conference on Automated Deduction.
2005‑2008 Vice-president, Florida Artificial Intelligence Research Society.
1996‑2008 Organizer, CADE ATP System Competition.
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-2006 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

2008‑TBA MS Supervisor, Kakkad A., Machine Learning for Automated Reasoning, 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

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

2007 Member of the Science Leadership Committee, College of Arts and Sciences, University of Miami.
2006-2007 Member of the University Curriculum Committee, University of Miami.
2005-2007 Member of the College of Arts and Science Curriculum Committee, University of Miami.
2003-2007 Advisor to the University of Miami SCUBA Club, University of Miami.
2001-2007 Director of Undergraduate Studies, Department of Computer Science, University of Miami.
2002-2007 Convener of Pizza Seminar Series, 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.
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.