---
title: "Faster, Higher, Stronger: E 2.3 — paper by Schulz et al. (2019)"
description: "This system description reports on E 2.3, a long-developed automated prover for equational… 31 references, cited by 11 papers here."
authors: ["Stephan Schulz", "Simon Cruanes", "Petar Vukmirović"]
year: 2019
venue: "CADE-27 (LNCS 11716)"
source: "https://hal.inria.fr/hal-02296188"
licence: "HAL — author's copy — read only"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/schulz-2019-faster-higher-stronger-e-2/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/schulz-2019-faster-higher-stronger-e-2/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2019](https://md.research.elamur.ai/free/en/papers/2019/page/5/) / Faster, Higher, Stronger: E 2.3

# Faster, Higher, Stronger: E 2.3

**Authors:** Stephan Schulz, Simon Cruanes and Petar Vukmirović · **Year:** 2019 · **Venue:** [CADE-27 (LNCS 11,716)](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/) ([Lecture notes in computer science 2019](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/2019/)) · **Publisher:** [Springer Science+Business Media](https://md.research.elamur.ai/free/en/publishers/springer-science-business-media/) · **Licence:** HAL — author's copy — read only

**Links:** [Publisher's page](https://doi.org/10.1007/978-3-030-29436-6_29) · [PDF](https://inria.hal.science/hal-02296188/document) · [OpenAlex](https://openalex.org/W2969992190)

**Citations:** 100 citations (OpenAlex, 2026-10-14) · [11](https://md.research.elamur.ai/free/en/papers/schulz-2019-faster-higher-stronger-e-2/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
This system description reports on E 2.3, a long-developed automated prover for equational first-order logic. It focuses on changes since E 1.8, which was last formally described in 2013. The authors outline the processing chain: parsing, optional SInE-style axiom selection, clausification, clause preprocessing, strategy choice, and a saturation core. That core runs a superposition calculus inside a DISCOUNT-style given-clause loop. The C implementation is built around a garbage-collected bank of perfectly shared terms. New capabilities include:
- many-sorted (typed) first-order logic,
- optional handling of λ-free higher-order logic (LFHOL),
- occasional grounding of the proof state, checked by the PicoSAT solver,
- proof objects that are always kept internally,
- lazy orphan removal,
- automatic recognition of the input format and stricter TPTP checks.

On the CNF and FOF part of TPTP, E 2.3 solves slightly more problems than E 1.8, both in its single-strategy auto mode and with its strategy scheduler. The paper serves as an up-to-date reference for a widely used free (GPL) prover and sets out its development plans.

## Key points
- **Evaluation setup:** 16,094 CNF/FOF problems from TPTP release 7.2.0, run on the StarExec cluster with a 300-second CPU limit per problem and memory capped at 2 GB.
- **Results:** the strategy scheduler reached 11,084 successes (10,050 proofs plus 1034 counter-saturations), compared with 10,948 for E 1.8. The auto mode reached 10,660, compared with 10,589.
- **Typed logic:** E reads the TFF0 sub-grammar of TPTP TFF. Sort compatibility is checked during unification and index retrieval, at negligible performance cost. Types are perfectly shared and were generalized to support LFHOL.
- **Usability changes:**
  - Since E 1.9.1, the prover automatically detects LOP, TPTP-2 and TPTP-3 input.
  - FOF, TFF and TCF formulas must now be fully quantified.
  - A ContradictoryAxioms status flags proofs that come from inconsistent axiom sets.
- **Future work:** full TFX/FOOL support, basic interpreted arithmetic, a more adaptive variant of feature vector indexing, and regenerated auto modes. Sources are available at eprover.org and on GitHub.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Vrije Universiteit Amsterdam](https://md.research.elamur.ai/free/en/universities/vrije-universiteit-amsterdam/) — University, Amsterdam, Netherlands · 45 works · 3,544 citations

Also on the byline: [Baden-Wuerttemberg Cooperative State University](https://ror.org/02xdzy536).

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

## Cite

Cite as: Stephan Schulz, Simon Cruanes and Petar Vukmirović. 2019. Faster, Higher, Stronger: E 2.3. CADE-27 (LNCS 11,716).

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{schulz2019faster,
  title = {{Faster, Higher, Stronger: E 2.3}},
  author = {Stephan Schulz, Simon Cruanes and Petar Vukmirović},
  booktitle = {CADE-27 (LNCS 11716)},
  year = {2019},
  doi = {10.1007/978-3-030-29436-6\_29},
  url = {https://doi.org/10.1007/978-3-030-29436-6_29}
}
```

- [← previous Simpler and Faster Learning of Adaptive Policies for Simultaneous Translation](https://md.research.elamur.ai/free/en/papers/zheng-2019-simpler-faster-learning-adaptive-policies/)
- [next → Low-Resource Corpus Filtering Using Multilingual Sentence Embeddings](https://md.research.elamur.ai/free/en/papers/chaudhary-2019-low-resource-corpus-filtering-multilingual/)
- [↑ back to papers of 2019](https://md.research.elamur.ai/free/en/papers/2019/page/5/)

## References

31 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Bachmair, L., Ganzinger, H.: Rewrite-Based Equational Theorem Proving with Selection and Simplification. Journal of Logic and Computation 3(4), 217–247 (1994) [find](https://scholar.google.com/scholar?q=Bachmair%2C+L%2E%2C+Ganzinger%2C+H%2E%3A+Rewrite%2DBased+Equational+Theorem+Proving+with+Selection+and+Simplification%2E+Journal+of+Logic+and+Computation+3%284%29%2C+217%E2%80%93247+%281994%29)
2. Barrett, C., Stump, A., Tinelli, C.: The SMT-lib standard: Version 2.0. In: Proc. of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) (2010), [http://homepage.cs.uiowa.edu/~tinelli/papers/BarST-SMT-10.pdf](http://homepage.cs.uiowa.edu/~tinelli/papers/BarST-SMT-10.pdf) [↗](http://homepage.cs.uiowa.edu/~tinelli/papers/BarST-SMT-10.pdf)
3. Biere, A.: PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation 4, 75–97 (2008) [find](https://scholar.google.com/scholar?q=Biere%2C+A%2E%3A+PicoSAT+essentials%2E+Journal+on+Satisfiability%2C+Boolean+Modeling+and+Computation+4%2C+75%E2%80%9397+%282008%29)
4. Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: [Hammering towards QED](https://md.research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/). J. Formal. Reasoning 9(1), 101–148 (2016). https://doi.org/10.6092/issn.1972-5787/4593 [↗](https://doi.org/10.6092/issn.1972-5787/4593)
5. Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd Your Herd of Provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages. pp. 53–64. Wroc law, Poland (August 2011), [http://proval.lri.fr/publications/boogie11final.pdf](http://proval.lri.fr/publications/boogie11final.pdf) [↗](http://proval.lri.fr/publications/boogie11final.pdf)
6. Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT: A Distributed and Learning Equational Prover. Journal of Automated Reasoning 18(2), 189–198 (1997), special Issue on the CADE 13 ATP System Competition [find](https://scholar.google.com/scholar?q=Denzinger%2C+J%2E%2C+Kronenburg%2C+M%2E%2C+Schulz%2C+S%2E%3A+DISCOUNT%3A+A+Distributed+and+Learning+Equational+Prover%2E+Journal+of+Automated+Reasoning+18%282%29%2C+189%E2%80%93198+%281997%29%2C+special+Issue+on+the+CADE+13+ATP+System+Competi)
7. Goertzel, Z., Jakubův, J., Schulz, S., Urban, J.: ProofWatch: Watchlist guidance for large theories in E. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving: 9th International Conference, Oxford, UK. pp. 270–288. Springer (2018) [find](https://scholar.google.com/scholar?q=Goertzel%2C+Z%2E%2C+Jakubu%CC%8Av%2C+J%2E%2C+Schulz%2C+S%2E%2C+Urban%2C+J%2E%3A+ProofWatch%3A+Watchlist+guidance+for+large+theories+in+E%2E+In%3A+Avigad%2C+J%2E%2C+Mahboubi%2C+A%2E+%28eds%2E%29+Interactive+Theorem+Proving%3A+9th+International+Conference)
8. Hoder, K., Voronkov, A.: Sine Qua Non for Large Theory Reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) Proc. of the 23rd CADE, Wroclav. LNAI, vol. 6803, pp. 299–314. Springer (2011) [find](https://scholar.google.com/scholar?q=Hoder%2C+K%2E%2C+Voronkov%2C+A%2E%3A+Sine+Qua+Non+for+Large+Theory+Reasoning%2E+In%3A+Bj%C3%B8rner%2C+N%2E%2C+Sofronie%2DStokkermans%2C+V%2E+%28eds%2E%29+Proc%2E+of+the+23rd+CADE%2C+Wroclav%2E+LNAI%2C+vol%2E+6803%2C+pp%2E+299%E2%80%93314%2E+Springer+%282011%29)
9. Korovin, K.: Inst-Gen - A Modular Approach to Instantiation-Based Automated Reasoning. In: Programming Logics - Essays in Memory of Harald Ganzinger, LNCS, vol. 7797, pp. 239–270. Springer (2013) [find](https://scholar.google.com/scholar?q=Korovin%2C+K%2E%3A+Inst%2DGen+%2D+A+Modular+Approach+to+Instantiation%2DBased+Automated+Reasoning%2E+In%3A+Programming+Logics+%2D+Essays+in+Memory+of+Harald+Ganzinger%2C+LNCS%2C+vol%2E+7797%2C+pp%2E+239%E2%80%93270%2E+Springer+%282013%29)
10. Kotelnikov, E., Kovács, L., Reger, G., Voronkov, A.: The Vampire and the FOOL. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, USA. pp. 37–48. ACM (2016) [find](https://scholar.google.com/scholar?q=Kotelnikov%2C+E%2E%2C+Kova%CC%81cs%2C+L%2E%2C+Reger%2C+G%2E%2C+Voronkov%2C+A%2E%3A+The+Vampire+and+the+FOOL%2E+In%3A+Avigad%2C+J%2E%2C+Chlipala%2C+A%2E+%28eds%2E%29+Proceedings+of+the+5th+ACM+SIGPLAN+Conference+on+Certified+Programs+and+Proofs%2C+Sain)
11. Löchner, B., Schulz, S.: An Evaluation of Shared Rewriting. In: de Nivelle, H., Schulz, S. (eds.) Proc. of the 2nd International Workshop on the Implementation of Logics. pp. 33–48. MPI Preprint, Max-Planck-Institut für Informatik, Saarbrücken (2001) [find](https://scholar.google.com/scholar?q=Lo%CC%88chner%2C+B%2E%2C+Schulz%2C+S%2E%3A+An+Evaluation+of+Shared+Rewriting%2E+In%3A+de+Nivelle%2C+H%2E%2C+Schulz%2C+S%2E+%28eds%2E%29+Proc%2E+of+the+2nd+International+Workshop+on+the+Implementation+of+Logics%2E+pp%2E+33%E2%80%9348%2E+MPI+Preprint%2C+Max)
12. McCune, W.: Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. Journal of Automated Reasoning 9(2), 147–167 (1992) [find](https://scholar.google.com/scholar?q=McCune%2C+W%2E%3A+Experiments+with+Discrimination%2DTree+Indexing+and+Path+Indexing+for+Term+Retrieval%2E+Journal+of+Automated+Reasoning+9%282%29%2C+147%E2%80%93167+%281992%29)
13. Nonnengart, A., Weidenbach, C.: Computing Small Clause Normal Forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chap. 5, pp. 335–367. Elsevier Science and MIT Press (2001) [find](https://scholar.google.com/scholar?q=Nonnengart%2C+A%2E%2C+Weidenbach%2C+C%2E%3A+Computing+Small+Clause+Normal+Forms%2E+In%3A+Robinson%2C+A%2E%2C+Voronkov%2C+A%2E+%28eds%2E%29+Handbook+of+Automated+Reasoning%2C+vol%2E+I%2C+chap%2E+5%2C+pp%2E+335%E2%80%93367%2E+Elsevier+Science+and+MIT+Press)
14. Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A.P., Middeldorp, A. (eds.) Proc. of the 25th CADE, Berlin, Germany. LNAI, vol. 9195, pp. 399–415. Springer (2015) [find](https://scholar.google.com/scholar?q=Reger%2C+G%2E%2C+Suda%2C+M%2E%2C+Voronkov%2C+A%2E%3A+Playing+with+AVATAR%2E+In%3A+Felty%2C+A%2EP%2E%2C+Middeldorp%2C+A%2E+%28eds%2E%29+Proc%2E+of+the+25th+CADE%2C+Berlin%2C+Germany%2E+LNAI%2C+vol%2E+9195%2C+pp%2E+399%E2%80%93415%2E+Springer+%282015%29)
15. Schulz, S.: E – A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002) [find](https://scholar.google.com/scholar?q=Schulz%2C+S%2E%3A+E+%E2%80%93+A+Brainiac+Theorem+Prover%2E+Journal+of+AI+Communications+15%282%2F3%29%2C+111%E2%80%93126+%282002%29)
16. Schulz, S.: Fingerprint Indexing for Paramodulation and Rewriting. In: Gramlich, B., Sattler, U., Miller, D. (eds.) Proc. of the 6th IJCAR, Manchester. LNAI, vol. 7364, pp. 477–483. Springer (2012) [find](https://scholar.google.com/scholar?q=Schulz%2C+S%2E%3A+Fingerprint+Indexing+for+Paramodulation+and+Rewriting%2E+In%3A+Gramlich%2C+B%2E%2C+Sattler%2C+U%2E%2C+Miller%2C+D%2E+%28eds%2E%29+Proc%2E+of+the+6th+IJCAR%2C+Manchester%2E+LNAI%2C+vol%2E+7364%2C+pp%2E+477%E2%80%93483%2E+Springer+%282012%29)
17. Schulz, S.: Simple and Efficient Clause Subsumption with Feature Vector Indexing. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, LNAI, vol. 7788, pp. 45–67. Springer (2013) [find](https://scholar.google.com/scholar?q=Schulz%2C+S%2E%3A+Simple+and+Efficient+Clause+Subsumption+with+Feature+Vector+Indexing%2E+In%3A+Bonacina%2C+M%2EP%2E%2C+Stickel%2C+M%2EE%2E+%28eds%2E%29+Automated+Reasoning+and+Mathematics%3A+Essays+in+Memory+of+William+W%2E+McCune%2C+L)
18. Schulz, S.: System Description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) Proc. of the 19th LPAR, Stellenbosch. LNCS, vol. 8312, pp. 735–743. Springer (2013) [find](https://scholar.google.com/scholar?q=Schulz%2C+S%2E%3A+System+Description%3A+E+1%2E8%2E+In%3A+McMillan%2C+K%2E%2C+Middeldorp%2C+A%2E%2C+Voronkov%2C+A%2E+%28eds%2E%29+Proc%2E+of+the+19th+LPAR%2C+Stellenbosch%2E+LNCS%2C+vol%2E+8312%2C+pp%2E+735%E2%80%93743%2E+Springer+%282013%29)
19. Schulz, S.: E 2.0 User Manual. EasyChair preprint no. 8 (2018). https://doi.org/10.29007/m4jw — [doi:10.29007/m4jw](https://doi.org/10.29007/m4jw) [↗](https://doi.org/10.29007/m4jw)
20. Schulz, S.: Light-weight integration of SAT solving into first-order reasoners – first experiments. In: Kovács, L., Voronkov, A. (eds.) Vampire 2017. Proceedings of the 4th Vampire Workshop. EPiC Series in Computing, vol. 53, pp. 9– 19. EasyChair (2018). https://doi.org/10.29007/89kc, https://easyc… — [doi:10.29007/89kc](https://doi.org/10.29007/89kc) [↗](https://doi.org/10.29007/89kc)
21. Schulz, S., Möhrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Olivetti, N., Tiwari, A. (eds.) Proc. of the 8th IJCAR, Coimbra. LNAI, vol. 9706, pp. 330–345. Springer (2016) [find](https://scholar.google.com/scholar?q=Schulz%2C+S%2E%2C+Mo%CC%88hrmann%2C+M%2E%3A+Performance+of+clause+selection+heuristics+for+saturation%2Dbased+theorem+proving%2E+In%3A+Olivetti%2C+N%2E%2C+Tiwari%2C+A%2E+%28eds%2E%29+Proc%2E+of+the+8th+IJCAR%2C+Coimbra%2E+LNAI%2C+vol%2E+9706%2C+pp%2E+33)
22. Schulz, S., Sutcliffe, G.: Proof generation for saturating first-order theorem provers. In: Delahaye, D., Woltzenlogel Paleo, B. (eds.) All about Proofs, Proofs for All, Mathematical Logic and Foundations, vol. 55, pp. 45–61. College Publications, London, UK (January 2015) [find](https://scholar.google.com/scholar?q=Schulz%2C+S%2E%2C+Sutcliffe%2C+G%2E%3A+Proof+generation+for+saturating+first%2Dorder+theorem+provers%2E+In%3A+Delahaye%2C+D%2E%2C+Woltzenlogel+Paleo%2C+B%2E+%28eds%2E%29+All+about+Proofs%2C+Proofs+for+All%2C+Mathematical+Logic+and+Foundat)
23. Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A Cross-Community Infrastructure for Logic Solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proc. of the 7th IJCAR, Vienna. LNCS, vol. 8562, pp. 367–373. Springer (2014) [find](https://scholar.google.com/scholar?q=Stump%2C+A%2E%2C+Sutcliffe%2C+G%2E%2C+Tinelli%2C+C%2E%3A+StarExec%3A+A+Cross%2DCommunity+Infrastructure+for+Logic+Solving%2E+In%3A+Demri%2C+S%2E%2C+Kapur%2C+D%2E%2C+Weidenbach%2C+C%2E+%28eds%2E%29+Proc%2E+of+the+7th+IJCAR%2C+Vienna%2E+LNCS%2C+vol%2E+8562%2C+pp)
24. Sutcliffe, G.: The 8th IJCAR automated theorem proving system competition– CASC-J8. AI Communications 29(5), 607–619 (2016) [find](https://scholar.google.com/scholar?q=Sutcliffe%2C+G%2E%3A+The+8th+IJCAR+automated+theorem+proving+system+competition%E2%80%93+CASC%2DJ8%2E+AI+Communications+29%285%29%2C+607%E2%80%93619+%282016%29)
25. Sutcliffe, G.: The TPTP problem library and associated infrastructure - from CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning 59(4), 483–502 (2017) [find](https://scholar.google.com/scholar?q=Sutcliffe%2C+G%2E%3A+The+TPTP+problem+library+and+associated+infrastructure+%2D+from+CNF+to+TH0%2C+TPTP+v6%2E4%2E0%2E+Journal+of+Automated+Reasoning+59%284%29%2C+483%E2%80%93502+%282017%29)
26. Sutcliffe, G., Kotelnikov, E.: TFX: The TPTP extended typed first-order form. In: Konev, B., Urban, J., Rümmer, P. (eds.) Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR), Oxford, UK. pp. 72–87. No. 2162 in CEUR Workshop Proceedings (2018), [http://ceur-ws.org/Vol-2…](http://ceur-ws.org/Vol-2…) [↗](http://ceur-ws.org/Vol-2…)
27. Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP Typed First-order Form with Arithmetic. In: Bjørner, N., Voronkov, A. (eds.) Proc. of the 18th LPAR, Merida. LNAI, vol. 7180, pp. 406–419. Springer (2012) [find](https://scholar.google.com/scholar?q=Sutcliffe%2C+G%2E%2C+Schulz%2C+S%2E%2C+Claessen%2C+K%2E%2C+Baumgartner%2C+P%2E%3A+The+TPTP+Typed+First%2Dorder+Form+with+Arithmetic%2E+In%3A+Bj%C3%B8rner%2C+N%2E%2C+Voronkov%2C+A%2E+%28eds%2E%29+Proc%2E+of+the+18th+LPAR%2C+Merida%2E+LNAI%2C+vol%2E+7180%2C+pp%2E+406)
28. Sutcliffe, G., Schulz, S., Claessen, K., Gelder, A.V.: Using the TPTP Language for Writing Derivations and Finite Interpretations . In: Fuhrbach, U., Shankar, N. (eds.) Proc. of the 3rd IJCAR, Seattle. LNAI, vol. 4130, pp. 67–81. Springer (2006) [find](https://scholar.google.com/scholar?q=Sutcliffe%2C+G%2E%2C+Schulz%2C+S%2E%2C+Claessen%2C+K%2E%2C+Gelder%2C+A%2EV%2E%3A+Using+the+TPTP+Language+for+Writing+Derivations+and+Finite+Interpretations+%2E+In%3A+Fuhrbach%2C+U%2E%2C+Shankar%2C+N%2E+%28eds%2E%29+Proc%2E+of+the+3rd+IJCAR%2C+Seattle)
29. Sutcliffe, G., Stickel, M., Schulz, S., Urban, J.: Answer Extraction for TPTP. [http://www.cs.miami.edu/~tptp/TPTP/Proposals/AnswerExtraction](http://www.cs.miami.edu/~tptp/TPTP/Proposals/AnswerExtraction). html, (acccessed 2013-07-08) [↗](http://www.cs.miami.edu/~tptp/TPTP/Proposals/AnswerExtraction)
30. Vukmirović, P., Blanchette, J.C., Cruanes, S., Schulz, S.: Extending a brainiac prover to lambda-free higher-order logic - report version. Tech. rep., Matryoshka Project (2018), [http://matryoshka.gforge.inria.fr/pubs/ehoh_report.pdf](http://matryoshka.gforge.inria.fr/pubs/ehoh_report.pdf) [↗](http://matryoshka.gforge.inria.fr/pubs/ehoh_report.pdf)
31. Vukmirović, P., Blanchette, J.C., Cruanes, S., Schulz, S.: Extending a brainiac prover to lambda-free higher-order logic. In: Vojnar, T., Zhang, L. (eds.) Proc. 25th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’19). pp. 192–210. No. 11427 in LNCS, Springer… [find](https://scholar.google.com/scholar?q=Vukmirovic%CC%81%2C+P%2E%2C+Blanchette%2C+J%2EC%2E%2C+Cruanes%2C+S%2E%2C+Schulz%2C+S%2E%3A+Extending+a+brainiac+prover+to+lambda%2Dfree+higher%2Dorder+logic%2E+In%3A+Vojnar%2C+T%2E%2C+Zhang%2C+L%2E+%28eds%2E%29+Proc%2E+25th+Conference+on+Tools+and+Algorithm)

*Updated 3 November 2026*