General

Personal

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

Education

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

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

Automated Theorem Proving (ATP)
Evaluation of ATP systems
Distributed and Parallel ATP systems

: 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. (2007), Special Issue: Empirically Successful Computerized Reasoning, Journal of Applied Logic, To appear.

Sutcliffe G., Urban J., Schulz S. (2007), Proceedings of the Workshop on Empirically Successful Automated Reasoning in Large Theories, 21sth 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

Urban J., Sutcliffe G. (2008), ATP-based Cross Verification of Mizar Proofs, Journal of Mathematics in Computer Science, To appear.

Sutcliffe G. (2008), The CADE-21 Automated Theorem Proving System Competition, AI Communications 21(1), 71-82.

Rabe F., Pudlak P., Sutcliffe G., Shen W. (2007), Solving the $100 Modal Logic Challenge, Journal of Applied Logic, To appear.

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, To appear.

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, To appear.

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.

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)

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.

Trac S., Puzis Y., Sutcliffe G. (2006), An Interactive Derivation Viewer, Autexier S., Benzmüller C., Proceedings of the 7th Workshop on 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., 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.

Sutcliffe G., Denney E., Fischer B. (2005), Practical Proof Checking for Program Certification, Sutcliffe G., Fischer B., Schulz S., Proceedings of the Workshop on Empirically Successful Classical Automated Reasoning, 20th International Conference on Automated Deduction (Tallinn, Estonia). (PDF)

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

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)

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.

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)

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)

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

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)

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

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)

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)

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, 1995), 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

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

2008	€TBA	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

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

2003	Benchmarks Area Editor, QPQ Repository for Deductive Software Components

Program Committees

2008	Program Committee, 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning (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

2008	Organizer, CICM 2008 Workshop on Empirically Successful Automated Reasoning for Mathematics (Birmingham, United Kingdom).
2008	Organizer, IJCAR 2008 Workshop on Evaluation of Systems for Higher Order Logic (Sydney, Australia).
2008	Publicity chair, 4th International Joint Conference on Automated Reasoning (Sydney, Australia).
2004‑2007	Member of the Board of Trustees, International Conference on Automated Deduction.
2005‑2007	Vice-president, Florida Artificial Intelligence Research Society.
1996‑2007	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

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

Teaching

Teaching Interests

Automated Theorem Proving
Artificial intelligence
Operating systems
Systems programming

Teaching Experience

Automated Theorem Proving
Artificial intelligence
Operating systems
Systems programming
Software development (programming, data structures, software engineering)
Introduction to Computer Science (analysis and design, programming, hardware, operating systems, theory, data structures)

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

Students Supervised

2008‑TBA	MS Supervisor, Kakkad A., Machine Learning with Semantics in Automated Reasoning, University of Miami.
2007‑TBA	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

2006‑TBA	PhD Committee member, Trac S., Title TBA, Department of Computer Science, University of Miami.
2005‑TBA	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.
2004‑TBA	PhD Committee member, Zhou W., Title TBA, Department of Computer 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

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

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.