56:. In contrast to most other current provers, the implementation actually uses a purely equational paradigm, and simulates non-equational inferences via appropriate equality inferences. Significant innovations include shared term rewriting (where many possible equational simplifications are carried out in a single operation), several efficient
96:, winning the CNF/MIX category in 2000 and finishing among the top systems ever since. In 2008 it came in second place. In 2009 it won second place in the FOF (full first order logic) and UEQ (unit equational logic) categories and third place (after two versions of
31:
and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E is developed by
Stephan Schulz, originally in the
104:(clausal logic). It repeated the performance in FOF and CNF in 2010, and won a special award as "overall best" system. In the 2011 CASC-23 E won the CNF division and achieved second places in UEQ and LTB.
60:
data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour. Since version 2.0, E supports
567:
Benzmüller, Christoph; Lawrence C. Paulson; Frank Theiss; Arnaud
Fietzke (2008). "LEO-II – A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)".
41:
179:
813:
341:
798:
637:
589:
516:
255:
222:
533:
808:
468:
Tools and
Techniques for Verification of System Infrastructure – A Festschrift in Honour of Professor Michael J. C. Gordon FRS
37:
568:
803:
708:
783:
93:
433:
406:
723:
81:
315:
129:
20:
136:
strategy. E also is the reasoning engine in SInE and LEO-II and used as the clausification system for iProver.
113:
97:
69:
139:
Applications of E include reasoning on large ontologies, software verification, and software certification.
101:
183:
735:
494:
53:
28:
702:
654:
345:
740:
620:
Korovin, Konstantin (2008). "iProver—an instantiation-based theorem prover for first-order logic".
499:
633:
585:
512:
251:
218:
125:
62:
24:
745:
688:
625:
577:
504:
380:
243:
238:
Schulz, Stephan (2001). "Learning Search
Control Knowledge for Equational Theorem Proving".
210:
655:"First-Orderized ResearchCyc : Expressivity and Efficiency in a Common-Sense Ontology"
368:
542:
778:
271:
693:
676:
792:
57:
687:(1). 4th International Workshop on First-Order Theorem Proving: Elsevier: 109–119.
677:"Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs"
629:
595:
581:
576:. Lecture Notes in Computer Science. Vol. 5195. Springer. pp. 162–170.
508:
493:. Lecture Notes in Computer Science. Vol. 3097. Springer. pp. 372–384.
214:
724:"An Empirical Evaluation of Automated Theorem Provers in Software Certification"
749:
247:
460:
662:
AAAI Workshop on
Contexts and Ontologies: Theory, Practice and Applications
384:
437:
410:
753:
624:. Lecture Notes in Computer Science. Vol. 5195. pp. 292–298.
242:. Lecture Notes in Computer Science. Vol. 2174. pp. 320–334.
209:. Lecture Notes in Computer Science. Vol. 3097. pp. 223–228.
319:
112:
E has been integrated into several other theorem provers. It is, with
461:"Automation for Interactive Proof: Techniques, Lessons and Prospects"
369:"The 4th IJCAR Automated Theorem Proving System Competition--CASC-J4"
77:
121:
117:
73:
491:
Experiments on
Supporting Interactive Proof Using Resolution
653:
Ramachandran, Deepak; Pace Reagan; Keith
Goolsbery (2005).
293:
156:
Schulz, Stephan (2002). "E – A Brainiac
Theorem Prover".
728:
International
Journal on Artificial Intelligence Tools
205:
180:"Entrants System Descriptions: E 1.0pre and EP 1.0pre"
722:
Denney, Ewen; Bernd Fischer; Johan Schumann (2006).
92:The prover has consistently performed well in the
681:Electronic Notes in Theoretical Computer Science
42:Baden-Württemberg Cooperative State University
27:with equality. It is based on the equational
8:
240:KI 2001: Advances in Artificial Intelligence
173:
171:
739:
692:
498:
489:Meng, Jia; Lawrence C. Paulson (2004).
148:
80:environment. It is available under the
700:
675:Ranise, Silvio; David Déharbe (2003).
532:Sutcliffe, Geoff; et al. (2009).
52:The system is based on the equational
436:. University of Miami. Archived from
409:. University of Miami. Archived from
7:
535:The 4th IJCAR ATP System Competition
14:
434:"The CADE ATP System Competition"
407:"The CADE ATP System Competition"
316:"The CADE ATP System Competition"
294:"The E Equational Theorem Prover"
814:Software using the GPL license
342:"FOF division of CASC in 2008"
1:
799:Free software programmed in C
694:10.1016/S1571-0661(04)80656-X
459:Paulson, Lawrence C. (2008).
630:10.1007/978-3-540-71070-7_24
582:10.1007/978-3-540-71070-7_14
509:10.1007/978-3-540-25984-8_28
215:10.1007/978-3-540-25984-8_15
158:Journal of AI Communications
94:CADE ATP System Competition
830:
750:10.1142/s0218213006002576
432:Sutcliffe, Geoff (2011).
405:Sutcliffe, Geoff (2010).
367:Sutcliffe, Geoff (2009).
34:Automated Reasoning Group
707:: CS1 maint: location (
292:Schulz, Stephan (2008).
248:10.1007/3-540-45422-5_23
178:Schulz, Stephan (2008).
809:Unix programming tools
54:superposition calculus
29:superposition calculus
19:is a high-performance
385:10.3233/AIC-2009-0441
272:"news on E's website"
72:and portable to most
804:Free theorem provers
68:E is implemented in
756:on 24 February 2012
622:Automated Reasoning
570:Automated Reasoning
207:Automated Reasoning
314:Sutcliffe, Geoff.
639:978-3-540-71069-1
591:978-3-540-71069-1
518:978-3-540-22345-0
440:on 12 August 2011
373:AI Communications
257:978-3-540-42612-7
224:978-3-540-22345-0
128:, at the core of
76:variants and the
63:many-sorted logic
25:first-order logic
821:
766:
765:
763:
761:
752:. Archived from
743:
719:
713:
712:
706:
698:
696:
672:
666:
665:
659:
650:
644:
643:
617:
611:
610:
608:
606:
600:
594:. Archived from
575:
564:
558:
557:
555:
553:
547:
541:. Archived from
540:
529:
523:
522:
502:
486:
480:
479:
477:
475:
465:
456:
450:
449:
447:
445:
429:
423:
422:
420:
418:
402:
396:
395:
393:
391:
364:
358:
357:
355:
353:
344:. Archived from
338:
332:
331:
329:
327:
318:. Archived from
311:
305:
304:
302:
300:
289:
283:
282:
280:
278:
268:
262:
261:
235:
229:
228:
202:
196:
195:
193:
191:
182:. Archived from
175:
166:
165:
153:
829:
828:
824:
823:
822:
820:
819:
818:
789:
788:
775:
770:
769:
759:
757:
741:10.1.1.163.4861
721:
720:
716:
699:
674:
673:
669:
657:
652:
651:
647:
640:
619:
618:
614:
604:
602:
601:on 15 June 2011
598:
592:
573:
566:
565:
561:
551:
549:
548:on 17 June 2009
545:
538:
531:
530:
526:
519:
488:
487:
483:
473:
471:
463:
458:
457:
453:
443:
441:
431:
430:
426:
416:
414:
413:on 29 June 2010
404:
403:
399:
389:
387:
366:
365:
361:
351:
349:
348:on 15 June 2009
340:
339:
335:
325:
323:
322:on 2 March 2009
313:
312:
308:
298:
296:
291:
290:
286:
276:
274:
270:
269:
265:
258:
237:
236:
232:
225:
204:
203:
199:
189:
187:
186:on 15 June 2009
177:
176:
169:
164:(2/3): 111–126.
155:
154:
150:
145:
110:
90:
50:
12:
11:
5:
827:
825:
817:
816:
811:
806:
801:
791:
790:
787:
786:
781:
774:
773:External links
771:
768:
767:
714:
667:
645:
638:
612:
590:
559:
524:
517:
500:10.1.1.62.5009
481:
451:
424:
397:
359:
333:
306:
284:
263:
256:
230:
223:
197:
167:
147:
146:
144:
141:
109:
106:
89:
86:
49:
46:
21:theorem prover
13:
10:
9:
6:
4:
3:
2:
826:
815:
812:
810:
807:
805:
802:
800:
797:
796:
794:
785:
784:E's developer
782:
780:
777:
776:
772:
755:
751:
747:
742:
737:
734:(1): 81–107.
733:
729:
725:
718:
715:
710:
704:
695:
690:
686:
682:
678:
671:
668:
663:
656:
649:
646:
641:
635:
631:
627:
623:
616:
613:
597:
593:
587:
583:
579:
572:
571:
563:
560:
544:
537:
536:
528:
525:
520:
514:
510:
506:
501:
496:
492:
485:
482:
469:
462:
455:
452:
439:
435:
428:
425:
412:
408:
401:
398:
386:
382:
378:
374:
370:
363:
360:
347:
343:
337:
334:
321:
317:
310:
307:
295:
288:
285:
273:
267:
264:
259:
253:
249:
245:
241:
234:
231:
226:
220:
216:
212:
208:
201:
198:
185:
181:
174:
172:
168:
163:
159:
152:
149:
142:
140:
137:
135:
131:
127:
123:
119:
115:
107:
105:
103:
99:
95:
87:
85:
83:
79:
75:
71:
66:
64:
59:
58:term indexing
55:
47:
45:
43:
39:
35:
30:
26:
22:
18:
758:. Retrieved
754:the original
731:
727:
717:
703:cite journal
684:
680:
670:
661:
648:
621:
615:
603:. Retrieved
596:the original
569:
562:
550:. Retrieved
543:the original
534:
527:
490:
484:
472:. Retrieved
467:
454:
442:. Retrieved
438:the original
427:
415:. Retrieved
411:the original
400:
388:. Retrieved
379:(1): 59–72.
376:
372:
362:
350:. Retrieved
346:the original
336:
324:. Retrieved
320:the original
309:
297:. Retrieved
287:
275:. Retrieved
266:
239:
233:
206:
200:
188:. Retrieved
184:the original
161:
157:
151:
138:
134:Sledgehammer
133:
111:
108:Applications
91:
88:Competitions
67:
51:
33:
16:
15:
779:E home page
760:19 December
605:20 December
552:18 December
474:19 December
390:16 December
352:19 December
44:Stuttgart.
793:Categories
143:References
736:CiteSeerX
495:CiteSeerX
444:14 August
40:, now at
38:TU Munich
23:for full
326:24 March
299:24 March
190:24 March
130:Isabelle
664:. AAAI.
470:: 29–30
417:20 July
277:10 July
114:Vampire
98:Vampire
82:GNU GPL
738:
636:
588:
515:
497:
254:
221:
124:, and
78:Cygwin
48:System
658:(PDF)
599:(PDF)
574:(PDF)
546:(PDF)
539:(PDF)
464:(PDF)
118:SPASS
100:) in
762:2009
709:link
634:ISBN
607:2009
586:ISBN
554:2009
513:ISBN
476:2009
446:2011
419:2010
392:2009
354:2009
328:2009
301:2009
279:2017
252:ISBN
219:ISBN
192:2009
122:CVC4
74:UNIX
746:doi
689:doi
626:doi
578:doi
505:doi
381:doi
244:doi
211:doi
132:'s
102:CNF
36:at
795::
744:.
732:15
730:.
726:.
705:}}
701:{{
685:86
683:.
679:.
660:.
632:.
584:.
511:.
503:.
466:.
377:22
375:.
371:.
250:.
217:.
170:^
162:15
160:.
126:Z3
120:,
116:,
84:.
65:.
764:.
748::
711:)
697:.
691::
642:.
628::
609:.
580::
556:.
521:.
507::
478:.
448:.
421:.
394:.
383::
356:.
330:.
303:.
281:.
260:.
246::
227:.
213::
194:.
70:C
17:E
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.