Enumerating proofs of positive formulae
Logic in Computer Science
2023-05-03 v1
Abstract
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.
Cite
@article{arxiv.2305.01440,
title = {Enumerating proofs of positive formulae},
author = {Gilles Dowek and Ying Jiang},
journal= {arXiv preprint arXiv:2305.01440},
year = {2023}
}