Models And Counter-Examples
میس کا مطلب ہے "ماڈلز اینڈ کاؤنٹر-ایکسمپلز"، اور یہ ایک ماڈل فائنڈر ہے۔ زیادہ تر خودکار تھیوریم پروورز ثبوت کے مسئلے کی شق نارمل فارم پر تردید کے ذریعے ثبوت انجام دینے کی کوشش کرتے ہیں، یہ ظاہر کرتے ہوئے کہ محوریات اور منافی قیاس آرائیوں کا مجموعہ کبھی بھی بیک وقت درست نہیں ہو سکتا، یعنی۔ کوئی نمونہ نہیں ہے۔ دوسری طرف میس جیسے ماڈل فائنڈر شقوں کے ایک سیٹ کا ایک واضح ماڈل تلاش کرنے کی کوشش کرتا ہے۔ اگر یہ کامیاب ہوتا ہے، تو یہ قیاس آرائی کے لیے ایک جوابی مثال سے مطابقت رکھتا ہے، یعنی۔ یہ (دعوی کردہ) نظریہ کو مسترد کرتا ہے۔ میس جی این یو جی پی ایل لائسنس یافتہ ہے۔ اوٹر (تھیوریم پروور) کہاوت 9 حوالہ جات بیرونی لنکس سسٹم ڈاؤن لوڈ فری تھیوریم پروورز فری سافٹ ویئر