Bibliographic Metadata

Title
Zyklische Superposition und Induktion / von Jannik Tim Vierling
Additional Titles
Cyclic superposition and induction
AuthorVierling, Jannik Tim
CensorHetzl, Stefan
PublishedWien, 2018
Descriptionxiii, 84 Seiten
Institutional NoteTechnische Universität Wien, Diplomarbeit, 2018
Annotation
Zusammenfassung in deutscher Sprache
Text in englischer Sprache
LanguageEnglish
Document typeThesis (Diplom)
Keywords (DE)Beweistheorie / Automatisches Beweisen
Keywords (EN)proof theory / automated deduction
URNurn:nbn:at:at-ubtuw:1-110547 Persistent Identifier (URN)
Restriction-Information
 The work is publicly available
Files
Zyklische Superposition und Induktion [0.89 mb]
Links
Reference
Classification
Abstract (English)

In 2013 Kersani and Peltier introduced the n-clause calculus, a superposition calculus enriched with a cycle detection rule realizing a form of reasoning by mathematical induction. Until now it is not known which form of induction is captured by the n-clause calculus. An upper bound in terms of the quantifier complexity of the induction invariant can be obtained by a two step translation: in a first step we encode cyclic refutations in a cyclic sequent calculus introduced by Brotherston and Simpson in 2010; in a second step we translate cyclic proofs into inductive LK proofs.

Stats
The PDF-Document has been downloaded 23 times.