AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

E 3.0 is a fully automatic theorem prover for classical first-order logic with equality, many-sorted first-order logic (with optional support for first-class Boolean formulas), and monomorpic typed higher order logic. It also supports efficient propositional reasoning, the near-zero-overhead proof objects, and the integration of machine learning for proof search. We describe the overall architecture of the system, with a focus on new features (first-class Booleans, full higher order logic, multicore-scheduling, data-driven schedule selection), discuss major aspects of the implementation, and the performance of the system on the TPTP library. We conclude with a short outlook on future work.

Jennifer Müller

+49 681 9325 2900

--email hidden

Zoom

651 8455 1540

passcode not visible

logged in users only