PhoX
स्वचालित प्रमेय साबित करने में, फोक्स उच्च-क्रम तर्क पर आधारित एक प्रमाण सहायक है जो विस्तार योग्य है। उपयोगकर्ता फोक्स को एक प्रारंभिक लक्ष्य देता है और उस लक्ष्य को साबित करने के लिए उप-लक्ष्यों और साक्ष्यों के माध्यम से इसका मार्गदर्शन करता है; आंतरिक रूप से, यह प्राकृतिक कटौती पेड़ों का निर्माण करता है। प्रत्येक पूर्व सिद्ध सूत्र बाद के प्रमाणों के लिए एक नियम बन सकता है। फोक्स को मूल रूप से ओसीएएमएल प्रोग्रामिंग भाषा में क्रिस्टोफ रफल्ली द्वारा डिजाइन और कार्यान्वित किया गया था। उन्होंने सावॉय विश्वविद्यालय और यूनिवर्सिटी पेरिस VII के संयुक्त प्रयास से वर्तमान विकास दल का नेतृत्व करना जारी रखा है। फोक्स परियोजना का प्राथमिक उद्देश्य पेरिस VII विश्वविद्यालय में जीन-लुई क्रिवाइन द्वारा विकसित प्रकार प्रणाली का उपयोग करके एक उपयोगकर्ता के अनुकूल प्रूफ चेकर बनाना है। यह विस्तार योग्य, कुशल और अभिव्यंजक रहते हुए अन्य प्रणालियों की तुलना में अधिक सहज ज्ञान युक्त होने के लिए है। अन्य प्रणालियों की तुलना में, प्रूफ-बिल्डिंग वाक्यविन्यास सरल और प्राकृतिक भाषा के करीब है। अन्य विशेषताओं में जी. यू. आई.-संचालित प्रूफ निर्माण, प्रारूपित आउटपुट प्रस्तुत करना और एम. एल. प्रोग्रामिंग भाषा में कार्यक्रमों की शुद्धता का प्रमाण शामिल है। फोक्स का उपयोग वर्तमान में सेवॉय विश्वविद्यालय में तर्क पढ़ाने के लिए किया जाता है। यह एक प्रयोगात्मक लेकिन उपयोग करने योग्य स्थिति में है। इसे सी. ई. सी. आई. एल. 2 के तहत जारी किया गया है। बाहरी लिंक फॉक्स वेबसाइट फ्री थ्योरम प्रोवर्स प्रूफ असिस्टेंट्स