سباس

SPASS هو برنامج آلي لإثبات النظريات في منطق الرتبة الأولى مع المساواة، طُوِّر في معهد ماكس بلانك لعلوم الحاسوب ، ويستخدم حساب التراكب . وكان الاسم في الأصل اختصارًا لـ Synergetic Prover Augmenting Superposition with Sorts . يُصدر نظام إثبات النظريات بموجب ترخيص FreeBSD . ^{[ 1 ]}

أضافت إضافة SPASS-XDB، وهي امتداد لبرنامج SPASS، دعمًا لاسترجاع بديهيات الوحدة الموجبة من مصادر خارجية بشكل فوري. ^{[ 2 ]} وبذلك، يستطيع SPASS-XDB دمج البيانات الواردة من قواعد البيانات العلائقية ، أو خدمات الويب ، أو خوادم البيانات المرتبطة . كما أُضيف دعم للعمليات الحسابية باستخدام برنامج Mathematica . ^{[ 3 ]}

مراجع

^ "معهد ماكس بلانك للمعلوماتية - أتمتة المنطق: سباس" . Spass-prover.org . 2010-05-28 . تم الاسترجاع 2016/08/10 .
↑ سودا، مارتن؛ سوتكليف، جيف؛ فيشنفسكي، باتريك؛ لاموت-شوبرت، مانويل؛ دي ميلو، جيرارد (2009). "مصادر خارجية للبديهيات في إثبات النظريات الآلي" . KI 2009: التطورات في الذكاء الاصطناعي . سلسلة محاضرات في علوم الحاسوب. المجلد 5803. الصفحات 281-288 . doi : 10.1007/978-3-642-04617-9_36 . ISBN 978-3-642-04616-2تم الاطلاع عليه بتاريخ 10 أغسطس 2016 .
↑ ديفيد ستانوفسكي؛ مارتن سودا؛ جيف سوتكليف. "SPASS-XDB نحو الرياضيات" (ملف PDF) . Karlin.mff.cuni.cz . تاريخ الاسترجاع: 10 أغسطس 2016 .

وايدنباخ، كريستوف؛ ديموفا، ديليانا؛ فيتزكي، أرنو؛ كومار، روهيت؛ سودا، مارتن؛ فيشنفسكي، باتريك (2009)، "SPASS الإصدار 3.5"، CADE -22: المؤتمر الدولي الثاني والعشرون للاستدلال الآلي ، سبرينغر، ص 140-145 .