<div class="csl-bib-body">
<div class="csl-entry">Vierling, J. (2018). <i>Zyklische Superposition und Induktion</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.51282</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2018.51282
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/3523
-
dc.description.abstract
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.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Beweistheorie
de
dc.subject
Automatisches Beweisen
de
dc.subject
proof theory
en
dc.subject
automated deduction
en
dc.title
Zyklische Superposition und Induktion
en
dc.title.alternative
Cyclic superposition and induction
de
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2018.51282
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Jannik Vierling
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
tuw.publication.orgunit
E180 - Fakultät für Informatik
-
dc.type.qualificationlevel
Diploma
-
dc.identifier.libraryid
AC15020641
-
dc.description.numberOfPages
84
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:1-110547
-
dc.thesistype
Diplomarbeit
de
dc.thesistype
Diploma Thesis
en
tuw.author.orcid
0000-0003-2329-5035
-
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.advisor.orcid
0000-0002-6461-5982
-
item.mimetype
application/pdf
-
item.openairetype
master thesis
-
item.openairecristype
http://purl.org/coar/resource_type/c_bdcc
-
item.openaccessfulltext
Open Access
-
item.grantfulltext
open
-
item.cerifentitytype
Publications
-
item.fulltext
with Fulltext
-
item.languageiso639-1
en
-
crisitem.author.dept
E104-02 - Forschungsbereich Computational Logic
-
crisitem.author.parentorg
E104 - Institut für Diskrete Mathematik und Geometrie
