Elamur Research⌕
☰
home / papers / 2019 / Faster, Higher, Stronger: E 2.3

Faster, Higher, Stronger: E 2.3

Paper · 2019 · Stephan Schulz, Simon Cruanes and Petar Vukmirović

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 AmsterdamAmsterdam · Netherlands45 works · 3,544 citations

Also on the byline: Baden-Wuerttemberg Cooperative State University.

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational 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.

@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}
}

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
  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 ↗
  3. Biere, A.: PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation 4, 75–97 (2008) find
  4. Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formal. Reasoning 9(1), 101–148 (2016). 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 ↗
  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
  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
  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
  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
  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
  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
  12. McCune, W.: Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. Journal of Automated Reasoning 9(2), 147–167 (1992) find
  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
  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
  15. Schulz, S.: E – A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002) find
  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
  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
  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
  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) ↗
  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) ↗
  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
  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
  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
  24. Sutcliffe, G.: The 8th IJCAR automated theorem proving system competition– CASC-J8. AI Communications 29(5), 607–619 (2016) find
  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
  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… ↗
  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
  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
  29. Sutcliffe, G., Stickel, M., Schulz, S., Urban, J.: Answer Extraction for TPTP. http://www.cs.miami.edu/~tptp/TPTP/Proposals/AnswerExtraction. html, (acccessed 2013-07-08) ↗
  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 ↗
  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

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/schulz-2019-faster-higher-stronger-e-2/