Show simple item record

AuthorStrecker, Martindc.contributor.author
Date of accession2016-03-14T11:51:59Zdc.date.accessioned
Available in OPARU since2016-03-14T11:51:59Zdc.date.available
Year of creation1999dc.date.created
AbstractThis dissertation is concerned with interactive proof construction and automated proof search in type theories, in particular the Calculus of Construction and its subsystems. Type theories can be conceived as expressive logics which combine a functional programming language, strong typing and a higher-order logic. They are therefore a suitable formalism for specification and verification systems. However, due to their expressiveness, it is difficult to provide appropriate deductive support for type theories. This dissertation first examines general methods for proof construction in type theories and then explores how these methods can be refined to yield proof search procedures for specialized fragments of the language. Proof development in type theories usually requires the construction of a term having a given type in a given context. For the term to be constructed, a metavariable is introduced which is successively instantiated in the course of the proof. A naive use of metavariables leads to problems, such as non-commutativity of reduction and instantiation and the generation of ill-typed terms during reduction. For solving these problems, a calculus with explicit substitutions is introduced, and it is shown that this calculus preserves properties such as strong normalization and decidability of typing. In order to obtain a calculus appropriate for proof search, the usual natural deduction presentation of type theories is replaced by a sequent style presentation. It is shown that the calculus thus obtained is correct with respect to the original calculus. Completeness (proved with a cut-elimination argument) is shown for all predicative fragments of the lambda cube. The dissertation concludes with a discussion of some techniques that make proof search practically applicable, such as unification and pruning of the proof search space by exploiting impermutabilities of the sequent calculus.dc.description.abstract
Languageendc.language.iso
PublisherUniversität Ulmdc.publisher
LicenseStandard (Fassung vom 03.05.2003)dc.rights
Link to license texthttps://oparu.uni-ulm.de/xmlui/license_v1dc.rights.uri
KeywordBeweissuchedc.subject
LCSHLogic, symbolic and mathematicaldc.subject.lcsh
LCSHType theorydc.subject.lcsh
TitleConstruction and deduction in type theoriesdc.title
Resource typeDissertationdc.type
DOIhttp://dx.doi.org/10.18725/OPARU-3dc.identifier.doi
PPN670346462dc.identifier.ppn
URNhttp://nbn-resolving.de/urn:nbn:de:bsz:289-vts-2596dc.identifier.urn
GNDAutomatisches Beweisverfahrendc.subject.gnd
GNDTypentheoriedc.subject.gnd
FacultyFakultät für Informatikuulm.affiliationGeneral
Date of activation1999-09-17T15:53:46Zuulm.freischaltungVTS
Peer reviewneinuulm.peerReview
Shelfmark print versionI: J-H 5.236 ; W: W-H 6.168uulm.shelfmark
DCMI TypeTextuulm.typeDCMI
VTS-ID259uulm.vtsID
CategoryPublikationenuulm.category
University Bibliographyjauulm.unibibliographie


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record