On the Generation of Quantified Lemmas

<p dir="ltr">In this paper we present an algorithmic method of lemma introduction. Given a proof in predicate logic with equality the algorithm is capable of introducing several universal lemmas. The method is based on an inversion of Gentzen’s cut-elimination method for sequent calc...

وصف كامل

محفوظ في:
التفاصيل البيبلوغرافية
المؤلف الرئيسي: Gabriel Ebner (23277217) (author)
مؤلفون آخرون: Stefan Hetzl (23277220) (author), Alexander Leitsch (23277223) (author), Giselle Reis (23276149) (author), Daniel Weller (8409270) (author)
منشور في: 2018
الموضوعات:
الوسوم: إضافة وسم
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!

مواد مشابهة