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