TPTP Citations

The following is a summary of the papers which cite the TPTP Problem Library. The purpose of this index is to raise awareness about system evaluations and to foster the exchange of results.


Papers containing results for TPTP problems

Sutcliffe G., Urban J. (2016), The CADE-25 Automated Theorem Proving System Competition - CASC-25, AI Communications 29(3), 423-433.

Sutcliffe G. (2016), The 8th IJCAR Automated Theorem Proving System Competition - CASC-J8, AI Communications 29(5), 607-619.

Sutcliffe G. (2015), The 7th IJCAR Automated Theorem Proving System Competition - CASC-J7, AI Communications 28(4), 683-692.

Sutcliffe G. (2014), The CADE-24 Automated Theorem Proving System Competition - CASC-24, AI Communications 27(4), 405-416.

Külwein D. (2013), Machine Learning for Automated Reasoning, PhD thesis, Radboud University Nijmegen (Nijmegen, The Netherlands).

Sutcliffe G. (2013), The 6th IJCAR Automated Theorem Proving System Competition - CASC-J6, AI Communications 26(2), 211-223.

Sutcliffe G. (2012), The CADE-23 Automated Theorem Proving System Competition - CASC-23, AI Communications 25(1), 49-63.

Sutcliffe G. (2011), The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5, AI Communications 24(1), 75-89.

Sutcliffe G., Benzmüller C. (2010), Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure, Journal of Formalized Reasoning 3(1), 1-27.

Sutcliffe G. (2010), The CADE-22 Automated Theorem Proving System Competition - CASC-22, AI Communications 23(1), 47-60.

Roederer A., Puzis Y., Sutcliffe G. (2009), Divvy: A ATP Meta-system based on Axiom Relevance Ordering, Schmidt R., Proceedings of the 22nd International Conference on Automated Deduction (Montreal Canada), 157-162, Lecture Notes in Artificial Intelligence 5663, Springer-Verlag.

Sutcliffe G., Benzmüller C., Brown C.E., Theiss F. (2009), Progress in the Development of Automated Theorem Proving for Higher-order Logic, Schmidt R., Proceedings of the 22nd International Conference on Automated Deduction (Montreal Canada), 116-130, Lecture Notes in Artificial Intelligence 5663, Springer-Verlag.

Sutcliffe G. (2009), The 4th IJCAR Automated Theorem Proving System Competition - CASC-J4, AI Communications 22(1), 59-72.

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

Deshane T., Hu W., Jablonski P., Lin H., Lynch C., McGregor R. (2007), Encoding First Order Proofs in SAT, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 476-491, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.

Kuncak V., Rinard M. (2007), Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 215-230, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.

Pudlak P. (2007), Draft Thesis: Verification of Mathematical Proofs, Charles University (Prague, Czech Republic).

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), 295-310, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.

Sutcliffe G. (2007), The 3rd IJCAR Automated Theorem Proving Competition, AI Communications 20(2), 117-126.

Loechner B. (2006), Things to Know When Implementing KBO, Journal of Automated Reasoning 36(4), 289-310.

Sutcliffe G. (2006), The CADE-20 Automated Theorem Proving Competition, AI Communications 19(2), 173-181.

Benzmüller C., Sorge V., Jamnik M., Kerber M. (2005), Can a Higher-Order and a First-Order Theorem Prover Cooperate?, Baader F., Voronkov A., Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Montevideo, Uruguay), 415-431, Lecture Notes in Artificial Intelligence 3452, Springer-Verlag.

Koshimura M., Umeda M., Hasegawa R. (2005), Abstract Model Generation of Preprocessing Clause Sets, Baader F., Voronkov A., Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Montevideo, Uruguay), 67-78, Lecture Notes in Artificial Intelligence 3452, Springer-Verlag.

Marcinkowski J., Otop J., Stelmaszek G. (2005), On a Semantic Subsumption Test, Baader F., Voronkov A., Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Montevideo, Uruguay), 142-153, Lecture Notes in Artificial Intelligence 3452, Springer-Verlag.

Sutcliffe G. (2005), The IJCAR-2004 Automated Theorem Proving Competition, AI Communications 18(1), 33-40.

Ganzinger H., Nieuwenhuis R., Nivela P. (2004), Fast Term Indexing with Coded Context Trees, Journal of Automated Reasoning 32(2), 103-120.

Sutcliffe G., Suttner C. (2004), The CADE-19 ATP System Competition, AI Communications 17(3), 103-182.

Dixon L., Fleuriot J. (2003), IsaPlanner: A prototype Proof Planner in Isabelle, Baader F., Proceedings of the 19th International Conference on Automated Deduction (Miami, USA), 279-283, Lecture Notes in Artificial Intelligence 2741, Springer-Verlag.

Gaillourdet J-M., Hillenbrand T., Löchner B., Spies H. (2003), The New Waldmeister Loop at Work, Baader F., Proceedings of the 19th International Conference on Automated Deduction (Miami, USA), 317-321, Lecture Notes in Artificial Intelligence 2741, Springer-Verlag.

Ganzinger H., Stuber J. (2003), Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation, Baader F., Proceedings of the 19th International Conference on Automated Deduction (Miami, USA), 335-349, Lecture Notes in Artificial Intelligence 2741, Springer-Verlag.

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, AAAI Press.

Sutcliffe G., Suttner C. (2003), The CADE-18 ATP System Competition, Journal of Automated Reasoning 31(1), 23-32.

Sutcliffe G., Suttner C., Pelletier F.J. (2002), The IJCAR ATP System Competition, Journal of Automated Reasoning 28(3), 307-320.

Ganzinger H., Nieuwenhuis R., Nivela P. (2001), Context Trees, Gore R., Leitsch A., Nipkow T., Proceedings of the International Joint Conference on Automated Reasoning (Siena, Italy), 242-256, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag.

Hodas J.S., Tamura N. (2001), lolliCoP - A Linear Logic Implmentation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic, Gore R., Leitsch A., Nipkow T., Proceedings of the International Joint Conference on Automated Reasoning (Siena, Italy), 670-684, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag.

Nieuwenhuis R., Hillenbrand T., Riazanov A., Voronkov A. (2001), On the Evaluation of Indexing Techniques for Theorem Proving, Gore R., Leitsch A., Nipkow T., Proceedings of the International Joint Conference on Automated Reasoning (Siena, Italy), 257-271, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag.

Sutcliffe G., Suttner C.B., Pelletier F.J. (2001), The IJCAR ATP System Competition: All the Details, UM-CSC-2001-001, Department of Computer Science, University of Miami (Miami, USA).

Sutcliffe G. (2001), The CADE-17 ATP System Competition, Journal of Automated Reasoning 27(3), 227-250.

Sutcliffe G. (2000), The CADE-16 ATP System Competition, Journal of Automated Reasoning 24(3), 371-396.

Voronkov A. (2000), CASC-16 1/2, CSPP-4, Department of Computer Science, University of Manchester (Manchester, United Kingdom).

Denzinger J., Fuchs D. (1999), Cooperation of Heterogeneous Provers, Dean T., Proceedings of the 16th International Joint Conference on Artificial Intelligence (Stockholm, Sweden), 10-15, Morgan Kaufmann.

Draeger J., Wolf A. (1999), Strategy Parallelism and Lemma Evaluation, Kumar A., Russell I., Proceedings of the 12th International FLAIRS Conference (Orlando, USA), 361-365, AAAI Press.

Sutcliffe G., Suttner C.B. (1999), The CADE-15 ATP System Competition, Journal of Automated Reasoning 23(1), 1-23.

Wolf A., Letz R. (1999), Strategy Parallelism in Automated Theorem Proving, International Journal of Pattern Recognition and Artificial Intelligence 13(2), 219-245.

Denzinger J., Fuchs M. (1998), A Comparison of Equality Reasoning Heuristics, Bibel W., Schmitt P.H., Automated Deduction, A Basis for Applications, 361-382, Applied Logic Series II Systems and Implementation Techniques(9), Kluwer Academic Publishers.

Fuchs M., Wolf A. (1998), System Description: Cooperation in Model Elimination: CPTHEO, Kirchner C., Kirchner H., Proceedings of the 15th International Conference on Automated Deduction (Lindau, Germany), 42-46, Lecture Notes in Artificial Intelligence 1421, Springer-Verlag.

Fuchs M. (1998), A Feature-Based Learning Method for Theorem Proving, Mostow J., Rich C., Proceedings of the 15th National Conference on Artificial Intelligence (Madison, USA), 457-462, AAAI Press.

Fuchs M. (1998), System Description: Similarity-Based Lemma Generation for Model Elimination, Kirchner C., Kirchner H., Proceedings of the 15th International Conference on Automated Deduction (Lindau, Germany), 33-37, Lecture Notes in Artificial Intelligence 1421, Springer-Verlag.

Fuchs M. (1998), Relevancy-Based Lemma Selection for Model Elimination using Lazy Tableaux Enumeration, Prade H., Proceedings of the 13th European Conference on Artificial Intelligence (Brighton, Englan), 346-350, Wiley.

Peltier N. (1998), A New Method for Automated Finite Model Building Exploiting Failures and Symmetries, Journal of Logic and Computation 8(4), 511-543.

Sutcliffe G., Suttner C. (1998), The CADE-14 ATP System Competition, 98/01, Department of Computer Science, James Cook University (Townsville, Australia).

Suttner C.B., Sutcliffe G. (1998), The CADE-14 ATP System Competition, Journal of Automated Reasoning 21(1), 99-134.

Baumgartner P., Furbach U., Stolzenburg F. (1997), Computing Answers with Model Elimination, Artificial Intelligence 90, 135-176.

Denzinger J., Fuchs M., Fuchs M. (1997), High Performance ATP Systems by Combining Several AI Methods, Pollack M.E., Proceedings of the 15th International Joint Conference on Artificial Intelligence (Nagoya, Japan), 102-107, Morgan Kaufmann.

Fuchs D., Fuchs M. (1997), CoDe: A Powerful Prover for Problems of Condensed Detatchment, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 260-263, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.

Fuchs M., Fuchs D., Fuchs M. (1997), Solving Problems of Combinatory Logic with Genetic Programming, Koza J., Deb K., Dorigo M., Fogel D., Garzon M., Iba H., Riolo R., Proceedings of the 2nd Annual Conference on Genetic Programming (Stanford, USA), 102-110, Morgan Kaufmann.

Fuchs M., Fuchs M. (1997), Applying Case-based Reasoning to Automated Deduction, Leake D., Plaza E., Proceedings of the 2nd International Conference on Case-based Reasoning (Providence, USA), 23-32, Lecture Notes in Artificial Intelligence 1266, Springer-Verlag.

Fuchs M. (1997), Evolving Combinators, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 416-430, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.

Fuchs M. (1997), Flexible Re-enactment of Proofs, Costa E., Cardoso A., Proceedings of the 8th Portuguese Conference on Artificial Intelligence (Coimbra, Portugal), 13-24, Lecture Notes in Artificial Intelligence 1323, Springer-Verlag.

Fuchs M. (1997), Automatic Selection of Search-guiding Heuristics, Dankel D., Proceedings of the 10th International FLAIRS Conference (Daytona Beach, USA), 1-5, Florida AI Research Society.

Fuchs M. (1997), Case-based Reasoning for Automated Deduction, Dankel D., Proceedings of the 10th International FLAIRS Conference (Daytona Beach, USA), 6-10, Florida AI Research Society.

Fuchs M. (1997), Similarity-Based Lemma Generation for Model Elimination, Salzer G., Proceedings of FT97, International Workshop on First Order Theorem Proving (Hagenberg, Austria), 63-67, RISC-Linz Report 97-50, Johannes Kepler Universität.

Fuchs M. (1997), Learning Search Heuristics for Automated Deduction, PhD thesis, Universität Kaiserslautern (Kaiserslautern, Germany), and Schriftenreihe Forschungsergebnisse zur Informatik, Bd.34, Verlag Dr. Kovac.

Sutcliffe G., Suttner C.B. (1997), The Results of the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), 271-286.

Baumgartner P. (1996), Linear and Unit-Resulting Refutations for Horn Theories, Journal of Automated Reasoning 16(3), 241-319.

Egly U., Rath T. (1996), On the Practical Value of Different Definitional Translations to Normal Form, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 403-417, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.

Fuchs M. (1996), Experiments in the Heuristic Use of Past Proof Experience, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 523-537, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.

Fuchs M. (1996), Powerful Search Heuristics Based on Weighted Symbols, Level and Features, Stewman J.H., Proceedings of the 9th International FLAIRS Conference (Key West, USA), 449-453, Florida AI Research Society.

Gordon M. (1996), Set Theory, Higher Order Logic or Both?, von Wright J., Grundy J., Harrison J., Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (Turku, Finland), 191-201, Lecture Notes in Computer Science 1125, Springer-Verlag.

Harrison J. (1996), Optimizing Proof Search in Model Elimination, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 313-327, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.

Schütz H., Geisler T. (1996), Efficient Model Generation through Compilation, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 431-447, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.

Sutcliffe G., Suttner C. (1996), Mathematics in the TPTP Problem Library (v1.2.1), 96/15, Department of Computer Science, James Cook University (Townsville, Australia).

Alexander G. (1995), Proving First-Order Equality Theorems with Hyper-Linking, PhD thesis, University of North Carolina at Chapel Hill (Chapel Hill, USA).

Geddis D.F. (1995), Caching and Non-Horn Inference in Model Elimination Theorem Provers, PhD thesis, Stanford University (Stanford, USA).

Suttner C.B. (1995), Parallelization of Search-based Systems by Static Partitioning with Slackness, PhD thesis, Institut für Informatik, Technische Universität München (Munich, Germany), and Dissertationen zur künstlichen Intelligenz 101, Springer-Verlag.

Baumgartner P., Furbach U. (1994), PROTEIN: A PROver with a Theory Extension INterface, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), 769-773, Lecture Notes in Artificial Intelligence 814, Springer-Verlag.

Baumgartner P., Furbach U. (1994), Model Elimination Without Contrapositives, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), 87-101, Lecture Notes in Artificial Intelligence 814, Springer-Verlag.

de Waal D.A., Gallagher J.P. (1994), The Applicability of Logic Programming Analysis and Transformation to Theorem Proving, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), 207-221, Lecture Notes in Artificial Intelligence 814, Springer-Verlag.

de Waal D.A. (1994), Analysis and Transformation of Proof Procedures, PhD thesis, University of Bristol (Bristol, United Kingdom).

Goller C., Letz R., Mayr K., Schumann J. (1994), SETHEO V3.2: Recent Developments, Bundy A., Proceedings of the 12th International Conference on Automated Deduction (Nancy, France), 778-782, Lecture Notes in Artificial Intelligence 814, Springer-Verlag.

Letz R., Mayr K., Goller C. (1994), Controlled Integration of the Cut Rule into Connection Tableau Calculi, Journal of Automated Reasoning 13(3), 297-337.


Papers refering to the TPTP, without results

McCune W.W. (), Otter: An Automated Deduction System, http://www.cs.unm.edu/~mccune/otter/.

Matsuzaki T., Iwane H., Kobayashi M., Zhan Y., Fukasaku R., Kudo J., Anai H., Arai N. (2016), Race against the Teens - Benchmarking Mechanized Math on Pre-university Problems, Olivetti N., Tiwari A., Proceedings of the 8th International Joint Conference on Automated Reasoning (Coimbra, Portugal), 213-227, Lecture Notes in Artificial Intelligence 9706.

Sutcliffe G. (2016), The CADE ATP System Competition - CASC, AI Magazine 37(2), 99-101.

Sutcliffe G. (2016), Proceedings of the 8th IJCAR ATP System Competition (Coimbra, Portugal), http://www.tptp.org/CASC/J8/Proceedings.pdf.

Külwein D., Urban J. (2015), MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers, Journal of Automated Reasoning, To appear.

Schulz S., Sutcliffe G. (2015), Proof Generation for Saturating First-Order Theorem Provers, Delahaye D., Woltzenlogel Paleo B., All about Proofs, Proofs for All, 45-61, Mathematical Logic and Foundations 55, College Publications.

Sutcliffe G. (2015), Proceedings of the CADE-25 ATP System Competition (Berlin, Germany), http://www.tptp.org/CASC/25/Proceedings.pdf.

Arhami N. (2014), The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics, MSc thesis, Department of Computer Science, University of Miami (Miami, USA).

Benzmüller C., Woltzenlogel Paleo B. (2014), Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers, Schaub T., Proceedings of the 21st European Conference on Artificial Intelligence (Prague, Czech Republic), 93-98.

Kumar R., Myreen M., Norrish M., Owens S. (2014), CakeML: A Verified Implementation of ML, Sewell P, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, USA), 179-191, ACM Press.

Sutcliffe G. (2014), Proceedings of the 7th IJCAR ATP System Competition (Vienna, Austria).

Blanchette J., Paskevich A. (2013), TFF1: The TPTP Typed First-order Form with Rank-1 Polymorphism, Bonacina M.P., Proceedings of the 24th International Conference on Automated Deduction (Lake Placid, USA), 414-420, Lecture Notes in Artificial Intelligence 7898, Springer-Verlag.

Kovacs L., Voronkov A. (2013), First-Order Theorem Proving and Vampire, Sharygina N., Veith H., Proceedings of the 25th International Conference on Computer Aided Verification (St Petersburg, Russia), 1-35, Lecture Notes in Artificial Intelligence 8044, Springer-Verlag.

Külwein D., Urban J., Schulz S. (2013), E-MaLeS 1.1, Bonacina M.P., Proceedings of the 24th International Conference on Automated Deduction (Lake Placid, USA), 407-413, Lecture Notes in Artificial Intelligence 7898, Springer-Verlag.

Schulz S. (2013), Simple and Efficient Clause Subsumption with Feature Vector Indexing, Bonacina M.P., Stickel M., Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, 45-67, Lecture Notes in Artificial Intelligence 7788, Springer-Verlag.

Sutcliffe G. (2013), Proceedings of the 24th CADE ATP System Competition (Lake Placid, USA).

Schulz S. (2012), Fingerprint Indexing for Paramodulation and Rewriting, Gramlich B., Miller D., Sattler U., Proceedings of the 6th International Joint Conference on Automated Reasoning (Manchester, United Kingdom), 477-483, Lecture Notes in Artificial Intelligence 7364, Springer-Verlag.

Stickel M.E. (2012), SNARK - SRI's New Automated Reasoning Kit, \url{http://www.ai.sri.com/~stickel/snark.html}.

Sutcliffe G., Schulz S., Claessen K., Baumgartner P. (2012), The TPTP Typed First-order Form with Arithmetic, Bj{\o}rner N., Voronkov A., Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Merida, Venezuela), 406-419, Lecture Notes in Artificial Intelligence 7180, Springer-Verlag.

Sutcliffe G. (2012), Proceedings of the 6th IJCAR ATP System Competition (Manchester, England).

Carpenter C., Sutcliffe G. (2011), Sporcle goes AI, McCarthy P., Murray C., Proceedings of the 24th International FLAIRS Conference (Palm Beach, USA), To appear, AAAI Press.

Pease A. (2011), Ontology: A Practical Guide, Articulate Software Press.

Sutcliffe G. (2011), Proceedings of the CADE-23 ATP System Competition (Wroclaw, Poland).

Benzmüller C., Pease A. (2010), Progress in Automating Higher-order Ontology Reasoning, Proceedings of IJACR 2010 Workshop on Practical Aspects of Automated Reasoning (Edinburgh, United Kingdom).

Pease A., Benzmüller C. (2010), Ontology Archaeology: Mining a Decade of Effort on the Suggested Upper Merged Ontology, Proceedings of ECAI 2010 Workshop on Automated Reasoning about Context and Ontology Evolution (Lisbon, Portugal), 19-20.

Pease A., Sutcliffe G., Siegel N., Trac S. (2010), Large Theory Reasoning with SUMO at CASC, AI Communications 23(2-3), 137-144.

Sutcliffe G., Chang C., Ding L., McGuinness D., Pinheiro da Silva P. (2010), Different Proofs are Good Proofs, McGuinness D., Stump A., Sutcliffe G., Tinelli C., Proceedings of the IJCAR 2010 Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions (Edinburgh, United Kingdom).

Sutcliffe G. (2010), The TPTP World - Infrastructure for Automated Reasoning, Clarke E., Voronkov A., Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Dakar, Senegal), 1-12, Lecture Notes in Artificial Intelligence 6355, Springer-Verlag.

Sutcliffe G. (2010), Proceedings of the 5th IJCAR ATP System Competition (Edinburgh, United Kingdom).

Urban J., Sutcliffe G. (2010), Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar: Challenges and Initial Solutions, Autexier S., Proceedings of the 10th International Conference on Artificial Intelligence and Symbolic Computation (Paris, France), 132-146, Lecture Notes in Artificial Intelligence 6167, Springer-Verlag.

Harrison J. (2009), Handbook of Practical Logic and Automated Reasoning, Cambridge University Press.

Sutcliffe G. (2009), Proceedings of the CADE-22 ATP System Competition (Montreal, Canada).

Urban J., Sutcliffe G., Trac S., Puzis Y. (2009), Combining Mizar and TPTP Semantic Presentation and Verification Tools, Studies in Logic, Grammar and Rhetoric 18(31), 121-136.

Urban J., Sutcliffe G. (2009), ATP-based Cross Verification of Mizar Proofs: Method, Systems, and First Experiments, Journal of Mathematics in Computer Science 2(2), 231-251.

Benzmüller C. (2008), Automating Access Control Logics in Simple Type Theory with LEO-II, SEKI Technical Report SR-2008-01, Universität des Saarlandes (Saarbrücken, Germany).

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 Workshop on Practical Aspects of Automated Reasoning, 4th International Joint Conference on Automated Reasoning (Sydney, Australia), 66-70, CEUR Workshop Proceedings 373.

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 Workshop on Practical Aspects of Automated Reasoning, 4th International Joint Conference on Automated Reasoning (Sydney, Australia), 81-93, CEUR Workshop Proceedings 373.

Rabe F., Pudlak P., Sutcliffe G., Shen W. (2008), Solving the \$100 Modal Logic Challenge, Journal of Applied Logic 7(1), 113-130.

Raths T., Otten J. (2008), {\sf randoCoP}: Randomizing the Proof Search Order in the Connection Calculus, Schmidt R., Konev B., Schulz S., Proceedings of the Workshop on Practical Aspects of Automated Reasoning, 4th International Joint Conference on Automated Reasoning (Sydney, Australia), Accepted.

Sutcliffe G. (2008), Proceedings of the 4th IJCAR ATP System Competition (Sydney, Australia).

Trac S., Sutcliffe G., Pease A. (2008), Integration of the TPTPWorld into SigmaKEE, Schmidt R., Konev B., Schulz S., Proceedings of the Workshop on Practical Aspects of Automated Reasoning, 4th International Joint Conference on Automated Reasoning (Sydney, Australia), 103-114, CEUR Workshop Proceedings 373.

Baumgartner P. (2007), Logical Engineering with Instance-Based Methods, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 404-409, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.

Ge Y., Barrett C., Tinelli C. (2007), Solving Quantified Verification Conditions Using Satisfiability Modulo Theories, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 167-182, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.

Kuncak V., Hguyen H., Rinard M. (2007), Deciding Boolean Algebra with Presburger Arithmetic, Journal of Automated Reasoning 36(3), 213-239.

Navarro-P{\'e}rez J.A., Voronkov A. (2007), Encodings of Bounded LTL Model Checking in Effectively Propositional Logic, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 346-361, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.

Otop J. (2007), Solution to some Right Alternative Ring Problems, Ahrendt W., Baumgartner P., de Nivelle H., Proceedings of the CADE-19 Workshop on DISPROVING - Non-Theorems, Non-Validity, Non-Provability (Bremen, Germany).

Paulson L., Susanto K. (2007), Source-level Proof Reconstruction for Interactive Theorem Proving, Schneider K., Brandt J., Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (Kaiserslautern, Germany), 232-245, Lecture Notes in Computer Science 4732, Springer-Verlag.

Pudlak P. (2007), Semantic Selection of Premisses for Automated Theorem Proving, Urban J., Sutcliffe G., Schulz S., Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (Bremen, German), 27-44, CEUR Workshop Proceedings 257.

Sutcliffe G. (2007), Proceedings of the CADE-21 ATP System Competition (Bremen, Germany).

Sutcliffe G. (2007), TPTP, TSTP, CASC, etc., Diekert V., Volkov M., Voronkov A., Proceedings of the 2nd International Symposium on Computer Science in Russia (Ekaterinburg, Russia), 6-22, Lecture Notes in Computer Science 4649, Springer-Verlag.

Trac S., Puzis Y., Sutcliffe G. (2007), 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), 109-123, Electronic Notes in Theoretical Computer Science 174.

Urban J. (2007), MaLARea: a Metasystem for Automated Reasoning in Large Theories, Urban J., Sutcliffe G., Schulz S., Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (Bremen, German), 45-58, CEUR Workshop Proceedings 257.

Verchinine K., Lyaletski A., Paskevich A. (2007), System for Automated Deduction (SAD): A Tool for Proof Verification, Pfenning F., Proceedings of the 21st International Conference on Automated Deduction (Bremen, Germany), 398-403, Lecture Notes in Artificial Intelligence 4603, Springer-Verlag.

Baumgartner P., Schmidt R. (2006), Blocking and Other Enhancements for Bottom-Up Model Generation Methods, Furbach U., Shankar N., Proceedings of the 3rd International Joint Conference on Automated Reasoning (Seattle, USA), 125-139, Lecture Notes in Artificial Intelligence 4130.

Shen W. (2006), Automated Proofs of Equivalence of Modal Logic Systems, MSc thesis, Department of Computer Science, University of Miami (Miami, USA).

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), 67-81, Lecture Notes in Artificial Intelligence 4130.

Sutcliffe G., Suttner C. (2006), The State of CASC, AI Communications 19(1), 35-48.

Sutcliffe G. (2006), Semantic Derivation Verification: Techniques and Implementation, International Journal on Artificial Intelligence Tools 15(6), 1053-1070.

Sutcliffe G. (2006), Proceedings of the 3rd IJCAR ATP System Competition (Seattle, USA).

Urban J. (2006), MPTP 0.2: Design, Implementation, and Initial Experiments, Journal of Automated Reasoning 37(1-2), 21-43.

Urban J. (2006), MizarMode - An Integrated Proof Assistance Tool for the Mizar Way of Formalizing Mathematics, Journal of Applied Logic 4(4), 414-427.

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), 156-161, Lecture Notes in Artificial Intelligence 4130, Springer-Verlag.

Zimmer J., Autexier S. (2006), The MathServe System for Semantic Web Reasoning Services, Furbach U., Shankar N., Proceedings of the 3rd International Joint Conference on Automated Reasoning (Seattle, USA), 17-20.

Sutcliffe G., Belfiore D. (2005), Semantic Derivation Verification, Russell I., Markov Z., Proceedings of the 18th International FLAIRS Conference (Clearwater Beach, USA), 641-646, AAAI Press.

Sutcliffe G. (2005), Proceedings of the CADE-20 ATP System Competition (Tallinn, Estonia).

Colton S., Meier A., Sorge V., McCasland R. (2004), Automatic Generation of Classification Theorems for Finite Algebras, Rusinowitch M., Basin D., Proceedings of the 2nd International Joint Conference on Automated Reasoning (Cork, Ireland), 400-414, Lecture Notes in Artificial Intelligence 3097.

Denney E., Fischer B., Schumann J. (2004), Using Automated Theorem Provers to Certify Auto-generated Aerospace Software, Rusinowitch M., Basin D., Proceedings of the 2nd International Joint Conference on Automated Reasoning (Cork, Ireland), 198-212, Lecture Notes in Artificial Intelligence 3097.

Gao Y. (2004), Automated Generation of Interesting Theorems, MSc thesis, University of Miami (Miami, USA).

Loechner B. (2004), A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting, Rusinowitch M., Basin D., Proceedings of the 2nd International Joint Conference on Automated Reasoning (Cork, Ireland), 45-59, Lecture Notes in Artificial Intelligence 3097.

Meng J., Paulson L. (2004), Experiments on Supporting Interactive Proof Using Resolution, Rusinowitch M., Basin D., Proceedings of the 2nd International Joint Conference on Automated Reasoning (Cork, Ireland), 372-384, Lecture Notes in Artificial Intelligence 3097.

Riazanov A., Voronkov A. (2004), Efficient Checking of Term Ordering Constraints, Rusinowitch M., Basin D., Proceedings of the 2nd International Joint Conference on Automated Reasoning (Cork, Ireland), 60-74, Lecture Notes in Artificial Intelligence 3097.

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, 201-215, Frontiers in Artificial Intelligence and Applications 112, IOS Press.

Sutcliffe G. (2004), Proceedings of the 2nd IJCAR ATP System Competition (Cork, Ireland).

Tammet T. (2004), Chain Resolution for Semantic Web, Rusinowitch M., Basin D., Proceedings of the 2nd International Joint Conference on Automated Reasoning (Cork, Ireland), 307-320, Lecture Notes in Artificial Intelligence 3097.

Tsarkov D., Riazanov A., Bechhofer S., Horrocks I. (2004), Using Vampire to Reason with OWL, McIlraith S., Plexousakis D., van Harmelen F., Proceedings of the 3rd International Semantic Web Conference (Hiroshima, Japan), 471-485, Lecture Notes in Computer Science 3298, Springer-Verlag.

Urban J. (2004), MPTP - Motivation, Implementation, First Experiments, Journal of Automated Reasoning 33(3-4), 319-339.

Corfield D. (2003), Towards a Philosophy of Real Mathematics, Cambridge University Press.

Kutsia T. (2003), Equational Prover of Theorema, Nieuwenhuis R., Proceedings of the 14nd International Conference on Rewriting Techniques and Applications (Valencia, Spain), 267-379, Lecture Notes in Computer Science 2706, Springer-Verlag.

MacCartney B., McIlraith S., Amir E., Uribe T. (2003), Practical Partition-Based Theorem Proving for Large Knowledge Bases, Gottlob G., Walsh T., Proceedings of the 18th International Joint Conference on Artificial Intelligence (Acapulco, Mexico), 89-96.

Newborn M. (2003), Proofs of Twenty-Four 1.0-Rated Theorems in the TPTP Problem Library, SOCS-03.6, School of Computer Science, McGill University (Montreal, Canada).

Riazanov A., Voronkov A. (2003), Efficient Instance Retrieval with Standard and Relational Path Indexing, Baader F., Proceedings of the 19th International Conference on Automated Deduction (Miami, USA), 380-396, Lecture Notes in Artificial Intelligence 2741, Springer-Verlag.

Riazanov A., Voronkov A. (2003), Limited Resource Strategy in Resolution Theorem Proving, Journal of Symbolic Computation 36(1-2), 101-115.

Sutcliffe G. (2003), Proceedings of the CADE-19 ATP System Competition (Miami, USA).

Urban J. (2003), Translating Mizar for First Order Theorem Provers, Asperti A., Buchberger B., Davenport J.H., Proceedings of the 2nd International Conference on Mathematical Knowledge Management (Bertinoro, Italy), 203-215, Lecture Notes in Computer Science 2594, Springer-Verlag.

Urban J. (2003), MPTP 0.1, Dahn I., Vigneron L., Proceedings of RDP'03 - The Federated Conference on Rewriting, Deduction and Programming 2003 (Valencia, Spain), Electronic Notes in Theoretical Computer Science 86(1).

Audemard G., Benhamou B. (2002), Reasoning by Symmetry and Function Ordering in Finite Model Generation Reasoning, Voronkov A., Proceedings of the 18th International Conference on Automated Deduction (Copenhagen, Denmark), 226-240, Lecture Notes in Artificial Intelligence 2392, Springer-Verlag.

Colton S., Sutcliffe G. (2002), Automatic Generation of Benchmark Problems for Automated Theorem Proving Systems, Faltings B., Proceedings of the 7th International Symposium on Artificial Intelligence and Mathematics (Ft Lauderdale, USA), AI-M 4-2002..

Colton S. (2002), The HR Program for Theorem Generation, Voronkov A., Proceedings of the 18th International Conference on Automated Deduction (Copenhagen, Denmark), 285-289, Lecture Notes in Artificial Intelligence 2392, Springer-Verlag.

Fuchs M., Sutcliffe G. (2002), Homogeneous Sets of ATP Problems, Haller S., Simmons G., Proceedings of the 15th International FLAIRS Conference (Pensecola, USA), 57-61, AAAI Press.

Hillenbrand T., Löchner B. (2002), The Next Waldmeister Loop, Voronkov A., Proceedings of the 18th International Conference on Automated Deduction (Copenhagen, Denmark), 486-500, Lecture Notes in Artificial Intelligence 2392, Springer-Verlag.

Pelletier F.J., Sutcliffe G., Suttner C.B. (2002), The Development of CASC, AI Communications 15(2-3), 79-90.

Schulz S., Sutcliffe G. (2002), System Description: GrAnDe 1.0, Voronkov A., Proceedings of the 18th International Conference on Automated Deduction (Copenhagen, Denmark), 280-284, Lecture Notes in Artificial Intelligence 2392, Springer-Verlag.

Schulz S. (2002), A Comparison of Different Techniques for Grounding Near-Propositional CNF Formulae, Haller S., Simmons G., Proceedings of the 15th International FLAIRS Conference (Pensecola, USA), 72-76, AAAI Press.

Schumann J. (2002), Automated Theorem Proving in Software Engineering, Springer-Verlag.

Slaney J.K. (2002), A Benchmark Template for Substructural Logics, Sutcliffe G., Pelletier J., Suttner C.B., Proceedings of the CADE-18 Workshop - Problem and Problem Sets for ATP (Copenhagen, Denmark), Department of Computer Science, University of Copenhagen, Technical Report 02/10.

Sutcliffe G. (2002), Proceedings of the CADE-18 ATP System Competition (Copenhagen, Denmark).

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.B., Proceedings of the CADE-18 Workshop - Problem and Problem Sets for ATP (Copenhagen, Denmark), Department of Computer Science, University of Copenhagen, Technical Report 02/10.

Zimmer J., Kohlhase M. (2002), System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning, Voronkov A., Proceedings of the 18th International Conference on Automated Deduction (Copenhagen, Denmark), 139-143, Lecture Notes in Artificial Intelligence 2392, Springer-Verlag.

Avenhaus J., Löchner B. (2001), System Description: CCE: Testing Ground Joinability, Gore R., Leitsch A., Nipkow T., Proceedings of the International Joint Conference on Automated Reasoning (Siena, Italy), 658-662, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag.

Fyffe G., Horton J., He Y. (2001), Experiments with Marmoset, a Deduction System Based on Clause Trees, de Nivelle H., Schulz S., Proceedings of the 2nd International Workshop on the Implementation of Logics (Havana, Cuba), 1-12, Max-Planck-Institut für Informatik, Research Report MPI-I-2001-2-006.

He L. (2001), UNSEARCHMO: Eliminating Redundant Search Space on Backtracking for Forward Chaining Theorem Proving, Nebel B., Proceedings of the 17th International Joint Conference on Artificial Intelligence (Seattle, USA), 618-623, Morgan Kaufmann.

He L. (2001), I-SATCHMO: An Improvement of SATCHMO, Journal of Automated Reasoning 27(3), 313-322.

Hodgson K., Slaney J.K. (2001), System Description: SCOTT-5, Gore R., Leitsch A., Nipkow T., Proceedings of the International Joint Conference on Automated Reasoning (Siena, Italy), 443-447, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag.

Horrocks I., Sattler U. (2001), Ontology Reasoning in the SHOQ(D) Description Logic, Nebel B., Proceedings of the 17th International Joint Conference on Artificial Intelligence (Seattle, USA), 199-204, Morgan Kaufmann.

Loechner B., Schulz S. (2001), An Evaluation of Shared Rewriting, de Nivelle H., Schulz S., Proceedings of the 2nd International Workshop on the Implementation of Logics (Havana, Cuba), 33-48, Max-Planck-Institut für Informatik, Research Report MPI-I-2001-2-006.

Newborn M. (2001), Automated Theorem Proving: Theory and Practice, Springer.

Pastre D. (2001), Muscadet 2.3 : A Knowledge-based Theorem Prover based on Natural Deduction, Gore R., Leitsch A., Nipkow T., Proceedings of the International Joint Conference on Automated Reasoning (Siena, Italy), 685-689, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag.

Pastre D. (2001), Implementation of Knowledge Bases for Natural Deduction, Nieuwenhuis R., Voronkov A., Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Havana, Cuba), 29-68, Lecture Notes in Artificial Intelligence 2250, Springer-Verlag.

Pelletier F.J., Sutcliffe G. (2001), Effective Evaluation having an Effect, Hoos H., Stützle T., Proceedings of the IJCAI'01 Workshop on Empirical Methods in Artificial Intelligence (Seattle, USA), 33-40.

Riazanov A., Voronkov A. (2001), Splitting without Backtracking, Nebel B., Proceedings of the 17th International Joint Conference on Artificial Intelligence (Seattle, USA), 611-617, Morgan Kaufmann.

Riazanov A., Voronkov A. (2001), Vampire 1.1 (System Description), Gore R., Leitsch A., Nipkow T., Proceedings of the International Joint Conference on Automated Reasoning (Siena, Italy), 376-380, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag.

Schulz S. (2001), System Abstract: E 0.61, Gore R., Leitsch A., Nipkow T., Proceedings of the International Joint Conference on Automated Reasoning (Siena, Italy), 370-375, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag.

Sekar R., Ramakrishnan I.V., Voronkov A. (2001), Term Indexing, Robinson A., Voronkov A., Handbook of Automated Reasoning, 1853-1964, Elsevier Science.

Stenz G., Letz R. (2001), DCTP - A Disconnection Calculus Theorem Prover - System Abstract, Gore R., Leitsch A., Nipkow T., Proceedings of the International Joint Conference on Automated Reasoning (Siena, Italy), 381-385, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag.

Sutcliffe G., Fuchs M., Suttner C. (2001), Progress in Automated Theorem Proving, 1997-2001, Hoos H., Stützle T., Proceedings of the IJCAI'01 Workshop on Empirical Methods in Artificial Intelligence (Seattle, USA), 53-60.

Sutcliffe G., Suttner C.B. (2001), Evaluating General Purpose Automated Theorem Proving Systems, Artificial Intelligence 131(1-2), 39-54.

Sutcliffe G. (2001), Proceedings of the IJCAR ATP System Competition (Siena, Italy).

Sutcliffe G. (2001), The Design and Implementation of a Compositional Competition-Cooperation Parallel ATP System, de Nivelle H., Schulz S., Proceedings of the 2nd International Workshop on the Implementation of Logics (Havana, Cuba), 92-102, Max-Planck-Institut für Informatik, Research Report MPI-I-2001-2-006.

Weidenbach C. (2001), Combining Superposition, Sorts and Splitting, Robinson A., Voronkov A., Handbook of Automated Reasoning, 1965-2011, Elsevier Science.

Wos L. (2001), Conquering the Meredith Single Axiom, Journal of Automated Reasoning 27(2), 175-199.

Balsiger P., Heuerding A., Schwendimann S. (2000), A Benchmark Method for the Propositional Modal Logics K, KT, S4, Journal of Automated Reasoning 24(3), 297-317.

Baumgartner P. (2000), FDPLL - A First Order Davis-Putnam-Logemann-Loveland Procedure, McAllester D., Proceedings of the 17th International Conference on Automated Deduction (Pittsburg, USA), 200-219, Lecture Notes in Artificial Intelligence 1831, Springer-Verlag.

Brown M., Sutcliffe G. (2000), PTTP+GLiDeS - Semantically Guided PTTP, McAllester D., Proceedings of the 17th International Conference on Automated Deduction (Pittsburg, USA), 411-416, Lecture Notes in Artificial Intelligence 1831, Springer-Verlag.

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

Fuchs M., Sutcliffe G. (2000), Homogeneous Sets of ATP Problems, TR-ARP-09-00, Automated Reasoning Project, Australian National University (Canberra, Australia).

Fuchs M. (2000), Proofs as Schemas and Their Heuristic Use, Journal of Symbolic Logic 30, 37-61.

Fuchs M. (2000), Controlled Use of Clausal Lemmas in Connection Tableau Calculi, Journal of Symbolic Computation 29(2), 299-341.

Fuchs M. (2000), Controlled Use of Clausal Lemmas in Connection Tableau Calculi, AR-98-02, Institut für Informatik, Technische Universität München (Munich, Germany).

Hasegawa R., Fujita H., Koshimura M. (2000), Efficient Minimal Model Generation Using Branching Lemmas, McAllester D., Proceedings of the 17th International Conference on Automated Deduction (Pittsburg, USA), 184-199, Lecture Notes in Artificial Intelligence 1831, Springer-Verlag.

Meier A. (2000), System Description: TRAMP - Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level, McAllester D., Proceedings of the 17th International Conference on Automated Deduction (Pittsburg, USA), 460-464, Lecture Notes in Artificial Intelligence 1831, Springer-Verlag.

Plaisted D.A., Zhu Y. (2000), Ordered Semantic Hyper-linking, Journal of Automated Reasoning 25(3), 167-217.

Spencer B., Horton J.D. (2000), Support Ordered Resolution, McAllester D., Proceedings of the 17th International Conference on Automated Deduction (Pittsburg, USA), 385-400, Lecture Notes in Artificial Intelligence 1831, Springer-Verlag.

Sutcliffe G. (2000), SystemOnTPTP, McAllester D., Proceedings of the 17th International Conference on Automated Deduction (Pittsburg, USA), 406-410, Lecture Notes in Artificial Intelligence 1831, Springer-Verlag.

Sutcliffe G. (2000), Proceedings of the CADE-17 ATP System Competition (Pittsburgh, USA).

Bruynooghe M., Van de Casteele H., de Waal A., Denecker M. (1999), Detecting Unsolvable Queries for Definite Logic Programs, Journal of Functional and Logic Programming Special Issue 2.

Cook D., Hannon C. (1999), Adaptive Parallel Search for Theorem Proving, Kumar A., Russell I., Proceedings of the 12th International FLAIRS Conference (Orlando, USA), 351-355, AAAI Press.

Fuchs D., Fuchs M. (1999), Cooperation between Top-Down and Bottom-Up Theorem Provers, Journal of Artificial Intelligence Research 10, 169-198.

Fuchs M., Fuchs D. (1999), Abstraction-Based Relvancy Testing for Model Elimination, Ganzinger H., Proceedings of the 16th International Conference on Automated Deduction (Trento, Italy), 344-358, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag.

Fuchs M. (1999), Lemma Generation for Model Elimination by Combining Top-Down and Bottom-Up Inference, Dean T., Proceedings of the 16th International Joint Conference on Artificial Intelligence (Stockholm, Sweden), 4-9, Morgan Kaufmann.

Hillenbrand T., Jaeger A., Löchner B. (1999), Waldmeister - Improvements in Performance and Ease of Use, Ganzinger H., Proceedings of the 16th International Conference on Automated Deduction (Trento, Italy), 232-236, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag.

Hutter D., Bundy A. (1999), The Design of the CADE-16 Induction Theorem Prover Contest, Ganzinger H., Proceedings of the 16th International Conference on Automated Deduction (Trento, Italy), 374-377, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag.

Konrad K., Wolfram D. (1999), System Description: Kimba, A Model Generator for Many-Valued First-Order Logics, Ganzinger H., Proceedings of the 16th International Conference on Automated Deduction (Trento, Italy), 282-286, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag.

Kulik L., Klippel A. (1999), Reasoning about Cardinal Directions Using Grids as Qualitative Geographic Coordinates, Freksa C., Mark D.M., Proceedings of the 1999 International Conference on Spatial Information Theory: Cognitive and Computational Foundations of Geographic Information Science (Stade, Germany), 205-220, Lecture Notes in Computer Science 1661, Springer-Verlag.

Loveland D.W. (1999), Automated Deduction - Looking Ahead, AI Magazine 20(1), 77-98.

Riazanov A., Voronkov A. (1999), Vampire, Ganzinger H., Proceedings of the 16th International Conference on Automated Deduction (Trento, Italy), 292-296, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag.

Schulz S., Brandt F. (1999), Using Term Space Maps to Capture Search Control Knowledge in Equational Theorem Proving, Russell I., Kumar A., Proceedings of the 12th International FLAIRS Conference (Orlando, USA), 244-248, AAAI Press.

Schulz S. (1999), System Abstract: E 0.3, Ganzinger H., Proceedings of the 16th International Conference on Automated Deduction (Trento, Italy), 297-301, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag.

Stenz G., Wolf A. (1999), Strategy Selection by Genetic Programming, Kumar A., Russell I., Proceedings of the 12th International FLAIRS Conference (Orlando, USA), 346-350, AAAI Press.

Stenz G., Wolf A. (1999), E-SETHEO: Design, Configuration and Use of a Parallel Automated Theorem Prover, Foo N., Proceedings of AI'99: The 12th Australian Joint Conference on Artificial Intelligence (Sydney, Australia), 231-243, Lecture Notes in Artificial Intelligence 1747, Springer-Verlag.

Sutcliffe G., Seyfang D. (1999), Smart Selective Competition Parallelism ATP, Kumar A., Russell I., Proceedings of the 12th International FLAIRS Conference (Orlando, USA), 341-345, AAAI Press.

Sutcliffe G. (1999), Proceedings of the CADE-16 ATP System Competition (Trento, Italy).

Suttner C.B. (1999), SPS-Parallelism + SETHEO = SPTHEO, Journal of Automated Reasoning 22(4), 397-431.

Weidenbach C., Afshordel B., Brahm U., Cohrs C., Engel T., Keen E., Theobalt C., Tpoic D. (1999), System Description: SPASS Version 1.0.0, Ganzinger H., Proceedings of the 16th International Conference on Automated Deduction (Trento, Italy), 378-382, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag.

Bündgen R., Göbel M., Küchlin W., Weber A. (1998), Parallel Term Rewriting with PaReDuX, Bibel W., Schmitt P.H., Automated Deduction, A Basis for Applications, 231-259, Applied Logic Series II Systems and Implementation Techniques(9), Kluwer Academic Publishers.

Defourneaux G., Bourely C., Peltier N. (1998), Semantic Generalizations for Proving and Disproving Conjectures by Analogy, Journal of Automated Reasoning 20(1-2), 27-45.

Denzinger J., Dahn I. (1998), Cooperating Theorem Provers, Bibel W., Schmitt P.H., Automated Deduction, A Basis for Applications, 383-416, Applied Logic Series II Systems and Implementation Techniques(9), Kluwer Academic Publishers.

Denzinger J., Schulz S. (1998), Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts, Journal of Information and Computation.

Fuchs D. (1998), Requirement-Based Cooperative Theorem Proving, Dix J., del Cerro F., Furbach U., Proceedings of the 6th European Workshop on Logics in Artificial Intelligence (Dagstuhl, Germany), 139-153, Lecture Notes in Artificial Intelligence 1489, Springer-Verlag.

Fuchs D. (1998), Coupling Saturation-Based Provers by Exchanging Positive/Negative Information, Nipkow T., Proceedings of the 9th International Conference on Rewriting Techniques and Applications (Tsukuba, Japan), 317-331, Lecture Notes in Computer Science 1379, Springer-Verlag.

Fuchs M. (1998), Automatic Selection of Search-Guiding Heuristics for Theorem Proving, TR-ARP-2-1998, Automated Reasoning Project, Australian National University (Canberra, Australia).

Nonnengart A., Rock G., Weidenbach C. (1998), On Generating Small Clause Normal Forms, Kirchner C., Kirchner H., Proceedings of the 15th International Conference on Automated Deduction (Lindau, Germany), 397-411, Lecture Notes in Artificial Intelligence 1421, Springer-Verlag.

Reif W., Schellhorn G. (1998), Theorem Proving in Large Theories, Bibel W., Schmitt P.H., Automated Deduction, A Basis for Applications, 225-241, Applied Logic Series III Applications(10), Kluwer Academic Publishers.

Schulz S. (1998), Term Space Mapping for DISCOUNT, Proceedings of the CADE-15 Workshop on Using AI Methods in Deduction (Lindau, Germany).

Schumann J., Wolf A., Suttner C.B. (1998), Parallel Theorem Provers Based on SETHEO, Bibel W., Schmitt P.H., Automated Deduction, A Basis for Applications, 261-290, Applied Logic Series II Systems and Implementation Techniques(9), Kluwer Academic Publishers.

Sutcliffe G., Suttner C.B. (1998), Proceedings of the CADE-15 ATP System Competition (Lindau, Germany).

Sutcliffe G., Suttner C.B. (1998), The TPTP Problem Library: CNF Release v1.2.1, Journal of Automated Reasoning 21(2), 177-203.

Tammet T. (1998), Towards Efficient Subsumption, Kirchner C., Kirchner H., Proceedings of the 15th International Conference on Automated Deduction (Lindau, Germany), 427-440, Lecture Notes in Artificial Intelligence 1421, Springer-Verlag.

Wolf A., Letz R. (1998), Strategy Parallelism in Automated Theorem Proving, Cook D., Proceedings of the 11th International FLAIRS Conference (Sanibel Island, USA), 1-5.

Autexier S., Hutter D. (1997), Equational Proof-Planning by Dynamic Abstraction, Salzer G., Proceedings of FTP'97, International Workshop on First Order Theorem Proving (Hagenberg, Austria), 1-6, RISC-Linz Report 97-50, Johannes Kepler Universität.

Baumgartner P., Brüning S. (1997), A Disjunctive Positive Refinement of Model Elimination and Its Application to Subsumption Deletion, Journal of Automated Reasoning 19(2), 205-262.

Benzmüller C., Cheikhrouhou L., Fehrer D., Fiedler A., Huang X., Kerber M., Kohlhase M., Konrad K., Meier A., Melis E., Schaarschmidt W., Siekmann J., Sorge V. (1997), OMEGA: Towards a Mathematical Assistant, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 252-255, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.

Dahn B.I., Gehne J., Honigmann T., Wolf A. (1997), Integration of Automated And Interactive Theorem Proving, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 57-60, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.

Defourneaux G., Peltier N. (1997), Partial Matching for Analogy Discovery in Proofs and Counter-Examples, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 431-445, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.

Fischer B., Schumann J. (1997), SETHEO Goes Software Engineering: Application of ATP to Software Reuse, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 65-68, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.

Fuchs D. (1997), Inference Rights for Controlling Search in Generating Theorem Provers, Costa E., Cardoso A., Proceedings of the 9th Portuguese Conference on Artificial Intelligence (Coimbra, Portugal), 25-36, Lecture Notes in Artificial Intelligence 1323, Springer-Verlag.

Fuchs D. (1997), Cooperation in Theorem Proving by Loosely Coupled Heuristics, SR-97-03, University of Kaiserslautern (Kaiserslautern, Germany).

Geisler T., Panne S., Schütz H. (1997), Satchmo: The Compiling and Functional Variants, Journal of Automated Reasoning 18(2), 227-236.

Harrison J. (1997), First Order Logic in Practice, Salzer G., Proceedings of FTP'97: International Workshop on First Order Theorem Proving (Hagenberg, Austria), 86-90, RISC-Linz Report 97-50, Johannes Kepler Universität.

Hasegawa R., Inoue K., Ohta Y., Koshimura M. (1997), Non-horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 176-190, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.

Horton J.D., Spencer B. (1997), Clause Trees: A Tool for Understanding and Implementing Resolution in Automated Reasoning, Artificial Intelligence 92, 25-89.

Iwanuma K. (1997), Lemma Matching for a PTTP-based Top-down Theorem Prover, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 146-160, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.

Jackobi P., Wolf A. (1997), DBFW: A Simple Database Framework for the Evaluation and Maintenance of Automated Theorem Prover Data, TUM-I9747, Technische Universität München (Munich, Germany).

Letz R. (1997), LINUS: A Link Instantiation Prover with Unit Support, Journal of Automated Reasoning 18(2), 205-210.

Moser M., Ibens O., Letz R., Steinbach J., Goller C., Schumann J., Mayr K. (1997), SETHEO and E-SETHEO: The CADE-13 Systems, Journal of Automated Reasoning 18(2), 237-246.

Pelletier F.J., Sutcliffe G. (1997), An Erratum to some Errata to ATP Problems, Journal of Automated Reasoning 18(1), 135.

Reif W., Schellhorn G. (1997), Theorem Proving in Large Theories, Salzer G., Proceedings of FT97, International Workshop on First Order Theorem Proving (Hagenberg, Austria), 119-124, RISC-Linz Report 97-50, Johannes Kepler Universität.

Schumann J. (1997), SiCoTHEO - Simple Competitive Parallel Theorem Provers based on SETHEO, Geller J., Kitano H., Suttner C, Proceedings of the Workshop on Parallel Processing for Artificial Intelligence (Montreal, Canada), Machine Intelligence and Pattern Recognition 16, Elsevier Science.

Spencer B., Horton J.D. (1997), Extending the Regular Restriction of Resolution to Non-Linear Subdeductions, Kuipers B., Webber B., Proceedings of the 14th National Conference on Artificial Intelligence (Providence, USA), 478-484, AAAI Press.

Sturgill D., Segre A.M. (1997), Nagging: A Distributed, Adversarial Search-Pruning Technique Applied to First-Order Inference, Journal of Automated Reasoning 19(3), 347-376.

Sutcliffe G., Suttner C.B. (1997), The Procedures of the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), 163-169.

Suttner C.B., Sutcliffe G. (1997), The Design of the CADE-13 ATP System Competition, Journal of Automated Reasoning 18(2), 139-162.

Suttner C.B., Sutcliffe G. (1997), The TPTP Problem Library (TPTP v2.1.0), Technical Report AR-97-01, Institut für Informatik, Technische Universität München, Munich, Germany; Technical Report 97/04, Department of Computer Science, James Cook University, Townsville, Australia..

Wolf A., Fuchs M. (1997), Cooperative Parallel Automated Theorem Proving, SFB Bereicht 342/21/97, Technische Universität München (München, Germany).

Wolf A., Schumann J. (1997), ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output, McCune W.W., Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia), 61-64, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag.

Baumgartner P., Furbach U., Niemelä I. (1996), Hyper Tableaux, Alferes J., Pereira L., Orlowska E., Proceedings of JELIA'96: European Workshop on Logic in Artificial Intelligence (Evora, Portugal), 1-17, Lecture Notes in Artificial Intelligence 1126, Springer-Verlag.

Beckert B., Hähnle R., Oel P., Sulzmann M. (1996), The Tableau-based Theorem Prover 3TAP Version 4.0, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 302-307, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.

Denzinger J., Schulz S. (1996), Learning Domain Knowledge to Improve Theorem Proving, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 62-76, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.

Fuchs M. (1996), Experiments in the Automatic Selection of Problem Solving Strategies, LSA-96-09E, Universität Kaiserslautern (Kaiserslautern, Germany).

Giunchiglia F., Sebastiani R. (1996), Building Decision Procedures for Modal Logics from Propositional Decision Procedures - The Case Study of Modal K*, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 583-597, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.

Hähnle R., Kerber M., Weidenbach C. (1996), Common Syntax of the DFG-Schwerpunktprogramm Deduction, TR 10/96, Fakultät für Informatik, Universät Karlsruhe (Karlsruhe, Germany).

Linton S., Shand D. (1996), Some Group Theoretic Examples with Completion Theorem Provers, Journal of Automated Reasoning 17(2), 145-169.

Schumann J. (1996), SiCoTHEO - Simple Competitive Parallel Theorem Provers, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 240-244, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.

Sutcliffe G., Melville S. (1996), The Practice of Clausification in Automatic Theorem Proving, South African Computer Journal 18, 57-68.

Suttner C.B., Sutcliffe G. (1996), The Design of the CADE-13 ATP System Competition, McRobbie M., Slaney J.K., Proceedings of the 13th International Conference on Automated Deduction (New Brunswick, USA), 146-160, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.

Suttner C.B., Sutcliffe G. (1996), The TPTP Problem Library (TPTP v1.2.1), Technical Report AR-96-02, Institut für Informatik, Technische Universität München, Munich, Germany; Technical Report 96/09, Department of Computer Science, James Cook University, Townsville, Australia..

Zhang J., Zhang H. (1996), System Description: Generating Models by SEM, Ganzinger H., Proceedings of the 16th International Conference on Automated Deduction (Trento, Italy), 308-312, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag.

Baumgartner P., Furbach U., Stolzenburg F. (1995), Model Elimination, Logic Programming and Computing Answers, Mellish C.S., Proceedings of the 14th International Joint Conference on Artificial Intelligence, 335-340, Morgan Kaufmann.

Caferra R., Peltier N. (1995), Extending Semantic Resolution via Automated Model Building: Applications, Mellish C.S., Proceedings of the 14th International Joint Conference on Artificial Intelligence, 328-334, Morgan Kaufmann.

Horton J.D., Spencer B. (1995), Clause Trees: A Tool for Understanding and Implementing Resolution in Automated Reasoning, TR95-095, University of New Brunswick (Fredericton, Canada).

Pelletier F.J., Sutcliffe G. (1995), An Erratum for Some Errata to Automated Theorem Proving Problems, Association for Automated Reasoning Newsletter, 8-14.

Reif W. (1995), The KIV-approach to Software Verification, Broy M., Jähnichen S., KORSO: Methods, Languages, and Tools for the Construction of Correct Software - Final Report, Lecture Notes in Computer Science 1009.

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

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

Suttner C.B., Sutcliffe G. (1995), The TPTP Problem Library (TPTP v1.2.0), Technical Report AR-95-03, Institut für Informatik, Technische Universität München, Munich, Germany; Technical Report 95/6, Department of Computer Science, James Cook University, Townsville, Australia..

Suttner C.B. (1995), Parallelization of Search-based Systems by Static Partitioning with Slackness, Dissertationen zur künstlichen Intelligenz 101, Springer-Verlag.

Wallace K., Wrightson G. (1995), Regressive Merging in Model Elimination Tableau-based Theorem Provers, Bulletin of the Interest Group in Pure and Applied Logics 3(6), 921-937.

Astrachan O.L., Loveland D.W. (1994), Measuring the Performance of Automated Theorem Provers, Sutcliffe G., Suttner C.B., Proceedings of the CADE-12 Workshop 2C - Evaluation of Automated Theorem Proving Systems (Nancy, France), 37-41.

Baumgartner P., Furbach U. (1994), Model Elimination without Contrapositives and its Application to PTTP, Journal of Automated Reasoning 13(3), 339-359.

Baumgartner P. (1994), Refinements of Theory Model Elimination and a Variant without Contrapositives, Cohn A.G., Proceedings of the 11th European Conference on Artificial Intelligence, 90-94, Wiley and Sons.

Huang X., Kerber M., Kohlhase M., Nesmith D., Richts J. (1994), A Test for Evaluating the Practical Usefulness of Deduction Systems, Sutcliffe G., Suttner C.B., Proceedings of the CADE-12 Workshop 2C - Evaluation of Automated Theorem Proving Systems (Nancy, France), 33-36.

Kropf T. (1994), Benchmark-Circuits for Hardware-Verification, Kropf T., Kumar R., Proceedings of the 2nd International Conference on Theorem Provers in Circuit Design, 1-12, Springer-Verlag.

Kropf T. (1994), Benchmark-Circuits for Hardware-Verification, Draft v0.8.3, Institut für Rechnerentwerf und Fehlertoleranz, Universität Karlsruhe (Karlsruhe, Germany).

McCune W.W. (1994), Otter 3.0, Sutcliffe G., Suttner C.B., Proceedings of the CADE-12 Workshop 2C - Evaluation of Automated Theorem Proving Systems (Nancy, France), 43-48.

Suttner C.B., Sutcliffe G. (1994), The TPTP Problem Library (TPTP v1.1.1), Technical Report AR-94-03, Institut für Informatik, Technische Universität München, Munich, Germany; Technical Report 93/11, Department of Computer Science, James Cook University, Townsville, Australia..

Wallace K., Wrightson G. (1994), Regressive Merging in Model Elimination Tableau-Based Theorem Provers, Broda K., D'Agostino M., Gore R., Johnson R., Reeves S., Proceedings of the 3rd International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (London, United Kingdom), 233-246.

Suttner C., Sutcliffe G., Yemenis T. (1993), The TPTP Problem Library for 1st Order Automated Theorem Provers (TPTP v1.0.0), Technical Report FKI-184-93, Institut für Informatik, Technische Universität München, Munich, Germany; Technical Report 93/11, Department of Computer Science, James Cook University, Townsville, Australia..