| Sutcliffe G. (2006), Semantic Derivation Verification, International Journal on Artificial Intelligence Tools, To appear. (PDF) |
| Sutcliffe G. (2006), The CADE-20 Automated Theorem Proving Competition, AI Communications, To appear. (PDF) |
| Sutcliffe G., Suttner, C. (2006), The State of CASC, AI Communications 19(1), 35-48. (PDF) |
| Sutcliffe G. (2005), The IJCAR-2004 Automated Theorem Proving Competition, AI Communications 18(1), pp.33-40. (PDF) |
| Sutcliffe G., Suttner C.B., (2004), The CADE-19 ATP System Competition, Artificial Intelligence Communications 17(3), pp 103-110. (PDF) |
| 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, pp.201-215. (PDF) |
| Sutcliffe G., Suttner C.B., (2003), The CADE-18 ATP System Competition, Journal of Automated Reasoning 31(1), pp.23-32. (PDF) |
| Pelletier F.J., Sutcliffe G., Suttner C.B. (2002), The Development of CASC, AI Communications 15(2-3), pp.79-90. (PDF) |
| Sutcliffe G., Suttner C.B., Pelletier F.J. (2002), The IJCAR ATP System Competition, Journal of Automated Reasoning 28(3), pp.307-320. (PDF) |
| Sutcliffe G. (2001), The CADE-17 ATP System Competition, Journal of Automated Reasoning 27(3), pp.227-250. (PS) |
| Sutcliffe G., Suttner C. (2001), Evaluating General Purpose Automated Theorem Proving Systems, Artificial Intelligence Journal 131(1-2), pp.39-54. (PDF) |
| Sutcliffe G. (2000), The CADE-16 ATP System Competition, Journal of Automated Reasoning 24(3), pp.371-396. (PS) |
| Gunn A., Sutcliffe G., Walker D. (1999), Knowledge Acquisition for Natural Resource Management, Computers and Electronics in Agriculture 23(1), pp.71-82. (PDF) |
| Sutcliffe G., Suttner C.B. (1999), The CADE-15 ATP System Competition, Journal of Automated Reasoning 23(1), pp.1-23. (PS) |
| Suttner C.B., Sutcliffe G. (1998), The CADE-14 ATP System Competition, Journal of Automated Reasoning 21(1), pp.99-134. (PS) |
| Sutcliffe G., Suttner C.B. (1998), The TPTP Problem Library: CNF Release v1.2.1, Journal of Automated Reasoning 21(2), pp.177-203. (PS) |
| Pelletier F.J., Sutcliffe G. (1997), An Erratum for Some Errata to ATP Problems, Journal of Automated Reasoning 18(1), p.135. (PS) |
| Suttner C.B., Sutcliffe G. (1997), The Design of the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), pp.139-162. (PS) |
| Sutcliffe G., Suttner C.B. (1997), The Procedures of the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), pp.163-169. (PS) |
| Sutcliffe G., Suttner C.B. (1997), The Results of the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), pp.271-286. (PS) |
| Pelletier F.J., Sutcliffe G., Suttner C.B. (1997), Conclusions about the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), pp.287-296. (PS) |
| Sutcliffe G., Melville S. (1996), The Practice of Clausification in Automated Theorem Proving, South African Computer Journal, pp.57-68. (PDF) |
| Sutcliffe G. Tabada W. (1991), Compulsory Reduction in Linear Derivation Systems, Bibel W. (Ed.), Artificial Intelligence (Letters to the Editor) 50, pp.131-132, Elsevier Science, Amsterdam, The Netherlands. (PDF) |
| Sutcliffe G. (1985), A Comparison of Methods used to Represent Graphs on a Computer, Bishop J. (Ed.), Quaestiones Informatica 4(1), pp.1-11, Computer Society Press, Johannesburg, South Africa. |
| Sutcliffe G. (1985), GRAPHIX - A Graph Theory Sub-language, The International Journal of Computer Mathematics 17(3&4), pp.257-276, Gordon and Breach, England. |
| 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, Springer-Verlag, To appear. (PDF) |
| 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, Springer-Verlag, To appear. (PDF) |
| 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). (PDF) |
| 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), pp.840-841. (PDF) |
| Sutcliffe G., Belfiore D. (2005), Semantic Derivation Verification, Russell I. Markov Z., Proceedings of the 18th International FLAIRS Conference (Clearwater Beach, USA), pp.641-646, (3rd best paper award). (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), pp.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), pp.87-94. (PDF) |
| Zimmer J., Meier A., Sutcliffe G., Zhang Y. (2004), Integrated Proof Transformation Services, Benzmüller C. and 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., 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), pp.1-11. (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), pp.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), pp.108-112. (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. (Eds), 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. (Ed), Proceedings of the 18th International Conference on Automated Deduction, (Copenhagen, Denmark), Lecture Notes in Artificial Intelligence 2392, pp.280-284. (PDF) |
| Fuchs M., Sutcliffe G. (2002), Homogeneous Sets of ATP Problems, Proceedings of the 15th International FLAIRS Conference (Pensecola, USA), pp.57-61. (PS) |
| 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, pp.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), pp.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), pp.53-60. (PDF) |
| Brown M., Sutcliffe G. (2000), PTTP+GLiDeS - Semantically Guided PTTP, McAllester D. (Ed), Proceedings of the 17th International Conference on Automated Deduction (Pittsburgh, USA), Lecture Notes in Artificial Intelligence 1831, pp.411-416. (PDF) |
| Sutcliffe G. (2000), SystemOnTPTP, McAllester D. (Ed), Proceedings of the 17th International Conference on Automated Deduction (Pittsburgh, USA), Lecture Notes in Artificial Intelligence 1831, pp.406-410. (PDF) |
| Brown M., Sutcliffe G. (2000), PTTP+GLiDeS - Using Models to Guide Linear Deductions, Baumgartner P., Fermueller C., Peltier N., Zhang H. (Eds), 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. (Ed), Proceedings of the 12th Australian Joint Conference on Artificial Intelligence (Sydney, Australia), Lecture Notes in Artificial Intelligence 1747, Springer-Verlag, pp.244-254. (PDF) |
| Sutcliffe G., Seyfang D. (1999), Smart Selective Competition Parallelism ATP, Kumar A., Russell I. (Eds), Proceedings of the 12th International FLAIRS Conference (Orlando, USA), AAAI Press, pp.341-345. (PDF) |
| Suttner C.B., Sutcliffe G., (1996), The Design of the CADE-13 ATP System Competition, McRobbie M., Slaney J. (Eds), Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), Lecture Notes in Artificial Intelligence 1104, pp.146-160. |
| Melville S., Sutcliffe G., Fraser D. (1996), Using Artificial Neural Networks for Meteor-Burst Communications Trail Prediction, Foo N., Goebel R. (Eds), Proceedings of PRICAI'96: The 4th Pacific Rim Conference on Artificial Intelligence (Cairns, Australia), Lecture Notes in Computer Science 1114, pp.423-434. (PDF) |
| Sutcliffe G., Suttner C., Yemenis T. (1994), The TPTP Problem Library, Bundy A. (Ed), Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), Lecture Notes in Artificial Intelligence 814, pp.252-266. (PS) |
| Sutcliffe G., Wu X. (1994), Extracting Rule Schemas from Rules, for an Intelligent Learning Database System, Zhang C., Debenham J. (Eds), Proceedings of the 7th Australian Joint Conference on Artificial Intelligence (Armidale, Australia), pp.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), pp.267-271. |
| Sutcliffe G. (1993), A Comparison of Mechanisms for Avoiding Repetition of Subdeductions in Chain Format Linear Deduction Systems, Voronkov A. (Ed.), Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (St Petersburg, Russia), Lecture Notes in Artificial Intelligence 698, pp. 321-332. (PS) |
| Sutcliffe G. (1992), Linear-Input Subset Analysis, Kapur, D. (Ed.), Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, USA), Lecture Notes in Artificial Intelligence 607, pp.268-280. (PDF) |
| Sutcliffe G. (1992), The Semantically Guided Linear Deduction System, Kapur, D. (Ed.), Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, USA), Lecture Notes in Artificial Intelligence 607, pp.677-680. (PDF) |
| Sutcliffe G., and Pinakis J. (1992), Prolog-D-Linda : An Embedding of Linda in SICStus Prolog, DeGroot D., Kacsuk P., Succi G., Talia D. (Eds.), Proceedings of the Joint Workshop on Distributed and Parallel Implementation of Logic Programming Systems (Washington, USA), pp.70-79. (PDF) |
| Sutcliffe G. (1992), A Heterogeneous Parallel Deduction System, Hasegawa R., Stickel M. E. (Eds.), 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. (Ed.), Proceedings of PPAI-91, International Workshop on Parallel Processing for Artificial Intelligence (Sydney, Australia), pp.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. (Ed.), Proceedings of the Australian Computer Conference'91 (Adelaide, Australia), pp.77-86. |
| Sutcliffe G. (1990), A General Clause Theorem Prover, Stickel M.E. (Ed.), Proceedings of the 10th International Conference on Automated Deduction (Kaiserslautern, Germany), Lecture Notes in Artificial Intelligence 449, pp.675-676. (PDF) |
| Sutcliffe G. Pinakis J. (1990), Prolog-Linda - An Embedding of Linda in muProlog, Tsang C.P. (Ed.), Proceedings of the 4th Australian Conference on Artificial Intelligence (Perth, Australia), pp.331-340. (PDF) |