First Order Logic; Sequent Calculus; Logic; Automated Deduction
en
Abstract:
Nach der Definition einer Verallgemeinerung des Herbrandschen Theorems für Sequente, beschreiben wir drei schon existierende Algorithmen für die Extraktion eines Herbrandsequents aus formalen Beweisen, die im Sequentialkalkül LK geschrieben sind. Darüber hinaus verbessern wir diese drei Algorithmen und entwicklen daraus einen vierten Algorithmus, welcher deren Ideen vereinigt und generalisiert.<br />Dieser Algorithmus wurde dann realisiert und in das CERes (Cut-Elimination by Resolution) Projekt integriert. Die Wichtigkeit der Extraktion von Herbrandsequenten liegt darin, dass Herbrandsequente die Kreativität der Beweise enthält.<br />
de
After defining a generalization of Herbrand's Theorem for sequents, we describe three pre-existing algorithms for the extraction of a Herbrand sequent of the end-sequent of proofs in the Sequent Calculus LK. Furthermore, we improve these three algorithms by designing a new fourth algorithm, which combines and generalizes their essential ideas. The implementation of this new algorithm was realized within the framework of the project CERes (Cut-Elimination by Resolution). The importance of extracting Herbrand sequents from proofs lies on the fact that a Herbrand sequent summarizes the creative content of a proof.
