Change search
ReferencesLink to record
Permanent link

Direct link
General Metarules for Interactive Modular Construction of Natural Deduction Proofs
Stockholm University, Faculty of Social Sciences, Department of Computer and Systems Sciences.
2003 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

This thesis proposes a set of general metarules for interactive modular construction of natural deduction proofs.

Interactive proof support systems are used for the construction of formal proofs in formal program development. They support the user interaction in the derivation of programs from specifications and in the development of proofs of properties of programs. Moreover, interactive proof support systems are often general theorem provers and provide general support for proof development. Natural deduction with its similarity to intuitive informal reasoning and its lucid proof explanations is ideal for interactive proof development. However, the formal proofs in formal program development tend to be long and detailed, and metarules for the development of proofs in natural deduction would give shorter proofs and facilitate the user interaction.

The focus of the thesis is the characterization of general metarules for the interactive construction of proofs in natural deduction. The solution presented supports modularity and flexibility in interactive proof development and it provides interactive construction of proofs at metalevel and facilitates the presentation of the proofs at different levels of abstraction.

The main contributions are:

· General metarules for modular proof development.

The general metarules for the interactive construction of derivations in natural deduction support the construction of proofs from proof parts. They compute parts of proofs on the demand of the user. By computing derived rules for each application, a user has important leeway in the number of rules to use.

· Flexibility in the development of proofs.

The flexibility in the interactive development of proofs is supported by general metarules for changes. The method for performing changes to proofs is based upon the replacement of parts of proofs.

· A proof structure supporting the development of fragmentary proofs.

· Explanations of proofs at different levels in accordance with the inference rules of natural deduction and the general metarules.

Place, publisher, year, edition, pages
Kista: Department of Computer and Systems Sciences (together with KTH), Stockholm University , 2003. , 134 p.
Report Series / Department of Computer & Systems Sciences, ISSN 1101-8526 ; 03:04
National Category
Computer Science
Research subject
Computer and Systems Sciences
URN: urn:nbn:se:su:diva-7509ISBN: 91-7265-613-1OAI: diva2:198465
Public defence
2003-05-07, Sal C, Forum, Isafjordsgatan 39, Kista, 13:00 (English)
Available from: 2003-04-14 Created: 2003-04-14 Last updated: 2009-06-25Bibliographically approved

Open Access in DiVA

No full text

By organisation
Department of Computer and Systems Sciences
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 54 hits
ReferencesLink to record
Permanent link

Direct link