Stephan Schulz
schulz@eprover.org

Bibliography

Most of my work deals with automated theorem proving, in particular techniques developed for and realised in the theorem prover E.

I am particularly interested in finding out more about good proof search 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. Another aspect of my work is the efficient implementation of reasoning mechanisms.

Publications are listed in chronological order, but the list is probably somewhat incomplete. I'm working on it.

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
  • 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).
  • The full thesis (960 Kbytes PDF).
  • 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 or 111 KBytes PDF)
  • 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 (487 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 (2 MBytes gzipped PostScript or 360 KBytes PDF)
  • Several minor errors have been fixed in this version.
  • 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
  Please see the 2013 version of the paper for an extended treatment of Feature Vector Indexing.
• 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
• M. Bozzano and R. Bruttomesso and A. Cimatti and T. Junttila and P. van Rossum and S. Schulz and R. Sebastiani: MathSAT: Tight Integration of SAT and Mathematical Decision Procedures, Journal of Automated Reasoning 35(1-3), 2005, pp. 265--293.
  • Abstract
  • The full paper (473 KBytes PDF)
  • BibTeX Entry
• Geoff Sutcliffe, Stephan Schulz, Koen Claessen and Allen Van Gelder: Using the TPTP Language for Writing Derivations and Finite Interpretations, Proceedings of the 3rd IJCAR, Seattle, 2006, pp. 67-81, LNAI 4130, © Springer Verlag.
  • Abstract
  • The full paper (169 KBytes PDF)
  • BibTeX Entry
• Alessandro Armando, Maria Paola Bonacina, Silvio Ranise and Stephan Schulz: New Results on Rewrite-Based Satisfiability Procedures, ACM Transactions on Computational Logic 10(1)
  • Abstract.
  • The full paper (453 KBytes PDF preprint).
  • BibTeX Entry.
• Geoff Sutcliffe, Stephan Schulz, Koen Claessen and Peter Baumgartner: The TPTP Typed First-order Form with Arithmetic, Proceedings of the 18th LPAR, Merida, 2012, pp. 406-419, LNAI 7180, © Springer Verlag.
  • Abstract
  • The full paper (306 KBytes PDF)
  • BibTeX Entry
• Stephan Schulz: Fingerprint Indexing for Paramodulation and Rewriting, Proceedings of the 6th IJCAR, Manchester, 2012, pp. 477-483, LNAI 7364, © Springer Verlag.
  • Abstract
  • The full paper (306 KBytes PDF)
  • BibTeX Entry
• Stephan Schulz: Simple and Efficient Clause Subsumption with Feature Vector Indexing, In Maria Paola Bonacina and Mark E. Stickel, Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, 2013, pp. 45-673, LNAI 7788, © Springer Verlag.
  • Abstract
  • The full paper (419 KBytes PDF)
  • BibTeX Entry
• Daniel Kühlwein, Stephan Schulz, and Josef Urban : E-MaLeS 1.1, Proceedings of the 24th CADE, Lake Placid, 2013 pp. 407-413, LNCS 7898 © Springer Verlag.
  • Abstract
  • The full paper (219 KBytes PDF)
  • BibTeX Entry
• Stephan Schulz: System Description: E 1.8, Proceedings of the 19th LPAR, Stellenbosch, 2013, pp. 477-483, LNCS 8312 © Springer Verlag.
  • Abstract
  • The full paper (339 KBytes PDF)
  • BibTeX Entry
• Stephan Schulz and Geoff Sutcliffe: Proof Generation for Saturating First-Order Theorem Provers. In David Delahaye and Bruno Woltzenlogel Paleo, All about Proofs, Proofs for All, volume 55 of Mathematical Logic and Foundations, pages 45–61, College Publications, 2015
  • Abstract
  • The full paper (3.5 MB PDF)
  • BibTeX Entry
• Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jiří Vyskočil: System description: ET 0.1, Proc. CADE-25, Berlin, 2015, pp. 389-398, LNCS 9195 © Springer Verlag.
  • Abstract
  • The full paper (370 KBytes PDF)
  • BibTeX Entry
• Simon Schäfer and Stephan Schulz: Breeding Theorem Proving Heuristics with Genetic Algorithms, Proceedings of the First GCAI, Tibilisi, 2015, EPiC.
  • Abstract
  • The full paper (488 KBytes PDF)
  • BibTeX Entry
• Stephan Schulz and Martin Möhrmann: Performance of clause selection heuristics for saturation-based theorem proving, Proceedings of the 8th IJCAR, Coimbra, volume 9706 of LNAI. Springer, 2016.
  • Abstract
  • The full paper (457 KBytes PDF)
  • BibTeX Entry
• Stephan Schulz, Geoff Sutcliffe, Josef Urban and Adam Pease: Detecting Inconsistencies in Large First-Order Knowledge Bases, Proceedings of the 26th CADE, Gothenburg, volume 10395 of LNAI. Springer, 2017.
  • Abstract
  • The full paper (457 KBytes PDF)
  • BibTeX Entry
• Stephan Schulz: Light-Weight Integration of SAT Solving into First-Order Reasoners -- First Experiments, Proceedings of the 4th Vampire Workshop , Gothenburg, volume 53 of EPiC Series in Computing, 2018.
  • Abstract
  • The full paper (347 KBytes PDF)
  • BibTeX Entry
• Zarathustra Goertzel, Jan Jakubův, Stephan Schulz, and Josef Urban: ProofWatch: Watchlist Guidance for Large Theories in E, Proceedings of the 9th Conference on Interactive Theorem Proving, Oxford, volume 10895 of LNCS. Springer, 2018.
  • Abstract
  • The full paper (375 KBytes PDF)
  • BibTeX Entry
• Petar Vukmirovic, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz: Extending a Brainiac Prover to Lambda-Free Higher-Order Logic, Proceedings of the 25th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-19). Volume 11427 of LNCS. Springer, 2019.
  • Abstract
  • The full paper (460 KBytes PDF)
  • BibTeX Entry
• Stephan Schulz, Simon Cruanes, Petar Vukmirovic: Faster, Higher, Stronger: E 2.3, Proceedings of the 27th Conference on Automated Deduction (CADE'19). Volume 11716 of LNAI. Springer, 2019.
  • Abstract
  • The full paper (380 KBytes PDF)
  • BibTeX Entry
• Stephan Schulz, Adam Pease: Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description), Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR'20). Volume 12167 of LNAI. Springer, 2020.
  • Abstract
  • The full paper (236 KBytes PDF)
  • BibTeX Entry
• Nahku Saidy, Hanna Siegfried, Stephan Schulz, Geoff Sutcliffe: Cutting down the TPTP language (and others), Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 , CEUR Workshop Proceedings 2752.
  • Abstract
  • The full paper (380 KBytes PDF)
  • BibTeX Entry
• Constantin Ruhdorfer, Stephan Schulz: Efficient Implementation of Large-Scale Watchlists, Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020, CEUR Workshop Proceedings 2752.
  • Abstract
  • The full paper (730 KBytes PDF)
  • BibTeX Entry
• Petar Vukmirovic, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz: Extending a Brainiac Prover to Lambda-Free Higher-Order Logic, International Journal on Software Tools for Technology Transfer, 2021, DOI 10.1007/s10009-021-00639-7
  • Abstract
  • The full paper (468 KBytes PDF)
  • BibTeX Entry
• Stephan Schulz: Empirical Properties of Term Orderings for Superposition, Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning, Haifa, Israel, 2022, CEUR Workshop Proceedings 3201.
  • Abstract
  • The full paper (1004kBytes PDF)
  • BibTeX Entry
• Petar Vukmirovic, Jasmin Christian Blanchette, Stephan Schulz: Extending a High-Performance Prover to Higher-Order Logic, Proceedings of the 29th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-23), Paris, France, Volume 13994 of LNCS. Springer, 2023.
  • Abstract
  • The full paper (511kBytes PDF)
  • BibTeX Entry
• Jan Jakubuv, Karel Chvalovsky, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olsak, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban: MizAR 60 for Mizar 50, Proceedings of the 15th Conference on Interactive Theorem Proving (ITP-23), Białystok, Poland, Volume 268 of LIPIcs. Schloss Dagstuhl, 2023.
  • Abstract
  • The full paper (860kBytes PDF)
  • BibTeX Entry
• Stephan Schulz: Lazy and Eager Patterns in High-Performance Automated Theorem Proving, Proceedings of the 7th and 8th Vampire Workshop, Rome and Nancy, volume 99 of EPiC Series in Computing, 2024.
  • Abstract
  • The full paper (347 KBytes PDF)
  • 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
• Rudnicki, P. and Sutcliffe, G. and Konev, B. and Schmidt, R. and Schulz, S. (editors): 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
• Geoff Sutcliffe, Eugenia Ternovska and Stephan Schulz (editors): Proceedings of the 8th International Workshop on the Implementation of Logics, 2010.
  • The proceedings (6.3 MBytes PDF)
  • BibTeX Entry
• Konstantin Korovin, Stephan Schulz and Eugenia Ternovska: (editors): Proceedings of the the 9th International Workshop on the Implementation of Logics, 2012
  • The EasyChair proceedings
  • BibTeX Entry
• Boris Konev, Stephan Schulz and Laurent Simon: (editors): Proceedings of the the 11th International Workshop on the Implementation of Logics, 2015
  • The EasyChair proceedings
  • BibTeX Entry
• Didier Galmiche, Stephan Schulz and Roberto Sebastiani: (editors): Proceedings of the the 9th International Joint Conference on Automated Reasoning, LNAI 10900, Springer, 2018
  • The Proceedings at Springer.
• 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)
• I have co-edited many of the the proceedings of the IJCAR workshop series on the Practical Aspects of Automated Reasoning (PAAR). Links to the publications are on the series page.
  • Proceedings of the First Workshop on Practical Aspects of Automated Reasoning, associated with the 4th IJCAR, Sydney, Australia, 2008 (with Boris Konev and Renate Schmidt)
  • Proceedings of the Second Workshop on Practical Aspects of Automated Reasoning, associated with FLoC 2010 and the 5th IJCAR, Edinburgh, UK, 2010 (with Boris Konev and Renate Schmidt)
  • Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, associated with the 6th IJCAR, Manchester, UK, 2012 (with Pascal Fontaine and Renate Schmidt)
  • Proceedings of the Fourth Workshop on Practical Aspects of Automated Reasoning, associated with the 7th IJCAR as part of the Vienna Summer of Logic, Vienna, Austria, 2014 (with Leonardo de Moura and Boris Konev)
  • Proceedings of the Fifth Workshop on Practical Aspects of Automated Reasoning, associated with the 7th IJCAR, Coimbra, Portugal, 2016 (with Pascal Fontaine and Josef Urban)

Presentations

I only make presentations availabe for major talks, and only if there is no associated paper. If you want any of my other presentations, feel free to ask (but I suggest you read the paper instead). In general, my newer slide sets are designed to complement the talk, not as stand-alone documents.

Older presentations are prepared using pdflatex and some modified style files originally borrowed from Matt Welsh, newer ones use a Frankenstein mixture of LaTeX Beamer and Apple's Keynote.

• 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)
• Schulz, S: Implementation of First-Order Theorem Provers. Lecture, Summer School 2009: Verification Technology, Systems & Applications, Nancy, France, 2009
  • Abstract
  • Presentation (980 KBytes PDF)
• Schulz, S: Fingerprint Indexing for Paramodulation. Deduktionstreffen 2010, Karlsruhe, Germany
  • Presentation (750 KBytes PDF)
  • Poster (690 KBytes PDF)
• Schulz, S: Where, What, and How? Lessons from the Evolution of E. Invited talk at the 19th LPAR, 2013, Stellenbosch, South Africa
  • Abstract
  • Presentation (4 MBytes PDF)
• Schulz, S: Implementation of Saturating Theorem Provers. Lecture, International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning, Manchester, UK, 2018
  • Abstract
  • Presentation (3 MBytes PDF)

Stephan Schulz, schulz@eprover.org