Skip Navigation


The Computer Journal Advance Access originally published online on May 27, 2008
The Computer Journal 2009 52(7):799-807; doi:10.1093/comjnl/bxn029
This Article
Right arrow Full Text (PDF)
Right arrow All Versions of this Article:
52/7/799    most recent
bxn029v1
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Dowek, G.
Right arrow Articles by Jiang, Y.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author 2008. Published by Oxford University Press on behalf of The British Computer Society. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

This article appears in the following The Computer Journal issue: Incorporating Profiling Expertise and Behaviour Special Issue [View the issue table of contents]

Enumerating Proofs of Positive Formulae

Gilles Dowek1 and Ying Jiang2,*

1 École polytechnique and INRIA, LIX, École polytechnique, 91128 Palaiseau Cedex, France
2 State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, P.R.China

* Corresponding author: jy{at}ios.ac.cn

Received 21 September 2007; revised 19 February 2008

We provide a semi-grammatical description of the set of normal proofs of positive formulae in minimal predicate logic, i.e. a grammar that generates a set of schemes, from each of which we can produce a finite number of normal proofs. This method is complete in the sense that each normal proof-term of the formula is produced by some scheme generated by the grammar. As a corollary, we get a similar description of the set of normal proofs of positive formulae for a large class of theories including simple type theory and System F.

Key Words: positive formulae • enumerating proofs • minimal predicate logic

Guest editors: Mingsheng Ying and Ruqian Lu


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.