Bibliography

I am particularly interested in finding out more about good proof heuristics, and I work towards the automatic acquistion of search control knowledge for deductive systems. Thus, much of my research has to do with (deductive) reasoning and with (inductive) machine learning.

Publications are listed in chronological order (I hope).

Authored Publications

• Schulz, S.: Analyse und Transformation von Gleichheitsbeweisen, Projektarbeit, Fachbereich Informatik, Universität Kaiserslautern, 1993
  • An abstract is available in English language.
  • The full report (247 Kbytes gzipped PostScript) is only available in German. Most of the topics covered here are revisited in the SEKI-Report below, although there is a slightly different focus.
  • BibTeX Entry
• Denzinger,J. ; Schulz, S.: Analysis and Representation of Equational Proofs Generated by a Distributed Completion Based Proof System, SEKI-Report SR-94-05, Universiät Kaiserslautern, 1994
  • Abstract
  • Download full report (253 Kbytes gzipped PostScript)
  • BibTeX Entry
• Denzinger,J. ; Schulz, S.: Recording, Analyzing and Presenting Distributed Deduction Processes, Proc. PASCO'94, Linz, 1994, pp. 114-123.
  • Abstract.
  • The full paper (100 Kbytes gzipped PostScript format).
  • BibTeX Entry
• Schulz, S.: Explanation Based Learning for Distributed Equational Deduction, Diplomarbeit, Fachbereich Informatik, Universität Kaiserslautern, 1995
  • Currently no abstract is available online.
  • The full thesis (261 Kbytes gzipped PostScript) and the Errata
  • BibTeX Entry
• Denzinger,J. ; Schulz, S.: Recording and Analysing Knowledge-Based Distributed Deduction Processes (preliminary version). The final version has appeared in the Journal of Symbolic Computation 21:523-541, 1996. This is an expanded and revised version of the previous work on the list.
  • Abstract.
  • The full paper (67 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schramm, M.; Schulz, S.: Combining Propositional Logic with Maximum Entropy Reasoning on Probability Models, Proc. of the ECAI'96 Workshop on Integrating Nonmonotonicity into Automated Reasoning Systems, Budapest, 1996. This paper is the odd one out. It is the result of work done for the European EPRIT Project 9119 MIX. The system described in the paper has mutated into the full blown probabilistic expert system PIT, with which I am still loosely associated.
  • Abstract.
  • The full paper (48 Kbytes gzipped PostScript).
  • BibTeX Entry
• Denzinger,J. ; Schulz, S.: Learning Domain Knowledge to Improve Theorem Proving, Proc. CADE-13, New Brunswick, NJ, USA 1996, pp. 62-76.
  • Abstract.
  • The full paper (62 Kbytes gzipped PostScript).
  • BibTeX Entry
• Denzinger,J. ; Kronburg, M; Schulz, S.: DISCOUNT: A Distributed and Learning Prover (preliminary version). The final version has appeared in the Journal of Automated Reasoning 18 (Special Edition on the CADE-13 ATP System Competition):189-198 in 1997. The paper describes the two versions of DISCOUNT participating in the CASC-13 theorem proving competition.
  • Abstract.
  • The full paper (66 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.; Küchler, A.; Goller, C.: Some Experiments on the Applicability of Folding Architecture Networks to Guide Theorem Proving. Proc. 10th International FLAIRS Conference, Daytona Beach, FL, USA, 1997, pp. 377-381.
  • Abstract.
  • Full paper (71 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.: Term Space Mapping for DISCOUNT. Proceedings of the CADE-15 Workshop on Using AI methods in Deduction, Lindau, Germany, 1998
  • Abstract.
  • Full paper (63 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.; Brandt, F.: Using Term Space Maps to Capture Search Control Knowledge in Equational Theorem Proving. Proc. 12th International FLAIRS Conference, Orlando, FL, USA, 1999, pp. 244-248.
  • Abstract.
  • Full paper (550 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.: System Abstract: E 0.3, Proc. CADE-16, Trento, Italy, 1999, pp. 297-301, LNAI 1632, © Springer Verlag.
  • Abstract.
  • The full paper (43 Kbytes gzipped PostScript).
  • BibTeX Entry
• Denzinger, J.; Fuchs, M.; Goller, C.; Schulz, S.: Learning from Previous Proof Experience: A Survey. AR-Report AR99-4, Fakultät für Informatik, Technische Universität München, 1999. This survey describes the current state of the art for learning theorem provers.
  • Abstract.
  • Full paper (187 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.: Learning Search Control Knowledge for Equational Deduction. Ph.D. Thesis, accepted by the Fakultät für Informatik of the Technische Universität München in February 2000. The printed version has appeared as number 230 in the DISKI series of infix. The publisher has generously agreed to let me offer an electronic version of the thesis on the web.
  • Abstract.
  • The full thesis (472 Kbytes gzipped PostScript).
  • BibTeX Entry
• Denzinger, J; Schulz, S.: Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts. Journal of Information and Computation 162:59-79, 2000. This is an expanded and revised version of Learning Domain Knowledge to Improve Theorem Proving above.
  • Abstract.
  • Full paper (63 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.: Information-Based Selection of Abstraction Levels. Proc. 14th International FLAIRS Conference, Key West, FL, USA, 2001, pp. 402--406.
  • Abstract.
  • Full paper (472 Kbytes gzipped PostScript).
  • BibTeX Entry
• Draeger, J.; Schulz, S.: Improving the Performance of Automated Theorem Provers by Redundancy-free Lemmatization. Proc. 14th International FLAIRS Conference, Key West, FL, USA, 2001, pp. 345--349.
  • Abstract.
  • Full paper (472 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.: System Abstract: E 0.61, Proc. 1st IJCAR, Siena, Italy, 2001, pp. 370-375, LNAI 2083, © Springer Verlag.
  • Abstract.
  • The full paper (44 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.: Learning Search Control Knowledge for Equational Theorem Proving, Proc. of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001), Vienna, Austria, 2001, pp.320-334, pp. 370-375, LNAI 2174, © Springer Verlag.
  • Abstract.
  • The full paper (74 Kbytes gzipped PostScript).
  • BibTeX Entry
• Löchner, B.;Schulz, S.: An Evaluation of Shared Rewriting, Proc. of the 2nd International Workshop on the Implementation of Logics, Havana, Cuba, 2001, pp.33-48. See below.
  • Abstract.
  • The full paper (106 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.: A Comparison of Different Techniques for Grounding Near-Propositional CNF Formulae. Proc. 15th International FLAIRS Conference, Pensacola, FL, USA, 2001, pp. 72--76. This paper received the best paper award at the 2002 FLAIRS conference. There is a separate page with the experimental data and the eground version used.
  • Abstract.
  • Full paper (36 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.; Sutcliffe, G: System Description: GrAnDe 1.0, Proc. CADE-18, Copenhagen, Denmark, 2002, pp. 280-284, LNAI 2392, © Springer Verlag.
  • My co-author considered this to be too short for an abstract ;-)
  • The full paper (45 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.: E -- A Brainiac Theorem Prover. Journal of AI communications 15(2/3):111-126, 2002.
  • Abstract.
  • Full paper (194 Kbytes gzipped PostScript or 251 KBytes PDF).
  • A minor typo in the subsumption rule has been fixed.
  • BibTeX Entry
• Sutcliffe, G.; Zimmer, J; Schulz, S.: Communication Formalisms for Automated Theorem Proving Tools. Proc. of the IJCAI-18 Workshop on Agents and Automated Reasoning, Acapulco, Mexico, 2003, pp. 53-58.
  • Abstract.
  • Full paper (59 Kbytes gzipped PostScript).
  • BibTeX Entry
  See the next entry for an updated and extended version.
• Sutcliffe, G.; Zimmer, J; Schulz, S.: TSTP Data-Exchange Formats for Automated Theorem Proving Tools. In V. Sorge and W. Zhang (eds.): Distributed and Multi-Agent Reasoning. IOS Press series on Frontiers in Artificial Intelligence and Applications, 2004.
  • Abstract.
  • Full paper (73 KBytes gzipped PostScript or 116 KBytes PDF)
  • BibTeX Entry
  This is work in progress, and there have been significant changes to the syntax and ontology. I encourage you to visit the TPTP website and get the latest versions.
• Schulz, S.: System Abstract: E 0.81, Proc. 2nd IJCAR, Cork, Ireland, 2004, pp. 223-228, LNAI 3097, © Springer Verlag.
  • Abstract.
  • The full paper (104 Kbytes gzipped PostScript).
  • BibTeX Entry
• Schulz, S.: Simple and Efficient Clause Subsumption with Feature Vector Indexing, Proc. of the IJCAR-2004 Workshop on Empirically Successful First-Order Theorem Proving, Cork, Ireland.
  • Abstract.
  • The full paper (225 Kbytes gzipped PostScript or 1004 KBytes PDF).
  • BibTeX Entry.
  • Detailed experimental data.
• Schulz, S.; Bonacina, M.P.: On Handling Distinct Objects in the Superposition Calculus, Proc. of the 5th International Workshop on the Implementation of Logics, Montevideo, Uruguay
  • Abstract.
  • The full paper (169 KBytes gzipped PostScript).
  • BibTeX Entry.

Edited Proceedings

• Hans de Nivelle; Stephan Schulz (editors): Proceedings of the Second International Workshop on the Implementation of Logics. MPI-Preprint MPI-I-2001-2-006, Max-Planck-Instituts für Informatik Saarbrücken, 2001.
  • Abstract
  • The full report (371 Kbytes gzipped PostScript)
  • BibTeX Entry
• Boris Konev and Stephan Schulz (editors): Proceedings of the Fifth International Workshop on the Implementation of Logics, Technical Report of the University of Liverpool, 2005.
  • BibTeX Entry
• Boris Konev, Renate Schmidt and Stephan Schulz: Proceedings of the IJCAR'08 Workshop on Practical Aspects of Automated Reasoning, 2008
  • The proceedings are published as Volume 273 of CEUR Workshop Proceedings.
  • BibTeX Entry
• Rudnicki, P. and Sutcliffe, G. and Konev, B. and Schmidt, R. and Schulz, S.: Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics, 2008
  • Abstract
  • The full report (2.3 MBytes PDF)
  • BibTeX Entry
• I have co-edited most of the proceedings of the Empirically Successful Topics in Automated Reasoning series of workshops. Links to the publications are on the series page.
  • Proceedings of the 2004 Workshop on Empirically Successful First Order Reasoning (with Geoff Sutcliffe and Tanel Tammed)
  • Proceedings of the 2005 Workshop on Empirically Successful Classical Automated Reasoning (with Geoff Sutcliffe and Bernd Fischer)
  • Proceedings of the 2006 Workshop on Empirically Successful Computerized Reasoning (with Geoff Sutcliffe and Renate Schmidt)
  • Proceedings of the 2007 Workshop on Empirically Successful Automated Reasoning in Large Theories (with Geoff Sutcliffe and Josef Urban)
  • Proceedings of the 2008 Workshop on Empirically Successful Automated Reasoning for Mathematics (with Geoff Sutcliffe and Simon Colton)

Presentations

• Schulz, S: How and Why E Works -- or -- Hand-Optimized Z80 Assembly Code. Presentation at the invited Reunion Workshop on the Implementation of Logic, Reunion Island, 2000.
  • Presentation (108 KBytes PDF). I've re-typeset this presentation in PDF, so there may be minor changes compared to the original talk.
• Schulz, S: Simplicity, Measuring, and Good Engineering - One Way to Build a World Class Automated Deduction System. Invited talk at the 4th International Workshop on the Implementation of Logics, Almaty, Kazakhstan, 2003
  • Abstract (64 KBytes PDF)
  • Presentation (140 KBytes PDF)