[metis-users] theorem prover

[Joe Leslie-Hurd]

Hi Moussa,

Metis is an automatic theorem prover that takes as input some axioms
and a conjecture in first order logic, and tries to prove the
conjecture from the axioms. It uses a fixed strategy, and it's not
easy to extend it with new proof tactics.*

For your application I would recommend looking at one of the HOL
family of theorem provers, such as HOL Light:
https://github.com/jrh13/hol-light

Good luck with your project,

Joe

[*] However, it's not impossible, as the MetiTarski project shows:
https://www.cl.cam.ac.uk/~lp15/papers/Arith/

2017-02-06 1:26 GMT-08:00 موسى دمبا <bah.demba at ju.edu.sa>:
> Dear,
> I would like a theorem prover where I can add new tactics for proving
> properties of equational programs. I don't know if I can do it with metis,
> and if metis supports second order substitutions,
> many thanks,
> --
> Moussa Demba
>
>
>
> بيان إخلاء المسؤولية
>
> إن المعلومات الواردة في هذا البريد الإلكتروني وأي ملفات مرفقة هي معلومات
> خاصة بالمرسل إليه أو المتعامل و قد تحتوي على معلومات سرية أو مواد محمية
> ولذلك يحظر على أي شخص آخر الإطلاع على محتويات هذا البريد الإلكتروني. الرجاء
> إذا لم تكن أحد المعنيين باستلام هذا البريد الإلكتروني، المبادرة بإشعار
> المرسل فوراً وحذف المواد التي يتضمنها البريد الإلكتروني. يمنع منعاً باتاً
> نسخ أو توزيع أو اتخاذ أو إلغاء أي أجراء بالإعتماد على هذا البريد الإلكتروني.
> لا تتحمل جامعة الجوف أي مسؤولية قانونية عن أي أضرار ناتجة عن أي فيروس أو
> برامج ترسل بواسطة هذا البريد الإلكتروني .
>
>
> _______________________________________________
> metis-users mailing list
> metis-users at gilith.com
> http://www.gilith.com/metis/mailing-list
>