PhoX
خودکار تھیوریم ثابت کرنے میں، فوکس اعلی ترتیب کی منطق پر مبنی ایک پروف اسسٹنٹ ہے جو ایکسٹینسیبل ہے۔ صارف فوکس کو ایک ابتدائی ہدف دیتا ہے اور اس مقصد کو ثابت کرنے کے لیے ذیلی اہداف اور شواہد کے ذریعے اس کی رہنمائی کرتا ہے ؛ اندرونی طور پر، یہ قدرتی کٹوتی کے درختوں کی تعمیر کرتا ہے۔ پہلے سے ثابت شدہ ہر فارمولا بعد کے ثبوتوں کے لیے ایک اصول بن سکتا ہے۔ فوکس کو اصل میں کرسٹوف رافالی نے او سی اے ایم ایل پروگرامنگ زبان میں ڈیزائن اور نافذ کیا تھا۔ انہوں نے موجودہ ترقیاتی ٹیم کی قیادت جاری رکھی ہے، جو یونیورسٹی آف سیوائے اور یونیورسٹی پیرس VII کی مشترکہ کوشش ہے۔ فوکس پروجیکٹ کا بنیادی مقصد پیرس VII یونیورسٹی میں جین لوئس کروائن کے تیار کردہ ٹائپ سسٹم کا استعمال کرتے ہوئے صارف دوست پروف چیکر بنانا ہے۔ اس کا مقصد دوسرے نظاموں کے مقابلے میں زیادہ بدیہی ہونا ہے جبکہ توسیع پذیر، موثر اور اظہار خیال رہتا ہے۔ دوسرے نظاموں کے مقابلے میں، پروف بلڈنگ نحو آسان اور قدرتی زبان کے قریب ہے۔ دیگر خصوصیات میں جی یو آئی پر مبنی ثبوت کی تعمیر، فارمیٹڈ آؤٹ پٹ پیش کرنا، اور ایم ایل پروگرامنگ زبان میں پروگراموں کی درستگی کا ثبوت شامل ہیں۔ فی الحال سیوائے یونیورسٹی میں منطق پڑھانے کے لیے فوکس استعمال کیا جاتا ہے۔ یہ تجرباتی لیکن قابل استعمال حالت میں ہے۔ اسے سی ای سی آئی ایل ایل 2 کے تحت جاری کیا گیا ہے۔ بیرونی روابط فاکس ویب سائٹ فری تھیوریم پروورز پروف اسسٹنٹ