On the Generation of Quantified Lemmas

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...

Full description

Saved in:
Bibliographic Details
Main Author: Gabriel Ebner (23277217) (author)
Other Authors: Stefan Hetzl (23277220) (author), Alexander Leitsch (23277223) (author), Giselle Reis (23276149) (author), Daniel Weller (8409270) (author)
Published: 2018
Subjects:
Information and computing sciences
Artificial intelligence
Mathematical sciences
Pure mathematics
Cut-introduction
Herbrand’s theorem
Proof theory
Lemma generation
The resolution calculus
Tags: Add Tag
No Tags, Be the first to tag this record!

Similar Items