Emacs-KB-ATP
Brief:
Imbue Emacs Lisp with a knowledge base and an automated theorem prover
Jump To: Parent Description
Jump To: Parent Description
- Emacs Lisp is similar to other Lisps, and lisp can be taken as the basis of a formal mathematical system. Therefore it may be possible to create theorem provers and associated knowledge bases directly in emacs. This would speed up some emacs related tasks and improve it's general "intelligence." We might consider using something similar to acl2, which is a theorem proving environment which uses an applicative subset of Common Lisp. There may be other Lisp ATP systems out there that we could either port or utilize. Furthermore, Chaitin has proven a number of results using Lisp systems, if his code is available and suitably licensed we could prove some metamathematical results using it. Would be nice to interface with other ATP systems as well, such as export. UniLang/FreeKBS2 already has an emacs syntax translatable to unilang's Prolog-like interlingua, which can be exported to vampire-kif and reasoned with.